# 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.

## 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.

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