liquidhaskell-0.8.10.7: docs/blog/2014-08-15-a-finer-filter.lhs
---
layout: post
title: "A Finer Filter"
date: 2014-08-15 16:12
author: Ranjit Jhala
published: true
comments: true
external-url:
categories: abstract-refinements
demo: filter.hs
---
This morning, I came across this [nice post](https://twitter.com/ertesx/status/500034598042996736) which describes how one can write a very expressive type for
`filter` using [singletons](https://hackage.haskell.org/package/singletons).
Lets see how one might achieve this with [abstract refinements][absref].
<!-- more -->
<div class="hidden">
\begin{code}
{-@ LIQUID "--short-names" @-}
module Filter (filter) where
import Prelude hiding (filter)
import Data.Set (Set)
import Prelude hiding (filter)
isPos, isEven, isOdd :: Int -> Maybe Int
filter, filter3 :: (a -> Maybe a) -> [a] -> [a]
{-@ measure elts :: [a] -> (Set a)
elts ([]) = {v | Set_emp v }
elts (x:xs) = {v | v = Set_cup (Set_sng x) (elts xs) }
@-}
\end{code}
</div>
Goal
----
What we're after is a way to write a `filter` function such that:
\begin{code}
{-@ getPoss :: [Int] -> [Pos] @-}
getPoss = filter isPos
{-@ getEvens :: [Int] -> [Even] @-}
getEvens = filter isEven
{-@ getOdds :: [Int] -> [Odd] @-}
getOdds = filter isOdd
\end{code}
where `Pos`, `Even` and `Odd` are just subsets of `Int`:
\begin{code}
{-@ type Pos = {v:Int| 0 < v} @-}
{-@ type Even = {v:Int| v mod 2 == 0} @-}
{-@ type Odd = {v:Int| v mod 2 /= 0} @-}
\end{code}
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.
\begin{code}
filter1 :: (a -> Maybe b) -> [a] -> [b]
filter1 f [] = []
filter1 f (x:xs) = case f x of
Just y -> y : filter1 f xs
Nothing -> filter1 f xs
\end{code}
To complete the picture, we need just define the predicates as
functions returning a `Maybe`:
\begin{code}
{- isPos :: Int -> Maybe Pos @-}
isPos x
| x > 0 = Just x
| otherwise = Nothing
{- isEven :: Int -> Maybe Even @-}
isEven x
| x `mod` 2 == 0 = Just x
| otherwise = Nothing
{- isOdd :: Int -> Maybe Odd @-}
isOdd x
| x `mod` 2 /= 0 = Just x
| otherwise = Nothing
\end{code}
and now, we can achieve our goal!
\begin{code}
{-@ getPoss1 :: [Int] -> [Pos] @-}
getPoss1 = filter1 isPos
{-@ getEvens1 :: [Int] -> [Even] @-}
getEvens1 = filter1 isEven
{-@ getOdds1 :: [Int] -> [Odd] @-}
getOdds1 = filter1 isOdd
\end{code}
**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:
\begin{spec}
filter :: (a -> Bool) -> [a] -> [a]
\end{spec}
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
\begin{spec}
filter1 :: (a -> Maybe b) -> [a] -> [b]
\end{spec}
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?
\begin{code}
filter2 :: (a -> Maybe a) -> [a] -> [a]
filter2 f [] = []
filter2 f (x:xs) = case f x of
Just y -> y : filter2 f xs
Nothing -> filter2 f xs
\end{code}
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...
\begin{code}
{-@ getPoss2 :: [Int] -> [Pos] @-}
getPoss2 = filter2 isPos
{-@ getEvens2 :: [Int] -> [Even] @-}
getEvens2 = filter2 isEven
{-@ getOdds2 :: [Int] -> [Odd] @-}
getOdds2 = filter2 isOdd
\end{code}
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][absref] which
let us parameterize a signature over its refinements:
\begin{code}
{-@ filter3 :: forall a <p :: a -> Prop>.
(a -> Maybe a<p>) -> [a] -> [a<p>] @-}
filter3 f [] = []
filter3 f (x:xs) = case f x of
Just x' -> x' : filter3 f xs
Nothing -> filter3 f xs
\end{code}
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!
\begin{code}
{-@ getPoss3 :: [Int] -> [Pos] @-}
getPoss3 = filter3 isPos
{-@ getEvens3 :: [Int] -> [Even] @-}
getEvens3 = filter3 isEven
{-@ getOdds3 :: [Int] -> [Odd] @-}
getOdds3 = filter3 isOdd
\end{code}
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](http://www.reddit.com/r/haskell/comments/2dozs5/liquidhaskell_a_finer_filter/cjrrx3y)
graciously pointed out my folly: the signature for `filter3` makes no guarantees
about the subset property. In fact,
\begin{code}
doubles = filter3 (\x -> Just (x + x))
\end{code}
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.
\begin{code}
{-@ filter :: forall a <p :: a -> Prop>.
(x:a -> Maybe {v:a<p> | v = x})
-> xs:[a]
-> {v:[a<p>] | Set_sub (elts v) (elts xs)} @-}
filter f [] = []
filter f (x:xs) = case f x of
Just x' -> x' : filter f xs
Nothing -> filter f xs
\end{code}
where `elts` describes the [set of elements in a list][sets].
**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][racket]
or this lovely new [paper by Kaki and Jagannathan][catalyst] which
shows how refinements can be further generalized to make Boolean filters fine.
[sets]: /blog/2013/03/26/talking-about-sets.lhs/
[absref]: /blog/2013/06/03/abstracting-over-refinements.lhs/
[racket]: http://www.ccs.neu.edu/racket/pubs/popl08-thf.pdf
[catalyst]: http://gowthamk.github.io/docs/icfp77-kaki.pdf