The Advantage of Measures
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:
Many
should take a non-empty list,Two
takes two non-emptyOrdList
s.
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 OrdList
s.
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 declaration
110: {-@ 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 OrdList
s 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 OrdList
s¶
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 OrdList
s 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 OrdList
s 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
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 foldOL
s 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 OrdList
s 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 aboutOrdList
s, - we didn't have to provide explict non-emptiness witnesses,
- we obtained extra information about the behavior of API functions like
concatOL
.
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 1. given a base case `z` that satisfies `p []` 2. and a function that, given a value that satisfies `p xs`, returns a value satisfying `p (x:xs)` 3. the value returned by `foldr f z ys` must satisfy `p 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)}aasWe haven't added the modified version of `foldr` to the LiquidHaskell Prelude yet because it adds the ghost variable to the Haskell type-signature.