Deducing code from types: filterM

The other day in #haskell a few people were trying to figure out how to generate the list of all sublists of a given list. Various people tried various kludgy things involving inits and tails and concatMap, none of which quite worked correctly, until:


13:26:10  > filterM (const [True,False]) "123"
13:26:11   ["123","12","13","1","23","2","3",""]
13:26:29  o_O

(lambdabot wasn’t working so Baughn had temporarily run another one under the nick Baughnie.) Anyway, this was sort of like that moment from Monty Python’s Holy Grail when the townspeople are trying to guess “what also floats in water”, and King Arthur suddenly says, “a duck”. To someone more well-versed in the ways of Haskell, Cale’s code is probably unremarkable; to me, it seemed like magic: although I’m quite comfortable with monads I had never seen filterM before, and had no idea how this worked (although clearly, it did). So, I looked up filterM using hoogle:

filterM :: Monad m => (a -> m Bool) -> [a] -> m [a]
--This generalizes the list-based filter function.

Here’s where I did something interesting, and I’m glad I did: instead of just clicking on “Source” to see the implementation, I decided to see if I could deduce the implementation of filterM, given only this information. I’d like to take you on a journey through my thought process: I learned a lot from this exercise and I think that anyone at about the same level of Haskell-fu as me (i.e. comfortable with the type system and monads, but still picking up idioms and bits and pieces of useful library functions, etc.) probably can too. Ready?

First, let’s recall the implementation of filter:

filter :: (a -> Bool) -> [a] -> [a]
filter _ []     = []
filter p (x:xs)
     | p x       = x : filter p xs
     | otherwise = filter p xs

Pretty straightforward: recursively take each element of the list, and prepend it to the result if and only if applying the predicate p to it returns True.

So now let’s write filterM. Note the type is almost the same as the type of filter, except that the predicate returns a Bool value inside a monad, and the resulting list is supposed to be inside the same monad. The first case is easy, and follows directly from the type:

filterM' p [] = return []

If the second argument (of type [a]) is an empty list, this is the only possible implementation (other than undefined): first of all, we know nothing about the type a, so there’s no way we can generate anything other than an empty list if we’re not given any values of type a in the first place; second, we want the result to be a list inside a monad, but we don’t know anything specific about the monad, so all we can do is return.

Now, for the recursive case. Since this is supposed to be similar to filter, we’ll first assume that we should do something with the first element, recurse on the rest, and combine them somehow. First things first:

filterM' p (x:xs) =
    let rest = filterM' p xs in ...

Of course, rest has type m [a]. OK, now what should we do with the first element, x? Let’s look at the types: x is of type a, and the other thing we have (p) is of type (a -> m Bool). It’s pretty obvious what we should do: apply p to a, and get something of type m Bool. Then we can pull out a Bool value using do-notation and call it b:

filterM' p (x:xs) =
    let rest = filterM' p xs in
      do b  p x ...

Now, what to do with b? Well, by analogy with filter, we should probably use it to decide whether to prepend x to rest! The only difference is that rest is of type m [a] so we can’t just prepend x like x : rest. We’ll have to use liftM to apply (x:) inside the monad:

filterM' p (x:xs) =
    let rest = filterM' p xs in
      do b  p x
         if b then liftM (x:) rest
              else            rest

And we’re done! Here’s the whole implementation, for reference:

import Control.Monad  -- for liftM

filterM' :: (Monad m) => (a -> m Bool) -> [a] -> m [a]
filterM' p [] = return []
filterM' p (x:xs) =
    let rest = filterM' p xs in
      do b  p x
         if b then liftM (x:) rest
              else            rest

Does it work?

*Main> filterM' (const [False,True]) [1,2,3]
[[],[3],[2],[2,3],[1],[1,3],[1,2],[1,2,3]]
*Main> filterM' (x -> if even x then Just True else Nothing) [2,4..8]
Just [2,4,6,8]
*Main> filterM' (x -> if even x then Just True else Nothing) [2,4,6,7,8]
Nothing

Sure seems to! A quick look at the actual library code shows that we did things a little differently, but filterM’ is essentially the same as filterM (I leave a formal proof as an exercise =). All with nothing more than the type and a vague statement of purpose! Of course, this is not the only implementation that fits the type — and I’m not just talking about things like filterM’ = undefined; there are other implementations whose most general type is the same as filterM. But it’s still amazing to me how much information is to be found just in types.

And now I understand how filterM (const [True,False]) works… do you? (Hint: how does (const [True,False]) match the type a -> m Bool? How does sequencing work in the list monad?)

About these ads
This entry was posted in haskell, learning. Bookmark the permalink.

2 Responses to Deducing code from types: filterM

  1. Ari Rahikkala says:

    Writing monadic versions of simple functions seems to be a skill that you learn pretty easily by simply doing it once. For instance, thanks to having written an unfoldM :: Monad m => (b -> m (Maybe (a, b))) -> b -> m [a] for my own use, it only took me a couple of minutes to write this in ghci:

    filterM p [] = return [];
    filterM p (x:xs) = do take

  2. Brent says:

    Unfortunately, it seems that WordPress really doesn’t like less-than signs in posts or comments. You can get around it if you use < but I realize that’s annoying.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s