Yesterday someone asked on Reddit how one might define GHC’s OrdList
in a way that statically enforces its three key invariants. The accepted
solution required rewriting OrdList as a GADT indexed by a proof of
emptiness (which is essentially created by a run-time check), and used
the new Closed Type Families extension in GHC 7.8 to define a type-level
join of the Emptiness index.
Today, let’s see a somewhat more direct way of tackling this problem in LiquidHaskell, in which we need not change a single line of code (well.. maybe one), and need not perform any dynamic checks.
27: module OrdList( 28: OrdList, 29: nilOL, isNilOL, unitOL, appOL, consOL, snocOL, concatOL, 30: mapOL, fromOL, toOL, foldrOL, foldlOL, foldr', concatOL' 31: ) where 32: 33: infixl 5 `appOL` 34: infixl 5 `snocOL` 35: infixr 5 `consOL` 36: -- UGH parsing issues... 37: {-@ 38: data OrdList [olen] a = None 39: | One (x :: a) 40: | Many (xs :: ListNE a) 41: | Cons (x :: a) (xs :: OrdList a) 42: | Snoc (xs :: OrdList a) (x :: a) 43: | Two (x :: OrdListNE a) (y :: OrdListNE a) 44: @-}
The OrdList Type
The OrdList type is defined as follows:
54: data OrdList a 55: = None 56: | One a 57: | Many [a] -- Invariant: non-empty 58: | Cons a (OrdList a) 59: | Snoc (OrdList a) a 60: | Two (OrdList a) -- Invariant: non-empty 61: (OrdList a) -- Invariant: non-empty
As indicated by the comments the key invariants are that:
Manyshould take a non-empty list,Twotakes two non-emptyOrdLists.
What is a Non-Empty OrdList?
To proceed, we must tell LiquidHaskell what non-empty means. We do this with a measure that describes the number of elements in a structure. When this number is strictly positive, the structure is non-empty.
We’ve previously seen how to measure the size of a list.77: measure len :: [a] -> Int 78: len ([]) = 0 79: len (x:xs) = 1 + (len xs)
We can use the same technique to measure the size of an OrdList.
85: {-@ measure olen :: OrdList a -> Int 86: olen (None) = 0 87: olen (One x) = 1 88: olen (Many xs) = (len xs) 89: olen (Cons x xs) = 1 + (olen xs) 90: olen (Snoc xs x) = 1 + (olen xs) 91: olen (Two x y) = (olen x) + (olen y) 92: @-} 93: 94: {-@ invariant {v:OrdList a | (olen v) >= 0} @-}
Now, we can use the measures to define aliases for non-empty lists and OrdLists.
100: {-@ type ListNE a = {v:[a] | (len v) > 0} @-} 101: {-@ type OrdListNE a = {v:OrdList a | (olen v) > 0} @-}
Capturing the Invariants In a Refined Type
Let’s return to the original type, and refine it with the above non-empty variants to specify the invariants as part of the data declaration110: {-@ data OrdList [olen] a 111: = None 112: | One (x :: a) 113: | Many (xs :: ListNE a) 114: | Cons (x :: a) (xs :: OrdList a) 115: | Snoc (xs :: OrdList a) (x :: a) 116: | Two (x :: OrdListNE a) (y :: OrdListNE a) 117: @-}
Notice immediately that LiquidHaskell can use the refined definition to warn us
about malformed OrdList values.
124: (OrdList.OrdList {VV : (GHC.Integer.Type.Integer) | (VV > 0)})ok = x1:{x6 : [{x9 : (GHC.Integer.Type.Integer) | (x9 > 0)}] | ((len x6) > 0)} -> {x2 : (OrdList.OrdList {x9 : (GHC.Integer.Type.Integer) | (x9 > 0)}) | ((olen x2) == (len x1))}Many {x5 : [{x11 : (GHC.Integer.Type.Integer) | (x11 > 0)}]<\x9 VV -> (x8 > 0) && (x8 > x9)> | (((null x5)) <=> false) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}[1,2,3] 125: forall a. {VV : (OrdList.OrdList {VV : a | false}) | ((olen VV) == 0)}bad = x1:{x4 : [{VV : a | false}] | ((len x4) > 0)} -> {x2 : (OrdList.OrdList {VV : a | false}) | ((olen x2) == (len x1))}Many {x8 : [{VV : a | false}]<\_ VV -> false> | (((null x8)) <=> true) && ((len x8) == 0) && ((olens x8) == 0) && ((sumLens x8) == 0) && ((len x8) >= 0) && ((olens x8) >= 0) && ((sumLens x8) >= 0)}[] 126: {VV : (OrdList.OrdList {VV : (GHC.Integer.Type.Integer) | (VV > 0)}) | ((olen VV) == (olen OrdList.ok))}badder = x1:{x10 : (OrdList.OrdList {x12 : (GHC.Integer.Type.Integer) | (x12 > 0)}) | ((olen x10) > 0)} -> x2:{x6 : (OrdList.OrdList {x12 : (GHC.Integer.Type.Integer) | (x12 > 0)}) | ((olen x6) > 0)} -> {x2 : (OrdList.OrdList {x12 : (GHC.Integer.Type.Integer) | (x12 > 0)}) | ((olen x2) == ((olen x1) + (olen x2)))}Two {x3 : (OrdList.OrdList {x4 : (GHC.Integer.Type.Integer) | false}) | ((olen x3) == 0) && ((olen x3) >= 0)}None {x3 : (OrdList.OrdList {x5 : (GHC.Integer.Type.Integer) | (x5 > 0)}) | (x3 == OrdList.ok) && ((olen x3) >= 0)}ok
All of the above are accepted by GHC, but only the first one is actually a valid
OrdList. Happily, LiquidHaskell will reject the latter two, as they violate
the invariants.
Basic Functions
Now let’s look at some of the functions!
First, we’ll define a handy alias for OrdLists of a given size:
142: {-@ type OrdListN a N = {v:OrdList a | (olen v) = N} @-}
Now, the nilOL constructor returns an empty OrdList:
148: {-@ nilOL :: OrdListN a {0} @-} 149: forall a. {v : (OrdList.OrdList a) | ((olen v) == 0)}nilOL = forall a. {x2 : (OrdList.OrdList a) | ((olen x2) == 0)}None
the unitOL constructor returns an OrdList with one element:
155: {-@ unitOL :: a -> OrdListN a {1} @-} 156: forall a. a -> {v : (OrdList.OrdList a) | ((olen v) == 1)}unitOL aas = {VV : a | (VV == as)} -> {x2 : (OrdList.OrdList {VV : a | (VV == as)}) | ((olen x2) == 1)}One {VV : a | (VV == as)}as
and snocOL and consOL return outputs with precisely one more element:
162: {-@ snocOL :: xs:OrdList a -> a -> OrdListN a {1 + (olen xs)} @-} 163: forall a. xs:(OrdList.OrdList a) -> a -> {v : (OrdList.OrdList a) | ((olen v) == (1 + (olen xs)))}snocOL (OrdList.OrdList a)as ab = x1:(OrdList.OrdList a) -> a -> {x2 : (OrdList.OrdList a) | ((olen x2) == (1 + (olen x1)))}Snoc {x3 : (OrdList.OrdList a) | (x3 == as) && ((olen x3) >= 0)}as {VV : a | (VV == b)}b 164: 165: {-@ consOL :: a -> xs:OrdList a -> OrdListN a {1 + (olen xs)} @-} 166: forall a. a -> xs:(OrdList.OrdList a) -> {v : (OrdList.OrdList a) | ((olen v) == (1 + (olen xs)))}consOL aa (OrdList.OrdList a)bs = a -> x2:(OrdList.OrdList a) -> {x2 : (OrdList.OrdList a) | ((olen x2) == (1 + (olen x2)))}Cons {VV : a | (VV == a)}a {x3 : (OrdList.OrdList a) | (x3 == bs) && ((olen x3) >= 0)}bs
Note: The OrdListN a {e} syntax just lets us use LiquidHaskell
expressions e as a parameter to the type alias OrdListN.
175: {-@ isNilOL :: xs:OrdList a -> {v:Bool | ((Prop v) <=> ((olen xs) = 0))} @-} 176: forall a. xs:(OrdList.OrdList a) -> {v : (GHC.Types.Bool) | (((Prop v)) <=> ((olen xs) == 0))}isNilOL None = {x3 : (GHC.Types.Bool) | ((Prop x3)) && (x3 == GHC.Types.True)}True 177: isNilOL _ = {x3 : (GHC.Types.Bool) | (not (((Prop x3)))) && (x3 == GHC.Types.False)}False
Appending OrdLists
The above functions really aren’t terribly interesting, however, since their
types fall right out of the definition of olen.
So how about something that takes a little thinking?
190: {-@ appOL :: xs:OrdList a -> ys:OrdList a 191: -> OrdListN a {(olen xs) + (olen ys)} 192: @-} 193: None forall a. xs:(OrdList.OrdList a) -> ys:(OrdList.OrdList a) -> {v : (OrdList.OrdList a) | ((olen v) == ((olen xs) + (olen ys)))}`appOL` (OrdList.OrdList a)b = {x3 : (OrdList.OrdList a) | (x3 == b) && ((olen x3) >= 0)}b 194: a `appOL` None = {x2 : (OrdList.OrdList a) | ((olen x2) >= 0)}a 195: One a `appOL` b = {VV : a | (VV == a) && (VV > a) && (VV < a)} -> x2:(OrdList.OrdList {VV : a | (VV == a) && (VV > a) && (VV < a)}) -> {x2 : (OrdList.OrdList {VV : a | (VV == a) && (VV > a) && (VV < a)}) | ((olen x2) == (1 + (olen x2)))}Cons {VV : a | (VV == a)}a {x3 : (OrdList.OrdList a) | (x3 == b) && ((olen x3) >= 0)}b 196: a `appOL` One b = x1:(OrdList.OrdList {VV : a | (VV == b) && (VV > b) && (VV < b)}) -> {VV : a | (VV == b) && (VV > b) && (VV < b)} -> {x2 : (OrdList.OrdList {VV : a | (VV == b) && (VV > b) && (VV < b)}) | ((olen x2) == (1 + (olen x1)))}Snoc {x2 : (OrdList.OrdList a) | ((olen x2) >= 0)}a {VV : a | (VV == b)}b 197: a `appOL` b = x1:{x6 : (OrdList.OrdList a) | ((olen x6) > 0)} -> x2:{x4 : (OrdList.OrdList a) | ((olen x4) > 0)} -> {x2 : (OrdList.OrdList a) | ((olen x2) == ((olen x1) + (olen x2)))}Two {x2 : (OrdList.OrdList a) | ((olen x2) >= 0)}a {x3 : (OrdList.OrdList a) | (x3 == b) && ((olen x3) >= 0)}b
appOL takes two OrdLists and returns a list whose length is the sum of
the two input lists. The most important thing to notice here is that we haven’t
had to insert any extra checks in appOL, unlike the GADT solution.
LiquidHaskell uses the definition of olen to infer that in the last case of
appOL, a and b must be non-empty, so they are valid arguments to Two.
We can prove other things about OrdLists as well, like the fact
that converting an OrdList to a Haskell list preserves length
211: {-@ toOL :: xs:[a] -> OrdListN a {(len xs)} @-} 212: forall a. xs:[a] -> {v : (OrdList.OrdList a) | ((olen v) == (len xs))}toOL [] = forall a. {x2 : (OrdList.OrdList a) | ((olen x2) == 0)}None 213: toOL xs = x1:{x4 : [a] | ((len x4) > 0)} -> {x2 : (OrdList.OrdList a) | ((olen x2) == (len x1))}Many {x4 : [a] | ((len x4) >= 0) && ((olens x4) >= 0) && ((sumLens x4) >= 0)}xs
as does mapping over an OrdList
219: {-@ mapOL :: (a -> b) -> xs:OrdList a -> OrdListN b {(olen xs)} @-} 220: forall a b. (b -> a) -> x3:(OrdList.OrdList b) -> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL _ None = forall a. {x2 : (OrdList.OrdList a) | ((olen x2) == 0)}None 221: mapOL f (One x) = a -> {x2 : (OrdList.OrdList a) | ((olen x2) == 1)}One (a -> bf {VV : a | (VV == x)}x) 222: mapOL f (Cons x xs) = a -> x2:(OrdList.OrdList a) -> {x2 : (OrdList.OrdList a) | ((olen x2) == (1 + (olen x2)))}Cons (a -> bf {VV : a | (VV == x)}x) (forall a b. (b -> a) -> x3:(OrdList.OrdList b) -> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL a -> bf {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs) 223: mapOL f (Snoc xs x) = x1:(OrdList.OrdList a) -> a -> {x2 : (OrdList.OrdList a) | ((olen x2) == (1 + (olen x1)))}Snoc (forall a b. (b -> a) -> x3:(OrdList.OrdList b) -> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL a -> bf {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs) (a -> bf {VV : a | (VV == x)}x) 224: mapOL f (Two x y) = x1:{x6 : (OrdList.OrdList a) | ((olen x6) > 0)} -> x2:{x4 : (OrdList.OrdList a) | ((olen x4) > 0)} -> {x2 : (OrdList.OrdList a) | ((olen x2) == ((olen x1) + (olen x2)))}Two (forall a b. (b -> a) -> x3:(OrdList.OrdList b) -> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL a -> bf {x4 : (OrdList.OrdList a) | (x4 == x) && ((olen x4) > 0) && ((olen x4) >= 0)}x) (forall a b. (b -> a) -> x3:(OrdList.OrdList b) -> {VV : (OrdList.OrdList a) | ((olen VV) == (olen x3))}mapOL a -> bf {x4 : (OrdList.OrdList a) | (x4 == y) && ((olen x4) > 0) && ((olen x4) >= 0)}y) 225: mapOL f (Many xs) = x1:{x4 : [a] | ((len x4) > 0)} -> {x2 : (OrdList.OrdList a) | ((olen x2) == (len x1))}Many ((a -> b) -> x3:[a] -> {x2 : [b] | ((len x2) == (len x3))}map a -> bf {x6 : [a] | (x6 == xs) && ((len x6) > 0) && ((len x6) >= 0) && ((olens x6) >= 0) && ((sumLens x6) >= 0)}xs)
as does converting a Haskell list to an OrdList.
231: {-@ type ListN a N = {v:[a] | (len v) = N} @-} 232: 233: {-@ fromOL :: xs:OrdList a -> ListN a {(olen xs)} @-} 234: forall a. xs:(OrdList.OrdList a) -> {v : [a] | ((len v) == (olen xs))}fromOL (OrdList.OrdList a)a = x1:(OrdList.OrdList a) -> x2:{x4 : [a] | ((len x4) == 0)} -> {x2 : [a] | ((len x2) == ((olen x1) + (len x2)))}go {x3 : (OrdList.OrdList a) | (x3 == a) && ((olen x3) >= 0)}a {x8 : [{VV : a | false}]<\_ VV -> false> | (((null x8)) <=> true) && ((len x8) == 0) && ((olens x8) == 0) && ((sumLens x8) == 0) && ((len x8) >= 0) && ((olens x8) >= 0) && ((sumLens x8) >= 0)}[] 235: where 236: {-@ go :: xs:_ -> ys:_ 237: -> {v:_ | (len v) = (olen xs) + (len ys)} 238: @-} 239: x1:(OrdList.OrdList a) -> x2:{VV : [a] | ((len VV) >= 0)} -> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go None {VV : [a] | ((len VV) >= 0)}acc = {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc 240: go (One a) acc = {VV : a | (VV == a)}a forall <p :: a-> a-> Bool>. x1:a -> x2:[{VV : a<p x1> | true}]<p> -> {x5 : [a]<p> | (((null x5)) <=> false) && ((len x5) == (1 + (len x2))) && ((olens x5) == ((olen x1) + (olens x2))) && ((sumLens x5) == ((len x1) + (sumLens x2)))}: {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc 241: go (Cons a b) acc = {VV : a | (VV == a)}a forall <p :: a-> a-> Bool>. x1:a -> x2:[{VV : a<p x1> | true}]<p> -> {x5 : [a]<p> | (((null x5)) <=> false) && ((len x5) == (1 + (len x2))) && ((olens x5) == ((olen x1) + (olens x2))) && ((sumLens x5) == ((len x1) + (sumLens x2)))}: x1:(OrdList.OrdList a) -> x2:{VV : [a] | ((len VV) >= 0)} -> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go {x3 : (OrdList.OrdList a) | (x3 == b) && ((olen x3) >= 0)}b {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc 242: go (Snoc a b) acc = x1:(OrdList.OrdList a) -> x2:{VV : [a] | ((len VV) >= 0)} -> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go {x3 : (OrdList.OrdList a) | (x3 == a) && ((olen x3) >= 0)}a ({VV : a | (VV == b)}bforall <p :: a-> a-> Bool>. x1:a -> x2:[{VV : a<p x1> | true}]<p> -> {x5 : [a]<p> | (((null x5)) <=> false) && ((len x5) == (1 + (len x2))) && ((olens x5) == ((olen x1) + (olens x2))) && ((sumLens x5) == ((len x1) + (sumLens x2)))}:{x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc) 243: go (Two a b) acc = x1:(OrdList.OrdList a) -> x2:{VV : [a] | ((len VV) >= 0)} -> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go {x4 : (OrdList.OrdList a) | (x4 == a) && ((olen x4) > 0) && ((olen x4) >= 0)}a (x1:(OrdList.OrdList a) -> x2:{VV : [a] | ((len VV) >= 0)} -> {v : [a] | ((len v) == ((olen x1) + (len x2)))}go {x4 : (OrdList.OrdList a) | (x4 == b) && ((olen x4) > 0) && ((olen x4) >= 0)}b {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc) 244: go (Many xs) acc = {x6 : [a] | (x6 == xs) && ((len x6) > 0) && ((len x6) >= 0) && ((olens x6) >= 0) && ((sumLens x6) >= 0)}xs x1:[a] -> x2:[a] -> {x2 : [a] | ((len x2) == ((len x1) + (len x2)))}++ {x5 : [a] | (x5 == acc) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}acc
though for this last one we actually need to provide an explicit qualifier, which we haven’t really seen so far. Can anyone guess why?
252: {-@ qualif Go(v:List a, xs:OrdList a, ys:List a): 253: (len v) = (olen xs) + (len ys) 254: @-}
The answer is that the return type of go must refer to the length
of the OrdList that it’s folding over as well as the length of
the accumulator acc! We haven’t written a refinement like that in
any of our type signatures in this module, so LiquidHaskell doesn’t
know to guess that type.
There’s nothing super interesting to say about the foldOLs but I’ll
include them here for completeness’ sake.
268: foldrOL :: (a->b->b) -> b -> OrdList a -> b 269: forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL _ az None = {VV : a | (VV == z)}z 270: foldrOL k z (One x) = a -> b -> bk {VV : a | (VV == x)}x {VV : a | (VV == z)}z 271: foldrOL k z (Cons x xs) = a -> b -> bk {VV : a | (VV == x)}x (forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL a -> b -> bk {VV : a | (VV == z)}z {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs) 272: foldrOL k z (Snoc xs x) = forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL a -> b -> bk (a -> b -> bk {VV : a | (VV == x)}x {VV : a | (VV == z)}z) {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs 273: foldrOL k z (Two b1 b2) = forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL a -> b -> bk (forall a b. (a -> b -> b) -> b -> (OrdList.OrdList a) -> bfoldrOL a -> b -> bk {VV : a | (VV == z)}z {x4 : (OrdList.OrdList a) | (x4 == b2) && ((olen x4) > 0) && ((olen x4) >= 0)}b2) {x4 : (OrdList.OrdList a) | (x4 == b1) && ((olen x4) > 0) && ((olen x4) >= 0)}b1 274: foldrOL k z (Many xs) = (a -> b -> b) -> b -> [a] -> bfoldr a -> b -> bk {VV : a | (VV == z)}z {x6 : [a] | (x6 == xs) && ((len x6) > 0) && ((len x6) >= 0) && ((olens x6) >= 0) && ((sumLens x6) >= 0)}xs 275: 276: foldlOL :: (b->a->b) -> b -> OrdList a -> b 277: forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL _ az None = {VV : a | (VV == z)}z 278: foldlOL k z (One x) = a -> b -> ak {VV : a | (VV == z)}z {VV : a | (VV == x)}x 279: foldlOL k z (Cons x xs) = forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL a -> b -> ak (a -> b -> ak {VV : a | (VV == z)}z {VV : a | (VV == x)}x) {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs 280: foldlOL k z (Snoc xs x) = a -> b -> ak (forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL a -> b -> ak {VV : a | (VV == z)}z {x3 : (OrdList.OrdList a) | (x3 == xs) && ((olen x3) >= 0)}xs) {VV : a | (VV == x)}x 281: foldlOL k z (Two b1 b2) = forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL a -> b -> ak (forall a b. (a -> b -> a) -> a -> (OrdList.OrdList b) -> afoldlOL a -> b -> ak {VV : a | (VV == z)}z {x4 : (OrdList.OrdList a) | (x4 == b1) && ((olen x4) > 0) && ((olen x4) >= 0)}b1) {x4 : (OrdList.OrdList a) | (x4 == b2) && ((olen x4) > 0) && ((olen x4) >= 0)}b2 282: foldlOL k z (Many xs) = (a -> b -> a) -> a -> [b] -> afoldl a -> b -> ak {VV : a | (VV == z)}z {x6 : [a] | (x6 == xs) && ((len x6) > 0) && ((len x6) >= 0) && ((olens x6) >= 0) && ((sumLens x6) >= 0)}xs
Concatenatation: Nested Measures
Now, the astute readers will have probably noticed that I’m missing
one function, concatOL, which glues a list of OrdLists into a
single long OrdList.
With LiquidHaskell we can give concatOL a super precise type, which
states that the size of the output list equals the sum-of-the-sizes
of the input OrdLists.
298: {-@ concatOL :: xs:[OrdList a] -> OrdListN a {(olens xs)} @-} 299: forall a. x1:[(OrdList.OrdList a)] -> {VV : (OrdList.OrdList a) | ((olen VV) == (olens x1))}concatOL [] = forall a. {x2 : (OrdList.OrdList a) | ((olen x2) == 0)}None 300: concatOL (ol:ols) = {x3 : (OrdList.OrdList a) | (x3 == ol) && ((olen x3) >= 0)}ol x1:(OrdList.OrdList a) -> x2:(OrdList.OrdList a) -> {x2 : (OrdList.OrdList a) | ((olen x2) == ((olen x1) + (olen x2)))}`appOL` forall a. x1:[(OrdList.OrdList a)] -> {VV : (OrdList.OrdList a) | ((olen VV) == (olens x1))}concatOL {x5 : [(OrdList.OrdList a)] | (x5 == ols) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}ols
The notion of sum-of-the-sizes of the input lists is specifed by the measure
306: {-@ measure olens :: [OrdList a] -> Int 307: olens ([]) = 0 308: olens (ol:ols) = (olen ol) + (olens ols) 309: @-} 310: 311: {-@ invariant {v:[OrdList a] | (olens v) >= 0} @-}
LiquidHaskell is happy to verify the above signature, again without requiring any explict proofs.
Conclusion
The above illustrates the flexibility provided by LiquidHaskell measures.
Instead of having to bake particular invariants into a datatype using indices or phantom types (as in the GADT approach), we are able to split our properties out into independent views of the datatype, yielding an approach that is more modular as
- we didn’t have to go back and change the definition of
[]to talk aboutOrdLists, - we didn’t have to provide explict non-emptiness witnesses,
- we obtained extra information about the behavior of API functions like
concatOL.
We can actually even verify the original definition of concatOL with a
clever use of abstract refinements, but we have to slightly change
the signature of foldr.
338: {- UGH CAN'T PARSE `GHC.Types.:`... foldr' :: forall <p :: [a] -> b -> Prop>. (xs:[a] -> x:a -> b<p xs> -> b<p (GHC.Types.: x xs)>) -> b<p GHC.Types.[]> -> ys:[a] -> b<p ys> @-} 345: forall a b. ({VV : [a] | ((len VV) >= 0)} -> a -> b -> b) -> b -> [a] -> bfoldr' {VV : [a] | ((len VV) >= 0)} -> a -> b -> bf az [] = {VV : a | (VV == z)}z 346: foldr' f z (x:xs) = {x2 : [a] | ((len x2) >= 0)} -> a -> b -> bf {x5 : [a] | (x5 == xs) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}xs {VV : a | (VV == x)}x (forall a b. ({VV : [a] | ((len VV) >= 0)} -> a -> b -> b) -> b -> [a] -> bfoldr' {x2 : [a] | ((len x2) >= 0)} -> a -> b -> bf {VV : a | (VV == z)}z {x5 : [a] | (x5 == xs) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}xs)
We’ve added a ghost parameter to the folding function, letting us
refer to the tail of the list at each folding step. This lets us
encode inductive reasoning in the type of foldr, specifically that
- given a base case
zthat satisfiesp [] - and a function that, given a value that satisfies
p xs, returns a value satisfyingp (x:xs) - the value returned by
foldr f z ysmust satisfyp ys!
LiquidHaskell can use this signature, instantiating p with \xs -> {v:OrdList a | (olen v) = (olens xs)} to prove the original
definition of concatOL!
363: {- concatOL' :: xs:[OrdList a] -> OrdListN a {(olens xs)} @-} 364: forall a. [(OrdList.OrdList a)] -> (OrdList.OrdList a)concatOL' [(OrdList.OrdList a)]aas = ([(OrdList.OrdList a)] -> (OrdList.OrdList a) -> (OrdList.OrdList a) -> (OrdList.OrdList a)) -> (OrdList.OrdList a) -> [(OrdList.OrdList a)] -> (OrdList.OrdList a)foldr' ((x5:(OrdList.OrdList a) -> x6:(OrdList.OrdList a) -> {x15 : (OrdList.OrdList a) | ((olen x15) == ((olen x5) + (olen x6))) && ((olen x15) == ((olen x6) + (olen x5)))}) -> [(OrdList.OrdList a)] -> x5:(OrdList.OrdList a) -> x6:(OrdList.OrdList a) -> {x15 : (OrdList.OrdList a) | ((olen x15) == ((olen x5) + (olen x6))) && ((olen x15) == ((olen x6) + (olen x5)))}const x1:(OrdList.OrdList a) -> x2:(OrdList.OrdList a) -> {x2 : (OrdList.OrdList a) | ((olen x2) == ((olen x1) + (olen x2)))}appOL) {x3 : (OrdList.OrdList {VV : a | false}) | ((olen x3) == 0) && ((olen x3) >= 0)}None {x5 : [(OrdList.OrdList a)] | (x5 == aas) && ((len x5) >= 0) && ((olens x5) >= 0) && ((sumLens x5) >= 0)}aas
We haven’t added the modified version of foldr to the LiquidHaskell
Prelude yet because it adds the ghost variable to the Haskell
type-signature.