LiquidHaskell

Tags: abstract-refinements

This morning, I came across this nice post which describes how one can write a very expressive type for filter using singletons.

Lets see how one might achieve this with abstract refinements.

23: 
24: {-@ LIQUID "--short-names" @-}
25: 
26: module Filter (filter) where
27: 
28: import Prelude hiding (filter)
29: import Data.Set (Set)
30: 
31: import Prelude hiding (filter)
32: isPos, isEven, isOdd :: Int -> Maybe Int
33: filter, filter3 :: (a -> Maybe a) -> [a] -> [a]
34: 
35: {-@ measure elts :: [a] -> (Set a) 
36:     elts ([])   = {v | Set_emp v }
37:     elts (x:xs) = {v | v = Set_cup (Set_sng x) (elts xs) }
38:   @-}
39:

Goal

What we’re after is a way to write a filter function such that:

50: {-@ getPoss  :: [Int] -> [Pos] @-}
51: x1:[{x7 : Int | false}]
-> {x2 : [{x7 : Int | false}] | ((Set_sub (elts x2) (elts x1)))}getPoss      = ({x10 : Int | false} -> (Maybe {x10 : Int | false}))
-> x3:[{x10 : Int | false}]
-> {x2 : [{x10 : Int | false}] | ((Set_sub (elts x2) (elts x3)))}filter x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && (x6 > 0) && (0 < x6)})isPos
52: 
53: {-@ getEvens :: [Int] -> [Even] @-}
54: x1:[{x7 : Int | false}]
-> {x2 : [{x7 : Int | false}] | ((Set_sub (elts x2) (elts x1)))}getEvens     = ({x10 : Int | false} -> (Maybe {x10 : Int | false}))
-> x3:[{x10 : Int | false}]
-> {x2 : [{x10 : Int | false}] | ((Set_sub (elts x2) (elts x3)))}filter x1:Int
-> (Maybe {x5 : Int | (x5 == x1) && (x5 == (x1  :  int)) && ((x5 mod 2) == 0)})isEven
55: 
56: {-@ getOdds  :: [Int] -> [Odd] @-}
57: x1:[{x7 : Int | false}]
-> {x2 : [{x7 : Int | false}] | ((Set_sub (elts x2) (elts x1)))}getOdds      = ({x10 : Int | false} -> (Maybe {x10 : Int | false}))
-> x3:[{x10 : Int | false}]
-> {x2 : [{x10 : Int | false}] | ((Set_sub (elts x2) (elts x3)))}filter x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && ((x6 mod 2) == 1) && (x6 /= 0)})isOdd

where Pos, Even and Odd are just subsets of Int:

63: {-@ type Pos  = {v:Int| 0 < v}        @-}
64: 
65: {-@ type Even = {v:Int| v mod 2 == 0} @-}
66: 
67: {-@ type Odd  = {v:Int| v mod 2 /= 0} @-}

Take 1: Map, maybe?

Bowing to the anti-boolean sentiment currently in the air, lets eschew the classical approach where the predicates (isPos etc.) return True or False and instead implement filter using a map.

78: filter1          :: (a -> Maybe b) -> [a] -> [b]
79: 
80: forall a b.
(a -> (Maybe b))
-> x3:[a] -> {VV : [b] | ((len VV) >= 0) && ((len VV) <= (len x3))}filter1 a -> (Maybe b)f []     = forall a <p :: a a -> Prop>.
{x5 : [a]<\x6 VV -> p x6> | (((null x5)) <=> true) && ((Set_emp (listElts x5))) && ((Set_emp (elts x5))) && ((len x5) == 0)}[]
81: filter1 f (x:xs) = case a -> (Maybe b)f {VV : a | (VV == x)}x of
82:                      Just y  -> {VV : a | (VV == y)}y x1:a
-> x2:[a]
-> {x5 : [a] | (((null x5)) <=> false) && ((listElts x5) == (Set_cup (Set_sng x1) (listElts x2))) && ((len x5) == (1 + (len x2))) && ((elts x5) == (Set_cup (Set_sng x1) (elts x2)))}: forall a b.
(a -> (Maybe b))
-> x3:[a] -> {VV : [b] | ((len VV) >= 0) && ((len VV) <= (len x3))}filter1 a -> (Maybe b)f {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs 
83:                      Nothing ->     forall a b.
(a -> (Maybe b))
-> x3:[a] -> {VV : [b] | ((len VV) >= 0) && ((len VV) <= (len x3))}filter1 a -> (Maybe b)f {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs

To complete the picture, we need just define the predicates as functions returning a Maybe:

90: {- isPos          :: Int -> Maybe Pos  @-}
91: x:Int
-> (Maybe {VV : Int | (VV == x) && (VV == (x  :  int)) && (VV > 0) && (0 < VV)})isPos Intx
92:   | {x2 : Int | (x2 == x)}x x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 > x2))}> {x2 : Int | (x2 == (0  :  int))}0          = x1:{x13 : Int | (x13 == x) && (x13 == (x  :  int)) && (x13 > 0) && (0 < x13)}
-> {x3 : (Maybe {x13 : Int | (x13 == x) && (x13 == (x  :  int)) && (x13 > 0) && (0 < x13)}) | (((isJust x3)) <=> true) && ((fromJust x3) == x1)}Just {x2 : Int | (x2 == x)}x
93:   | otherwise      = {x2 : (Maybe {x3 : Int | false}) | (((isJust x2)) <=> false)}Nothing
94: 
95: {- isEven         :: Int -> Maybe Even @-}
96: x:Int
-> (Maybe {VV : Int | (VV == x) && (VV == (x  :  int)) && ((VV mod 2) == 0)})isEven Intx
97:   | {x2 : Int | (x2 == x)}x x1:Int
-> x2:Int
-> {x6 : Int | (((0 <= x1) && (0 < x2)) => ((0 <= x6) && (x6 < x2))) && (x6 == (x1 mod x2))}`mod` {x2 : Int | (x2 == (2  :  int))}2 x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 == x2))}== {x2 : Int | (x2 == (0  :  int))}0 = x1:{x11 : Int | (x11 == x) && (x11 == (x  :  int)) && ((x11 mod 2) == 0)}
-> {x3 : (Maybe {x11 : Int | (x11 == x) && (x11 == (x  :  int)) && ((x11 mod 2) == 0)}) | (((isJust x3)) <=> true) && ((fromJust x3) == x1)}Just {x2 : Int | (x2 == x)}x
98:   | otherwise      = {x2 : (Maybe {x3 : Int | false}) | (((isJust x2)) <=> false)}Nothing
99: 
100: {- isOdd          :: Int -> Maybe Odd  @-}
101: x:Int
-> (Maybe {VV : Int | (VV == x) && (VV == (x  :  int)) && ((VV mod 2) == 1) && (VV /= 0)})isOdd Intx
102:   | {x2 : Int | (x2 == x)}x x1:Int
-> x2:Int
-> {x6 : Int | (((0 <= x1) && (0 < x2)) => ((0 <= x6) && (x6 < x2))) && (x6 == (x1 mod x2))}`mod` {x2 : Int | (x2 == (2  :  int))}2 x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 /= x2))}/= {x2 : Int | (x2 == (0  :  int))}0 = x1:{x13 : Int | (x13 == x) && (x13 == (x  :  int)) && ((x13 mod 2) == 1) && (x13 /= 0)}
-> {x3 : (Maybe {x13 : Int | (x13 == x) && (x13 == (x  :  int)) && ((x13 mod 2) == 1) && (x13 /= 0)}) | (((isJust x3)) <=> true) && ((fromJust x3) == x1)}Just {x2 : Int | (x2 == x)}x
103:   | otherwise      = {x2 : (Maybe {x3 : Int | false}) | (((isJust x2)) <=> false)}Nothing

and now, we can achieve our goal!

109: {-@ getPoss1 :: [Int] -> [Pos] @-}
110: [Int] -> [{v : Int | (0 < v)}]getPoss1     = (Int -> (Maybe {x14 : Int | (x14 > 0) && (0 < x14)}))
-> x3:[Int]
-> {x3 : [{x14 : Int | (x14 > 0) && (0 < x14)}] | ((len x3) >= 0) && ((len x3) <= (len x3))}filter1 x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && (x6 > 0) && (0 < x6)})isPos
111: 
112: {-@ getEvens1 :: [Int] -> [Even] @-}
113: [Int] -> [{v : Int | ((v mod 2) == 0)}]getEvens1    = (Int -> (Maybe {x12 : Int | ((x12 mod 2) == 0)}))
-> x3:[Int]
-> {x3 : [{x12 : Int | ((x12 mod 2) == 0)}] | ((len x3) >= 0) && ((len x3) <= (len x3))}filter1 x1:Int
-> (Maybe {x5 : Int | (x5 == x1) && (x5 == (x1  :  int)) && ((x5 mod 2) == 0)})isEven
114: 
115: {-@ getOdds1 :: [Int] -> [Odd] @-}
116: [Int] -> [{v : Int | ((v mod 2) == 1)}]getOdds1     = (Int -> (Maybe {x14 : Int | ((x14 mod 2) == 1) && (x14 /= 0)}))
-> x3:[Int]
-> {x3 : [{x14 : Int | ((x14 mod 2) == 1) && (x14 /= 0)}] | ((len x3) >= 0) && ((len x3) <= (len x3))}filter1 x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && ((x6 mod 2) == 1) && (x6 /= 0)})isOdd

The Subset Guarantee

Well that was easy! Or was it?

I fear we’ve cheated a little bit.

One of the nice things about the classical filter is that by eyeballing the signature:

129: filter :: (a -> Bool) -> [a] -> [a]

we are guaranteed, via parametricity, that the output list’s elements are a subset of the input list’s elements. The signature for our new-fangled

136: filter1 :: (a -> Maybe b) -> [a] -> [b]

yields no such guarantee!

In this case, things work out, because in each case, LiquidHaskell instantiates the type variables a and b in the signature of filter1 suitably:

In getPoss LH instantiates a := Int and b := Pos
In getEvens LH instantiates a := Int and b := Even
In getOdds LH instantiates a := Int and b := Odd

(Hover over the different instances of filter1 above to confirm this.)

But in general, we’d rather not lose the nice “subset” guarantee that the classical filter provides.

Take 2: One Type Variable

Easy enough! Why do we need two type variables anyway?

160: filter2          :: (a -> Maybe a) -> [a] -> [a]
161: 
162: forall a.
(x2:a -> (Maybe {VV : a | (VV == x2)}))
-> x3:[a]
-> {VV : [a] | ((Set_sub (elts VV) (elts x3))) && ((len VV) >= 0) && ((len VV) <= (len x3))}filter2 x1:a -> (Maybe {VV : a | (VV == x1)})f []     = forall a <p :: a a -> Prop>.
{x5 : [a]<\x6 VV -> p x6> | (((null x5)) <=> true) && ((Set_emp (listElts x5))) && ((Set_emp (elts x5))) && ((len x5) == 0)}[]
163: filter2 f (x:xs) = case x1:a -> (Maybe {VV : a | (VV == x1)})f {VV : a | (VV == x)}x of
164:                      Just y  -> {VV : a | (VV == y) && (VV == x)}y x1:a
-> x2:[a]
-> {x5 : [a] | (((null x5)) <=> false) && ((listElts x5) == (Set_cup (Set_sng x1) (listElts x2))) && ((len x5) == (1 + (len x2))) && ((elts x5) == (Set_cup (Set_sng x1) (elts x2)))}: forall a.
(x2:a -> (Maybe {VV : a | (VV == x2)}))
-> x3:[a]
-> {VV : [a] | ((Set_sub (elts VV) (elts x3))) && ((len VV) >= 0) && ((len VV) <= (len x3))}filter2 x1:a -> (Maybe {VV : a | (VV == x1)})f {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs 
165:                      Nothing ->     forall a.
(x2:a -> (Maybe {VV : a | (VV == x2)}))
-> x3:[a]
-> {VV : [a] | ((Set_sub (elts VV) (elts x3))) && ((len VV) >= 0) && ((len VV) <= (len x3))}filter2 x1:a -> (Maybe {VV : a | (VV == x1)})f {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs

There! Now the f is forced to take or leave its input x, and so we can breathe easy knowing that filter2 returns a subset of its inputs.

But…

175: {-@ getPoss2 :: [Int] -> [Pos] @-}
176: [Int] -> [{v : Int | (0 < v)}]getPoss2     = (x2:Int -> (Maybe {x13 : Int | (x13 == x2)}))
-> x3:[Int]
-> {x4 : [Int] | ((Set_sub (elts x4) (elts x3))) && ((len x4) >= 0) && ((len x4) <= (len x3))}filter2 x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && (x6 > 0) && (0 < x6)})isPos
177: 
178: {-@ getEvens2 :: [Int] -> [Even] @-}
179: [Int] -> [{v : Int | ((v mod 2) == 0)}]getEvens2    = (x2:Int -> (Maybe {x13 : Int | (x13 == x2)}))
-> x3:[Int]
-> {x4 : [Int] | ((Set_sub (elts x4) (elts x3))) && ((len x4) >= 0) && ((len x4) <= (len x3))}filter2 x1:Int
-> (Maybe {x5 : Int | (x5 == x1) && (x5 == (x1  :  int)) && ((x5 mod 2) == 0)})isEven
180: 
181: {-@ getOdds2 :: [Int] -> [Odd] @-}
182: [Int] -> [{v : Int | ((v mod 2) == 1)}]getOdds2     = (x2:Int -> (Maybe {x13 : Int | (x13 == x2)}))
-> x3:[Int]
-> {x4 : [Int] | ((Set_sub (elts x4) (elts x3))) && ((len x4) >= 0) && ((len x4) <= (len x3))}filter2 x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && ((x6 mod 2) == 1) && (x6 /= 0)})isOdd

Yikes, LH is not impressed – the red highlight indicates that LH is not convinced that the functions have the specified types.

Perhaps you know why already?

Since we used the same type variable a for both the input and output, LH must instantiate a with a type that matches both the input and output, i.e. is a super-type of both, which is simply Int in all the cases.

Consequently, we get the errors above – “expected Pos but got Int”.

Take 3: Add Abstract Refinement

What we need is a generic way of specifying that the output of the predicate is not just an a but an a that also enjoys whatever property we are filtering for.

This sounds like a job for abstract refinements which let us parameterize a signature over its refinements:

208: {-@ filter3      :: forall a <p :: a -> Prop>.
209:                       (a -> Maybe a<p>) -> [a] -> [a<p>] @-}
210: forall a <p :: a -> Prop>.
(a -> (Maybe {VV : a<p> | true})) -> [a] -> [{VV : a<p> | true}]filter3 a -> (Maybe {VV : a | ((papp1 p VV))})f []     = forall a <p :: a a -> Prop>.
{x5 : [a]<\x6 VV -> p x6> | (((null x5)) <=> true) && ((Set_emp (listElts x5))) && ((Set_emp (elts x5))) && ((len x5) == 0)}[]
211: filter3 f (x:xs) = case a -> (Maybe {VV : a | ((papp1 p VV))})f {VV : a | (VV == x)}x of
212:                      Just x'  -> {VV : a | ((papp1 p VV)) && (VV == x')}x' x1:{VV : a | ((papp1 p VV))}
-> x2:[{VV : a | ((papp1 p VV))}]<\_ VV -> ((papp1 p VV))>
-> {x5 : [{VV : a | ((papp1 p VV))}]<\_ VV -> ((papp1 p VV))> | (((null x5)) <=> false) && ((listElts x5) == (Set_cup (Set_sng x1) (listElts x2))) && ((len x5) == (1 + (len x2))) && ((elts x5) == (Set_cup (Set_sng x1) (elts x2)))}: forall a <p :: a -> Prop>.
(a -> (Maybe {VV : a<p> | true})) -> [a] -> [{VV : a<p> | true}]filter3 a -> (Maybe {VV : a | ((papp1 p VV))})f {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs 
213:                      Nothing ->       forall a <p :: a -> Prop>.
(a -> (Maybe {VV : a<p> | true})) -> [a] -> [{VV : a<p> | true}]filter3 a -> (Maybe {VV : a | ((papp1 p VV))})f {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs

Now, we’ve decoupled the filter-property from the type variable a.

The input still is a mere a, but the output is an a with bells on, specifically, which satisfies the (abstract) refinement p.

Voila!

224: {-@ getPoss3  :: [Int] -> [Pos] @-}
225: [Int] -> [{v : Int | (0 < v)}]getPoss3      = (Int -> (Maybe {x13 : Int | (x13 > 0) && (0 < x13)}))
-> [Int] -> [{x13 : Int | (x13 > 0) && (0 < x13)}]filter3 x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && (x6 > 0) && (0 < x6)})isPos
226: 
227: {-@ getEvens3 :: [Int] -> [Even] @-}
228: [Int] -> [{v : Int | ((v mod 2) == 0)}]getEvens3     = (Int -> (Maybe {x11 : Int | ((x11 mod 2) == 0)}))
-> [Int] -> [{x11 : Int | ((x11 mod 2) == 0)}]filter3 x1:Int
-> (Maybe {x5 : Int | (x5 == x1) && (x5 == (x1  :  int)) && ((x5 mod 2) == 0)})isEven
229: 
230: {-@ getOdds3  :: [Int] -> [Odd] @-}
231: [Int] -> [{v : Int | ((v mod 2) == 1)}]getOdds3      = (Int -> (Maybe {x13 : Int | ((x13 mod 2) == 1) && (x13 /= 0)}))
-> [Int] -> [{x13 : Int | ((x13 mod 2) == 1) && (x13 /= 0)}]filter3 x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && ((x6 mod 2) == 1) && (x6 /= 0)})isOdd

Now, LH happily accepts each of the above.

At each use of filter LH separately instantiates the a and the p. In each case, the a is just Int but the p is instantiated as:

In getPoss LH instantiates p := \v -> 0 <= v
In getEvens LH instantiates p := \v -> v mod 2 == 0
In getOdds LH instantiates p := \v -> v mod 2 /= 0

That is, in each case, LH instantiates p with the refinement that describes the output type we are looking for.

Edit: At this point, I was ready to go to bed, and so happily declared victory and turned in. The next morning, mypetclone graciously pointed out my folly: the signature for filter3 makes no guarantees about the subset property. In fact,

252: [Integer] -> [Integer]doubles = (Integer -> (Maybe Integer)) -> [Integer] -> [Integer]filter3 (Integer -> (Maybe Integer)\Integerx -> x1:Integer
-> {x3 : (Maybe Integer) | (((isJust x3)) <=> true) && ((fromJust x3) == x1)}Just ({x2 : Integer | (x2 == x)}x x1:Integer -> x2:Integer -> {x4 : Integer | (x4 == (x1 + x2))}+ {x2 : Integer | (x2 == x)}x))

typechecks just fine, while doubles clearly violates the subset property.

Take 4:

I suppose the moral is that it may be tricky – for me at least! – to read more into a type than what it actually says. Fortunately, with refinements, our types can say quite a lot.

In particular, lets make the subset property explicit, by

Requiring the predicate return its input (or nothing), and,
Ensuring the output is indeed a subset of the inputs.

270: {-@ filter      :: forall a <p :: a -> Prop>.
271:                        (x:a -> Maybe {v:a<p> | v = x})
272:                     -> xs:[a]
273:                     -> {v:[a<p>] | Set_sub (elts v) (elts xs)} @-}
274: 
275: forall a <p :: a -> Prop>.
(x2:a -> (Maybe {VV : a<p> | (VV == x2)}))
-> x3:[a]
-> {v : [{VV : a<p> | true}] | ((Set_sub (elts v) (elts x3)))}filter x1:a -> (Maybe {VV : a | ((papp1 p VV)) && (VV == x1)})f []     = forall a <p :: a a -> Prop>.
{x5 : [a]<\x6 VV -> p x6> | (((null x5)) <=> true) && ((Set_emp (listElts x5))) && ((Set_emp (elts x5))) && ((len x5) == 0)}[]
276: filter f (x:xs) = case x1:a -> (Maybe {VV : a | ((papp1 p VV)) && (VV == x1)})f {VV : a | (VV == x)}x of
277:                     Just x'  -> {VV : a | ((papp1 p VV)) && (VV == x) && (VV == x')}x' x1:{VV : a | ((papp1 p VV))}
-> x2:[{VV : a | ((papp1 p VV))}]<\_ VV -> ((papp1 p VV))>
-> {x5 : [{VV : a | ((papp1 p VV))}]<\_ VV -> ((papp1 p VV))> | (((null x5)) <=> false) && ((listElts x5) == (Set_cup (Set_sng x1) (listElts x2))) && ((len x5) == (1 + (len x2))) && ((elts x5) == (Set_cup (Set_sng x1) (elts x2)))}: forall a <p :: a -> Prop>.
(x2:a -> (Maybe {VV : a<p> | (VV == x2)}))
-> x3:[a]
-> {v : [{VV : a<p> | true}] | ((Set_sub (elts v) (elts x3)))}filter x1:a -> (Maybe {VV : a | ((papp1 p VV)) && (VV == x1)})f {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs 
278:                     Nothing ->       forall a <p :: a -> Prop>.
(x2:a -> (Maybe {VV : a<p> | (VV == x2)}))
-> x3:[a]
-> {v : [{VV : a<p> | true}] | ((Set_sub (elts v) (elts x3)))}filter x1:a -> (Maybe {VV : a | ((papp1 p VV)) && (VV == x1)})f {x3 : [a] | (x3 == xs) && ((len x3) >= 0)}xs

where elts describes the set of elements in a list.

Note: The implementation of each of the above filter functions are the same; they only differ in their type specification.

Conclusion

And so, using abstract refinements, we’ve written a filter whose signature guarantees:

The outputs must be a subset of the inputs, and
The outputs indeed satisfy the property being filtered for.

Another thing that I’ve learnt from this exercise, is that the old school Boolean approach has its merits. Take a look at the clever “latent predicates” technique of Tobin-Hochstadt and Felleisen or this lovely new paper by Kaki and Jagannathan which shows how refinements can be further generalized to make Boolean filters fine.