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 instantiatesa := Int
andb := Pos
- In
getEvens
LH instantiatesa := Int
andb := Even
- In
getOdds
LH instantiatesa := Int
andb := 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 instantiatesp := \v -> 0 <= v
- In
getEvens
LH instantiatesp := \v -> v mod 2 == 0
- In
getOdds
LH instantiatesp := \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.