PolymorphicPerplexion

Tags:basic

Polymorphism plays a vital role in automating verification in LH. However, thanks to its ubiquity, we often take it for granted, and it can be quite baffling to figure out why verification fails with monomorphic signatures. Let me explain why, using a simple example that has puzzled me and other users several times.

22: 
23: module PolymorphicPerplexion where

A Type for Ordered Lists

Previously we have seen how you can use LH to define a type of lists whose values are in increasing (ok, non-decreasing!) order.

First, we define an IncList a type, with Emp (“empty”) and :< (“cons”) constructors.

38: data IncList a = Emp
39:                | (:<) { hd :: a, tl :: IncList a }
40: 
41: infixr 9 :<

Next, we refine the type to specify that each “cons” :< constructor takes as input a hd and a tl which must be an IncList a of values v each of which is greater than hd .

50: {-@ data IncList a = Emp 
51:                    | (:<) { hd :: a, tl :: IncList {v:a | hd <= v}}  
52:   @-}

We can confirm that the above definition ensures that the only legal values are increasingly ordered lists, as LH accepts the first list below, but rejects the second where the elements are out of order.

61: legalList :: IncList Int
62: (PolymorphicPerplexion.IncList GHC.Types.Int)legalList = GHC.Types.Int0 :< GHC.Types.Int1 :< GHC.Types.Int2 :< GHC.Types.Int3 :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp
63: 
64: illegalList :: IncList Int 
65: (PolymorphicPerplexion.IncList GHC.Types.Int)illegalList = GHC.Types.Int0 :< GHC.Types.Int1 :< GHC.Types.Int3 :< GHC.Types.Int2 :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp

A Polymorphic Insertion Sort

Next, lets write a simple insertion-sort function that takes a plain unordered list of [a] and returns the elements in increasing order:

76: insertSortP :: (Ord a) => [a] -> IncList a
77: forall a .
(GHC.Classes.Ord<[]> a) =>
[a] -> (PolymorphicPerplexion.IncList a)insertSortP [a]xs = foldr a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)insertP {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp {v : [a] | len v >= 0
           && v == xs}xs
78: 
79: insertP             :: (Ord a) => a -> IncList a -> IncList a
80: forall a .
(GHC.Classes.Ord<[]> a) =>
a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)insertP ay Emp       = {VV : a | VV == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp
81: insertP y (x :< xs)
82:   | {VV : a | VV == y}y <= {VV : a | VV == x}x         = {VV : a | VV == y}y :< {VV : a | VV == x}x :< {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs
83:   | otherwise      = {VV : a | VV == x}x :< (PolymorphicPerplexion.IncList a)insertP {VV : a | VV == y}y {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs

Happily, LH is able to verify the above code without any trouble! (If that seemed too easy, don’t worry: if you mess up the comparison, e.g. change the guard to x <= y LH will complain about it.)

A Monomorphic Insertion Sort

However, lets take the exact same code as above but change the type signatures to make the functions monomorphic , here, specialized to Int lists.

99: insertSortM :: [Int] -> IncList Int 
100: [GHC.Types.Int] -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertSortM [GHC.Types.Int]xs = foldr GHC.Types.Int -> (PolymorphicPerplexion.IncList GHC.Types.Int) -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertM {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp {v : [GHC.Types.Int] | len v >= 0
                       && v == xs}xs
101: 
102: insertM            :: Int -> IncList Int -> IncList Int 
103: GHC.Types.Int -> (PolymorphicPerplexion.IncList GHC.Types.Int) -> (PolymorphicPerplexion.IncList GHC.Types.Int)insertM GHC.Types.Inty Emp      = {v : GHC.Types.Int | v == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp
104: insertM y (x :< xs)
105:   | {v : GHC.Types.Int | v == y}y <= {v : GHC.Types.Int | v == x}x         = {v : GHC.Types.Int | v == y}y :< {v : GHC.Types.Int | v == x}x :< {v : (PolymorphicPerplexion.IncList {v : GHC.Types.Int | x <= v}) | v == xs}xs
106:   | otherwise      = {v : GHC.Types.Int | v == x}x :< (PolymorphicPerplexion.IncList GHC.Types.Int)insertM {v : GHC.Types.Int | v == y}y {v : (PolymorphicPerplexion.IncList {v : GHC.Types.Int | x <= v}) | v == xs}xs

Huh? Now LH appears to be unhappy with the code! How is this possible?

Lets look at the type error:

114:  /Users/rjhala/PerplexingPolymorphicProperties.lhs:80:27-38: Error: Liquid Type Mismatch
115:   
116:  80 |   | otherwise      = x :
	

LH		expects
that since we’re using the “cons” operator		:<
the “tail” value		insertM y xs
must contain values		VV
that are greater than the “head”		x
. The error says that, LH cannot prove this requirement of		actual
list		insertM y xs
.	
	
Hmm, well thats a puzzler. Two questions that should come to mind.
	

		

			

				Why
does the above fact hold in the first place?			
		
		

			

				How
is LH able to deduce this fact with the				polymorphic
signature but not the monomorphic one?			
		
	
	

Lets ponder the first question: why		is
every element of		insert y xs
in fact larger than		x
? For three reasons:	
	

		

			

every element in				xs
is larger than				x
, as the list				x :
was ordered,			

		

		

			

				y
is larger than				x
as established by the				otherwise
and crucially			
		
		

			

the elements returned by				insert y xs
are either				y
or from				xs
!			
		
	

	

Now onto the second question: how		does
LH verify the polymorphic code, but not the monomorphic one? The reason is the fact (c)! LH is a		modular
verifier, meaning that the		only
information that it has about the behavior of		insert
at a call-site is the information captured in the (refinement)		type specification
for		insert
. The		polymorphic
signature:	
	
156: insertP :: (Ord a) => a -> IncList a -> IncList a
	

via		parametricity
, implicitly states fact (c). That is, if at a call-site		insertP y xs
we pass in a value that is greater an		x
and a list of values greater than		x
then via		polymorphic instantiation
at the call-site, LH infers that the returned value must also be a list of elements greater than		x
!	
	

However, the		monomorphic
signature	
	
167: insertM :: Int -> IncList Int -> IncList Int
	

offers no such insight. It simply says the function takes in an		Int
and another ordered list of		Int
and returns another ordered list, whose actual elements could be arbitrary		Int
. Specifically, at the call-site		insertP y xs
LH has no way to conclude the the returned elements are indeed greater than		x
and hence rejects the monomorphic code.	
	
Perplexity
	

While parametricity is all very nice, and LH’s polymorphic instanatiation is very clever and useful, it can also be quite mysterious. For example, q curious user Oisín		pointed out
that while the code below is		rejected
that if you		uncomment
the type signature for		go
then it is		accepted
by LH!	
	
187: insertSortP' :: (Ord a) => [a] -> IncList a 
188: forall a .
(GHC.Classes.Ord<[]> a) =>
[a] -> (PolymorphicPerplexion.IncList a)insertSortP' = (PolymorphicPerplexion.IncList a)foldr a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)go {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp 
189:   where
190:     -- go :: (Ord a) => a -> IncList a -> IncList a
191:     a -> (PolymorphicPerplexion.IncList a) -> (PolymorphicPerplexion.IncList a)go ay Emp       = {VV : a | VV == y}y :< {VV : forall a . (PolymorphicPerplexion.IncList a) | VV == Emp}Emp
192:     go y (x :< xs)
193:       | {VV : a | VV == y}y <= {VV : a | VV == x}x     = {VV : a | VV == y}y :< {VV : a | VV == x}x :< {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs
194:       | otherwise  = {VV : a | VV == x}x :< (PolymorphicPerplexion.IncList a)go {VV : a | VV == y}y {v : (PolymorphicPerplexion.IncList {VV : a | x <= VV}) | v == xs}xs
	

This is thoroughly perplexing, but again, is explained by the absence of parametricity. When we		remove
the type signature, GHC defaults to giving		go
a		monomorphic
signature where the		a
is not universally quantified, and which roughly captures the same specification as the monomorphic		insertM
above causing verification to fail!	
	

Restoring the signature provides LH with the polymorphic specification, which can be instantiated at the call-site to recover the fact		(c)
that is crucial for verification.	
	
Moral
	
I hope that example illustrates two points.
	

First,		parametric polymorphism
lets type specifications say a lot more than they immediately let on: so do write polymorphic signatures whenever possible.	
	

Second, on a less happy note,		explaining
why fancy type checkers fail remains a vexing problem, whose difficulty is compounded by increasing the cleverness of the type system.	
	
We’d love to hear any ideas you might have to solve the explanation problem!