Safely Catching A List By Its Tail

Posted by Ranjit Jhala Jan 31, 2013

Tags: measures

Previously we saw some examples of how refinements could be used to encode invariants about basic Int values. Today, let’s see how refinements allow us specify and verify structural invariants about recursive data types like lists. In particular, we will learn about at a new mechanism called a measure, use measures to describe the length of a list, and use the resulting refinement types to obtain compile-time assurances that canonical list manipulating operations like head, tail, foldl1 and (incomplete) pattern matches will not blow up at run-time.

26: module ListLengths where
27: 
28: import Prelude hiding (length, map, filter, head, tail, foldl1)
29: import Language.Haskell.Liquid.Prelude (liquidError)
30: import qualified Data.HashMap.Strict as M
31: import Data.Hashable

Measuring the Length of a List

To begin, we need some instrument by which to measure the length of a list. To this end, let’s introduce a new mechanism called measures which define auxiliary (or so-called ghost) properties of data values. These properties are useful for specification and verification, but don’t actually exist at run-time. That is, measures will appear in specifications but never inside code.

Let’s reuse this mechanism, this time, providing a definition for the measure 
48: measure len :: forall a. [a] -> GHC.Types.Int
49: len ([])     = 0
50: len (y:ys)   = 1 + (len ys)
The description of len above should be quite easy to follow. Underneath the covers, LiquidHaskell transforms the above description into refined versions of the types for the constructors (:) and [], Something like 
57: data [a] where 
58:   []  :: forall a. {v: [a] | (len v) = 0 }
59:   (:) :: forall a. y:a -> ys:[a] -> {v: [a] | (len v) = 1 + (len ys) }

To appreciate this, note that we can now check that

65: {-@ xs :: {v:[String] | (len v) = 1 } @-}
66: {VV : [[(GHC.Types.Char)]] | (len([VV]) = 1)}xs = {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"dog" y:{VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}
-> ys:[{VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}]
-> {VV : [{VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}] | (len([VV]) = (1 + len([ys])))}: {VV : [{VV : [{VV : (GHC.Types.Char) | false}] | false}] | (len([VV]) = 0),
                                                           (len([VV]) >= 0)}[]
67: 
68: {-@ ys :: {v:[String] | (len v) = 2 } @-}
69: {VV : [[(GHC.Types.Char)]] | (len([VV]) = 2)}ys = {VV : [{VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}] | (len([VV]) >= 0)}[{VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"cat", {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"dog"]
70: 
71: {-@ zs :: {v:[String] | (len v) = 3 } @-}
72: {VV : [[(GHC.Types.Char)]] | (len([VV]) = 3)}zs = {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"hippo" y:[(GHC.Types.Char)]
-> ys:[[(GHC.Types.Char)]]
-> {VV : [[(GHC.Types.Char)]] | (len([VV]) = (1 + len([ys])))}: {VV : [[(GHC.Types.Char)]] | (VV = ys),
                             (len([VV]) = 2),
                             (len([VV]) >= 0)}ys

Dually, when we de-construct the lists, LiquidHaskell is able to relate the type of the outer list with its constituents. For example,

79: {-@ zs' :: {v:[String] | (len v) = 2 } @-}
80: {VV : [[(GHC.Types.Char)]] | (len([VV]) = 2)}zs' = case {VV : [[(GHC.Types.Char)]] | (VV = zs),
                             (len([VV]) = 3),
                             (len([VV]) >= 0)}zs of 
81:         h : t -> {VV : [[(GHC.Types.Char)]] | (VV = t),(len([VV]) >= 0)}t

Here, from the use of the : in the pattern, LiquidHaskell can determine that (len zs) = 1 + (len t); by combining this fact with the nugget that (len zs) = 3 LiquidHaskell concludes that t, and hence, zs' contains two elements.

Reasoning about Lengths

Let’s flex our new vocabulary by uttering types that describe the behavior of the usual list functions.

First up: a version of the standard length function, slightly simplified for exposition.

99: {-@ length :: xs:[a] -> {v: Int | v = (len xs)} @-}
100: length :: [a] -> Int
101: xs:[a] -> {VV : (GHC.Types.Int) | (VV = len([xs]))}length []     = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0
102: length (x:xs) = {VV : (GHC.Types.Int) | (VV = (1  :  int))}1 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}+ xs:[a] -> {VV : (GHC.Types.Int) | (VV = len([xs]))}length {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs

Note: Recall that measure values don’t actually exist at run-time. However, functions like length are useful in that they allow us to effectively pull or materialize the ghost values from the refinement world into the actual code world (since the value returned by length is logically equal to the len of the input list.)

Similarly, we can speak and have confirmed, the types for the usual list-manipulators like

115: {-@ map      :: (a -> b) -> xs:[a] -> {v:[b] | (len v) = (len xs)} @-}
116: (a -> b)
-> x1:[a] -> {VV : [b] | (len([VV]) = len([x1])),(len([VV]) >= 0)}map _ []     = {VV : [{VV : a | false}] | (len([VV]) = 0)}[] 
117: map f (x:xs) = (a -> bf {VV : a | (VV = x)}x) y:a -> ys:[a] -> {VV : [a] | (len([VV]) = (1 + len([ys])))}: ((a -> b)
-> x1:[a] -> {VV : [b] | (len([VV]) = len([x1])),(len([VV]) >= 0)}map a -> bf {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs)

and

123: {-@ filter :: (a -> Bool) -> xs:[a] -> {v:[a] | (len v) <= (len xs)} @-}
124: (a -> (GHC.Types.Bool))
-> x1:[a] -> {VV : [a] | (len([VV]) >= 0),(len([VV]) <= len([x1]))}filter _ []     = {VV : [{VV : a | false}] | (len([VV]) = 0)}[]
125: filter f (x:xs) 
126:   | a -> (GHC.Types.Bool)f {VV : a | (VV = x)}x         = {VV : a | (VV = x)}x y:a -> ys:[a] -> {VV : [a] | (len([VV]) = (1 + len([ys])))}: (a -> (GHC.Types.Bool))
-> x1:[a] -> {VV : [a] | (len([VV]) >= 0),(len([VV]) <= len([x1]))}filter a -> (GHC.Types.Bool)f {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs
127:   | otherwise   = (a -> (GHC.Types.Bool))
-> x1:[a] -> {VV : [a] | (len([VV]) >= 0),(len([VV]) <= len([x1]))}filter a -> (GHC.Types.Bool)f {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs

and, since doubtless you are wondering,

133: {-@ append :: xs:[a] -> ys:[a] -> {v:[a] | (len v) = (len xs) + (len ys)} @-}
134: x4:[a]
-> x3:[a]
-> {VV : [a] | (len([VV]) = (len([x4]) + len([x3]))),
               (len([VV]) = (len([x3]) + len([x4]))),
               (len([VV]) >= 0)}append [] [a]ys     = {VV : [a] | (VV = ys),(len([VV]) >= 0)}ys 
135: append (x:xs) ys = {VV : a | (VV = x)}x y:a -> ys:[a] -> {VV : [a] | (len([VV]) = (1 + len([ys])))}: x4:[a]
-> x3:[a]
-> {VV : [a] | (len([VV]) = (len([x4]) + len([x3]))),
               (len([VV]) = (len([x3]) + len([x4]))),
               (len([VV]) >= 0)}append {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs {VV : [a] | (VV = ys),(len([VV]) >= 0)}ys

We will return to the above at some later date. Right now, let’s look at some interesting programs that LiquidHaskell can prove safe, by reasoning about the size of various lists.

Example 1: Safely Catching A List by Its Tail (or Head)

Now, let’s see how we can use these new incantations to banish, forever, certain irritating kinds of errors. Recall how we always summon functions like head and tail with a degree of trepidation, unsure whether the arguments are empty, which will awaken certain beasts 
150: Prelude> head []
151: *** Exception: Prelude.head: empty list

LiquidHaskell allows us to use these functions with confidence and surety! First off, let’s define a predicate alias that describes non-empty lists:

159: {-@ predicate NonNull X = ((len X) > 0) @-}

Now, we can type the potentially dangerous head as:

165: {-@ head   :: {v:[a] | (NonNull v)} -> a @-}
166: {VV : [a] | (len([VV]) > 0)} -> ahead (x:_) = {VV : a | (VV = x)}x
167: head []    = {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}liquidError {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"Fear not! 'twill ne'er come to pass"

As with the case of divide-by-zero, LiquidHaskell deduces that the second equation is dead code since the precondition (input) type states that the length of the input is strictly positive, which precludes the case where the parameter is [].

Similarly, we can write

178: {-@ tail :: {v:[a] | (NonNull v)} -> [a] @-}
179: {VV : [a] | (len([VV]) > 0)} -> [a]tail (_:xs) = {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs
180: tail []     = {VV : [(GHC.Types.Char)] | false}
-> {VV : [{VV : a | false}] | false}liquidError {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"Relaxeth! this too shall ne'er be"

Once again, LiquidHaskell will use the precondition to verify that the liquidError is never invoked.

Let’s use the above to write a function that eliminates stuttering, that is which converts "ssstringssss liiiiiike thisss" to "strings like this".

190: {-@ eliminateStutter :: (Eq a) => [a] -> [a] @-}
191: (GHC.Classes.Eq a) -> [a] -> [a]eliminateStutter [a]xs = ({VV : [a] | (len([VV]) > 0)} -> a)
-> xs:[{VV : [a] | (len([VV]) > 0)}]
-> {VV : [a] | (len([VV]) = len([xs]))}map {VV : [a] | (len([VV]) > 0)} -> ahead ({VV : [{VV : [a] | (len([VV]) > 0)}] | ((len([xs]) > 0) => (len([VV]) > 0)),
                                        (len([VV]) >= 0)}
 -> {VV : [a] | (len([VV]) >= 0)})
-> {VV : [{VV : [a] | (len([VV]) > 0)}] | ((len([xs]) > 0) => (len([VV]) > 0)),
                                          (len([VV]) >= 0)}
-> {VV : [a] | (len([VV]) >= 0)}$ x1:{VV : [a] | (len([VV]) >= 0)}
-> {VV : [{VV : [a] | (len([VV]) > 0)}] | ((len([x1]) > 0) => (len([VV]) > 0)),
                                          (len([VV]) >= 0)}groupEq {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs

The heavy lifting is done by groupEq

197: x1:{VV : [a] | (len([VV]) >= 0)}
-> {VV : [{VV : [a] | (len([VV]) > 0)}] | ((len([x1]) > 0) => (len([VV]) > 0)),
                                          (len([VV]) >= 0)}groupEq []     = {VV : [{VV : [{VV : a | false}] | false}] | (len([VV]) = 0)}[]
198: groupEq (x:xs) = ({VV : a | (VV = x)}xy:a -> ys:[a] -> {VV : [a] | (len([VV]) = (1 + len([ys])))}:{VV : [a] | (VV = ys),
            (VV = ys),
            (len([VV]) = len([ys])),
            (len([VV]) >= 0),
            (len([VV]) <= len([ys]))}ys) y:{VV : [a] | (len([VV]) > 0)}
-> ys:[{VV : [a] | (len([VV]) > 0)}]
-> {VV : [{VV : [a] | (len([VV]) > 0)}] | (len([VV]) = (1 + len([ys])))}: x1:{VV : [a] | (len([VV]) >= 0)}
-> {VV : [{VV : [a] | (len([VV]) > 0)}] | ((len([x1]) > 0) => (len([VV]) > 0)),
                                          (len([VV]) >= 0)}groupEq {VV : [a] | (VV = zs),
            (VV = zs),
            (len([VV]) = len([zs])),
            (len([VV]) >= 0),
            (len([VV]) <= len([zs]))}zs
199:                  where ({VV : [a] | (VV = ys),
            (len([VV]) = len([ys])),
            (len([VV]) >= 0),
            (len([VV]) <= len([ys]))}ys,{VV : [a] | (VV = zs),
            (len([VV]) = len([zs])),
            (len([VV]) >= 0),
            (len([VV]) <= len([zs]))}zs) = (a -> (GHC.Types.Bool)) -> [a] -> ([a] , [a])span ({VV : a | (VV = x)}x x:a
-> y:a -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x = y))}==) {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs

which gathers consecutive equal elements in the list into a single list. By using the fact that each element in the output returned by groupEq is in fact of the form x:ys, LiquidHaskell infers that groupEq returns a list of non-empty lists. (Hover over the groupEq identifier in the code above to see this.) Next, by automatically instantiating the type parameter for the map in eliminateStutter to (len v) > 0 LiquidHaskell deduces head is only called on non-empty lists, thereby verifying the safety of eliminateStutter. (Hover your mouse over map above to see the instantiated type for it!)

Example 2: Risers

The above examples of head and tail are simple, but non-empty lists pop up in many places, and it is rather convenient to have the type system track non-emptiness without having to make up special types. Let’s look at a more interesting example, popularized by Neil Mitchell which is a key step in an efficient sorting procedure, which we may return to in the future when we discuss sorting algorithms.

224: risers           :: (Ord a) => [a] -> [[a]]
225: (GHC.Classes.Ord a)
-> zs:[a] -> {VV : [[a]] | ((len([zs]) > 0) => (len([VV]) > 0))}risers []        = {VV : [{VV : [{VV : a | false}] | false}] | (len([VV]) = 0)}[]
226: risers [x]       = {VV : [{VV : [{VV : a | false}] | false}] | (len([VV]) = 0),
                                            (len([VV]) >= 0)}[{VV : [{VV : a | (VV = x)}] | (len([VV]) >= 0)}[{VV : a | (VV = x)}x]]
227: risers (x:y:etc) = {VV : [{VV : a | false}] | (len([VV]) = 0),(len([VV]) >= 0)}if {VV : a | (VV = x)}x x:a
-> y:a -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : a | (VV = y)}y then ({VV : a | (VV = x)}xy:a -> ys:[a] -> {VV : [a] | (len([VV]) = (1 + len([ys])))}:{VV : [a] | (VV = s),
            (VV = s),
            (len([VV]) = len([s])),
            (len([VV]) >= 0),
            (len([VV]) <= len([s]))}s)y:[a] -> ys:[[a]] -> {VV : [[a]] | (len([VV]) = (1 + len([ys])))}:{VV : [[a]] | (VV = ss),
              (VV = ss),
              (len([VV]) = len([ss])),
              (len([VV]) >= 0),
              (len([VV]) <= len([ss]))}ss else {VV : [{VV : a | (VV = x),(VV > y)}] | (len([VV]) >= 0)}[{VV : a | (VV = x)}x]y:[a] -> ys:[[a]] -> {VV : [[a]] | (len([VV]) = (1 + len([ys])))}:({VV : [a] | (VV = s),
            (VV = s),
            (len([VV]) = len([s])),
            (len([VV]) >= 0),
            (len([VV]) <= len([s]))}sy:[a] -> ys:[[a]] -> {VV : [[a]] | (len([VV]) = (1 + len([ys])))}:{VV : [[a]] | (VV = ss),
              (VV = ss),
              (len([VV]) = len([ss])),
              (len([VV]) >= 0),
              (len([VV]) <= len([ss]))}ss)
228:     where 
229:       ({VV : [a] | (VV = s),
            (len([VV]) = len([s])),
            (len([VV]) >= 0),
            (len([VV]) <= len([s]))}s, {VV : [[a]] | (VV = ss),
              (len([VV]) = len([ss])),
              (len([VV]) >= 0),
              (len([VV]) <= len([ss]))}ss)    = {VV : [[a]] | (len([VV]) > 0)}
-> ([a] , {VV : [[a]] | (len([VV]) >= 0)})safeSplit ({VV : [[a]] | ((len([etc]) > 0) => (len([VV]) > 0)),
               (len([VV]) > 0)}
 -> ([a] , {VV : [[a]] | (len([VV]) >= 0)}))
-> {VV : [[a]] | ((len([etc]) > 0) => (len([VV]) > 0)),
                 (len([VV]) > 0)}
-> ([a] , {VV : [[a]] | (len([VV]) >= 0)})$ zs:[a] -> {VV : [[a]] | ((len([zs]) > 0) => (len([VV]) > 0))}risers ({VV : a | (VV = y)}yy:a -> ys:[a] -> {VV : [a] | (len([VV]) = (1 + len([ys])))}:{VV : [a] | (VV = etc),(len([VV]) >= 0)}etc)

The bit that should cause some worry is safeSplit which simply returns the head and tail of its input, if they exist, and otherwise, crashes and burns

237: {VV : [a] | (len([VV]) > 0)} -> (a , {VV : [a] | (len([VV]) >= 0)})safeSplit (x:xs)  = x1:a -> b -> (a , b)({VV : a | (VV = x)}x, {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs)
238: safeSplit _       = {VV : [(GHC.Types.Char)] | false}
-> {VV : ({VV : a | false} , {VV : [{VV : a | false}] | false}) | false}liquidError {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"don't worry, be happy"

How can we verify that safeSplit will not crash ?

The matter is complicated by the fact that since risers does sometimes return an empty list, we cannot blithely specify that its output type has a NonNull refinement.

Once again, logic rides to our rescue!

The crucial property upon which the safety of risers rests is that when the input list is non-empty, the output list returned by risers is also non-empty. It is quite easy to clue LiquidHaskell in on this, namely through a type specification:

255: {-@ risers :: (Ord a) 
256:            => zs:[a] 
257:            -> {v: [[a]] | ((NonNull zs) => (NonNull v)) } @-}

Note how we relate the output’s non-emptiness to the input’s non-emptiness,through the (dependent) refinement type. With this specification in place, LiquidHaskell is pleased to verify risers (i.e. the call to safeSplit).

Example 3: MapReduce

Here’s a longer example that illustrates this: a toy map-reduce implementation.

First, let’s write a function keyMap that expands a list of inputs into a list of key-value pairs:

274: keyMap :: (a -> [(k, v)]) -> [a] -> [(k, v)]
275: (a -> {VV : [(b , c)] | (len([VV]) >= 0)}) -> [a] -> [(b , c)]keyMap a -> {VV : [(b , c)] | (len([VV]) >= 0)}f [a]xs = (a -> [(b , c)]) -> [a] -> [(b , c)]concatMap a -> {VV : [(b , c)] | (len([VV]) >= 0)}f {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs

Next, let’s write a function group that gathers the key-value pairs into a Map from keys to the lists of values with that same key.

282: (GHC.Classes.Eq a)
-> (Data.Hashable.Class.Hashable a)
-> [(a , b)]
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})group [(a , b)]kvs = ((a , b)
 -> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})
 -> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)}))
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})
-> [(a , b)]
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})foldr ((a , b)
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})\(k, v) (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})m -> a
-> b
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})inserts {VV : a | (VV = k)}k {VV : a | (VV = v)}v {VV : (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)}) | (VV = m)}m) (Data.HashMap.Base.HashMap {VV : a | false} {VV : [{VV : b | false}] | false})M.empty {VV : [(a , b)] | (VV = kvs),(len([VV]) >= 0)}kvs

The function inserts simply adds the new value v to the list of previously known values lookupDefault [] k m for the key k.

289: (GHC.Classes.Eq a)
-> (Data.Hashable.Class.Hashable a)
-> a
-> b
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})inserts ak av (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})m = a
-> {VV : [b] | (len([VV]) > 0)}
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})M.insert {VV : a | (VV = k)}k ({VV : a | (VV = v)}v y:a -> ys:[a] -> {VV : [a] | (len([VV]) = (1 + len([ys])))}: {VV : [a] | (VV = vs),(len([VV]) >= 0)}vs) {VV : (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)}) | (VV = m)}m 
290:   where {VV : [a] | (len([VV]) >= 0)}vs    = {VV : [a] | (len([VV]) >= 0)}
-> b
-> (Data.HashMap.Base.HashMap b {VV : [a] | (len([VV]) >= 0)})
-> {VV : [a] | (len([VV]) >= 0)}M.lookupDefault {VV : [{VV : a | false}] | (len([VV]) = 0),(len([VV]) >= 0)}[] {VV : a | (VV = k)}k {VV : (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)}) | (VV = m)}m

Finally, a function that reduces the list of values for a given key in the table to a single value:

297: reduce    :: (v -> v -> v) -> M.HashMap k [v] -> M.HashMap k v
298: (x2:a -> x3:a -> {VV : a | (VV > x2),(VV > x3)})
-> (Data.HashMap.Base.HashMap b {VV : [a] | (len([VV]) > 0)})
-> (Data.HashMap.Base.HashMap b a)reduce x1:a -> x2:a -> {VV : a | (VV > x1),(VV > x2)}op = ({VV : [a] | (len([VV]) > 0)} -> a)
-> (Data.HashMap.Base.HashMap b {VV : [a] | (len([VV]) > 0)})
-> (Data.HashMap.Base.HashMap b a)M.map ((a -> a -> a) -> {VV : [a] | (len([VV]) > 0)} -> afoldl1 x1:a -> x2:a -> {VV : a | (VV > x1),(VV > x2)}op)

where foldl1 is a left-fold over non-empty lists

304: {-@ foldl1      :: (a -> a -> a) -> {v:[a] | (NonNull v)} -> a @-}
305: (a -> a -> a) -> {VV : [a] | (len([VV]) > 0)} -> afoldl1 a -> a -> af (x:xs) =  (a -> a -> a) -> a -> [a] -> afoldl a -> a -> af {VV : a | (VV = x)}x {VV : [a] | (VV = xs),(len([VV]) >= 0)}xs
306: foldl1 _ []     =  {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}liquidError {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"will. never. happen."

We can put the whole thing together to write a (very) simple Map-Reduce library

312: mapReduce   :: (Eq k, Hashable k) 
313:             => (a -> [(k, v)])    -- ^ key-mapper
314:             -> (v -> v -> v)      -- ^ reduction operator
315:             -> [a]                -- ^ inputs
316:             -> [(k, v)]           -- ^ output key-values
317: 
318: (GHC.Classes.Eq a)
-> (Data.Hashable.Class.Hashable a)
-> (b -> {VV : [(a , c)] | (len([VV]) >= 0)})
-> (x7:c -> x8:c -> {VV : c | (VV > x7),(VV > x8)})
-> [b]
-> [(a , c)]mapReduce a -> {VV : [(b , c)] | (len([VV]) >= 0)}f x1:a -> x2:a -> {VV : a | (VV > x1),(VV > x2)}op  = (Data.HashMap.Base.HashMap a b) -> [(a , b)]M.toList 
319:                 ((Data.HashMap.Base.HashMap a b) -> [(a , b)])
-> ([c] -> (Data.HashMap.Base.HashMap a b)) -> [c] -> [(a , b)]. (x2:a -> x3:a -> {VV : a | (VV > x2),(VV > x3)})
-> (Data.HashMap.Base.HashMap b {VV : [a] | (len([VV]) > 0)})
-> (Data.HashMap.Base.HashMap b a)reduce x1:a -> x2:a -> {VV : a | (VV > x1),(VV > x2)}op 
320:                 ((Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})
 -> (Data.HashMap.Base.HashMap a b))
-> ([c]
    -> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)}))
-> [c]
-> (Data.HashMap.Base.HashMap a b). [(a , b)]
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)})group 
321:                 ([(a , b)]
 -> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)}))
-> ([c] -> [(a , b)])
-> [c]
-> (Data.HashMap.Base.HashMap a {VV : [b] | (len([VV]) > 0)}). (a -> {VV : [(b , c)] | (len([VV]) >= 0)}) -> [a] -> [(b , c)]keyMap a -> {VV : [(b , c)] | (len([VV]) >= 0)}f

Now, if we want to compute the frequency of Char in a given list of words, we can write:

327: {-@ charFrequency :: [String] -> [(Char, Int)] @-}
328: charFrequency     :: [String] -> [(Char, Int)]
329: [[(GHC.Types.Char)]] -> [((GHC.Types.Char) , (GHC.Types.Int))]charFrequency     = ([(GHC.Types.Char)]
 -> {VV : [((GHC.Types.Char) , {VV : (GHC.Types.Int) | (VV > 0)})] | (len([VV]) >= 0)})
-> (x8:{VV : (GHC.Types.Int) | (VV > 0)}
    -> x9:{VV : (GHC.Types.Int) | (VV > 0)}
    -> {VV : (GHC.Types.Int) | (VV > 0),(VV > x8),(VV > x9)})
-> [[(GHC.Types.Char)]]
-> [((GHC.Types.Char) , {VV : (GHC.Types.Int) | (VV > 0)})]mapReduce x1:[(GHC.Types.Char)]
-> {VV : [((GHC.Types.Char) , {VV : (GHC.Types.Int) | (VV = 1),
                                                      (VV = len([xs])),
                                                      (VV > 0)})] | (len([VV]) = len([x1])),
                                                                    (len([VV]) >= 0)}wordChars x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}(+)
330:   where x1:[a]
-> {VV : [(a , {VV : (GHC.Types.Int) | (VV = 1),
                                       (VV = len([xs])),
                                       (VV > 0)})] | (len([VV]) = len([x1])),(len([VV]) >= 0)}wordChars = (a
 -> (a , {VV : (GHC.Types.Int) | (VV = 1),
                                 (VV = len([xs])),
                                 (VV > 0)}))
-> xs:[a]
-> {VV : [(a , {VV : (GHC.Types.Int) | (VV = 1),
                                       (VV = len([xs])),
                                       (VV > 0)})] | (len([VV]) = len([xs]))}map (c:a
-> ({VV : a | (VV = c)} , {VV : (GHC.Types.Int) | (VV = 1),
                                                  (VV = len([xs])),
                                                  (VV > 0)})\ac -> x1:a -> b -> (a , b)({VV : a | (VV = c)}c, {VV : (GHC.Types.Int) | (VV = (1  :  int))}1))

You can take it out for a spin like so:

336: [((GHC.Types.Char) , (GHC.Types.Int))]f0 = [[(GHC.Types.Char)]] -> [((GHC.Types.Char) , (GHC.Types.Int))]charFrequency [ {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"the", {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"quick" , {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"brown"
337:                    , {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"fox", {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"jumped", {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"over"
338:                    , {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"the", {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"lazy"  , {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"cow"   ]

Look Ma! No Types: LiquidHaskell will gobble the whole thing up, and verify that none of the undesirable liquidError calls are triggered. By the way, notice that we didn’t write down any types for mapReduce and friends. The main invariant, from which safety follows is that the Map returned by the group function binds each key to a non-empty list of values. LiquidHaskell deduces this invariant by inferring suitable types for group, inserts, foldl1 and reduce, thereby relieving us of that tedium. In short, by riding on the broad and high shoulders of SMT and abstract interpretation, LiquidHaskell makes a little typing go a long way.

Conclusions

Well folks, thats all for now. I trust this article gave you a sense of

  1. How we can describe certain structural properties of data types, such as the length of a list,

  2. How we might use refinements over these properties to describe key invariants and establish, at compile-time, the safety of operations that might blow up on unexpected values at run-time, and perhaps, most importantly,

  3. How we can achieve the above, whilst just working with good old lists, without having to make up new types (which have the unfortunate effect of cluttering programs with their attendant new functions) in order to enforce special invariants.