A Finer Filter

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

1. Requiring the predicate return its input (or nothing), and,
2. 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.

Ranjit Jhala

2014-08-15 16:12

abstract-refinements