How to write programs in two easy steps

I’m bored, so I’m browsing the blog-o-tubes, and noticing the occasional comment wondering why functional languages like Haskell and Lisp are typically used for no more than implementing other programming languages. I won’t comment on the truth or otherwise of this claim, because I don’t think it’s a bad thing in any case. Here’s why — this is a technique I learned from Conor McBride (who learned it from his father Fred McBride), explaining how to write any computer program in two easy stages:

Dependent Pattern Matching in Ivor

I’m working on Ivor, a theorem proving library for Haskell. It’s an implementation of dependent type theory which is embeddable in Haskell applications and easily extensible with domain specific tactics. You can read a paper explaining the motivation and design in more detail.

I’ve been using it for research into using dependent types for proving resource bounds of functional programs, and more generally for experiments with multi-stage programming with dependent types. However, I’ve found it frustratingly hard to implement interesting dependently typed programs, because of the lack of pattern matching, or an Epigram-like elimination with a motive tactic. Doing the latter by hand is, er, an interesting challenge up to a point, but gets tedious very quickly.

And so, over the last couple of days I’ve been adding dependent pattern matching. You can now do such things as bounds safe vector lookup functions as follows:

Data Nat:* = O:Nat | S:(k:Nat)Nat; -- Natural numbers

Data Fin:(n:Nat)*
  = fz:(k:Nat)Fin (S k)
  | fs:(k:Nat)(i:Fin k)(Fin (S k)); -- Bounded natural numbers

Data Vect (A:*) : (n:Nat)*
  = nil : Vect A O
  | cons : (k:Nat)(xs:Vect A k)(Vect A (S k)); -- Bounded vector

Match lookup : (A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A =
    lookup _ _ (fz _) (cons _ _ x xs) = x
  | lookup _ _ (fs n i) (cons _ n x xs) = lookup _ _ i xs;

Ivor checks that the patterns for lookup cover all possible cases (any other patterns would not be well-typed, in particular cases for vnil), and that recursive calls are well-founded.
It will, of course, only match on constructor patterns (you can’t do anything like Epigram’s views), and you can’t develop functions interactively (i.e. leave holes in terms to fill in later) but nevertheless it’s a big improvement on what was available before.

I really ought to write up the way the system works out which patterns are needed to guarantee all possibilities are covered; intuitively I’m sure it works but writing it up more formally may reveal a few holes. But it’s too late in the evening (um, early in the morning in fact) to do that just now…

I think it would be nice to deal with implicit arguments, so that you could write, e.g.:

Match lookup : (i:Fin n)(xs:Vect A n)A =
    lookup fz (cons x xs) = x
  | lookup (fs n i) (cons x xs) = lookup i xs;

Then it’s almost beginning to look like a proper programming language. However, I expect there are more important things to do first…

Error Handling in Haskell

I like to program in Haskell, and typically write theorem provers and compilers and that sort of thing. This typically involves processing of large data structures (syntax trees representing formulas or programs) which might fail at any point. So, usually, I run such functions inside a monad; forexample, part of a typechecker might look like:

typecheck :: Monad m => RawCode -> m (Expression, Type)
typecheck (RawApply f a) =
	do (fgood, ftype) <- typecheck f
	   (agood, atype) <- typecheck a
	   if (domain ftype == atype)
		then return (Apply f a, codomain ftype)
		else fail $ "Type error " ++ ftype ++ ", " ++ atype

This way, I can call typecheck recursively on f and a and let the machine deal with what happens if there’s an error, rather than endlessly nesting case expressions.

However, the fact that fail takes a String can be somewhat limiting. What if I want to handle the error in some appropriate way which relies on me knowing the structure of ftype, for example? Or there might be some specific kinds of error I can recover from that I want to handle specially (e.g. if name lookup fails, I might want to look in some other module). I might even just want to translate error messages into a number of languages. This is the sort of thing that exception handling systems in mainstream languages can do quite easily (define an exception which carries the relevant data), but in Haskell I have to make do with a String.

The Haskell library contains an Error type, which I think would handle this sort of situation. But I don’t really like gratuitous use of non-portable features like multi-parameter type classes — I prefer to look for a simpler solution first. I like to keep things simple, so that other people can understand my code fairly easily (Six months from now, I will be one of those other people myself anyway).

[Aside: yes, I do believe Dependent Types make things simpler all round. That's a topic for another day...]

So, anyway, now I do things like this:

data Possibly a b = Success b | Failure a
   deriving (Show, Eq, Ord)

failure :: a -> Possibly a b
failure x = Failure x

success :: b -> Possibly a b
success x = Success x

instance Monad (Possibly a) where
    (Success r) >>= k = k r
    (Failure err) >>= k = Failure err
    return = Success
    fail s = error $ "Possibly definitely broken: " ++ s

Yes, it’s just like Either (but is Either a a monad? Why not? It seems to obey the monad laws; perhaps there is something I’m missing…) I like my name better for reasons you’ll see from the type of the next function. Now I can write code just like before, letting the monad deal with failure, while having more expressive errors. e.g.

data Broken = TooBig Int | TooSmall Int

doThings :: Int -> Int -> Possibly Broken Int
doThings x y = do x <- check x
                  y <- check y
                  success (x+y)

check :: Int -> Possibly Broken Int
check x | x > 5 && x < 20 = success x
        | x < 6 = failure $ TooSmall x
        | x > 19 = failure $ TooBig x

And then the calling function can handle the error in some appropriate and informative way, e.g.:

run :: Int -> Int -> Int
run x y = case doThings x y of
            Success x -> x
            Failure (TooSmall x) ->
                error $ show x ++ " needs to be at least " ++
                         show (6-x) ++ " bigger"
            Failure (TooBig x) ->
                error $ show x ++ " needs to be at least " ++
                         show (x-19) ++ " smaller"

It seems nice and simple, and a neat way of dealing with errors more nicely in a large program, so there’s probably something deeply flawed with it. Please let me know…