Letting the compiler do it for you

A while back I posted about how looking at the type can give you hints or even tell you what a function has to do, giving the simple example of function composition and pointing at a video by Matthew Brecknell showing how you can enlist ghci to help you in that respect.

Here's another example, provoked by a comment on a reddit question, namely map. If you only knew

map :: (a -> b) -> [a] -> [b]

could you write map? The signature says "give me a function that maps as to bs and a list of as, and I'll give you back a list of bs". Well, you could be a wise guy and write

map _ _ = []

and if anyone complained, say "Hey, the empty list is a list of bs", but in your heart you'd know you were cheating. The only way you're given to get a b given an a is to use the function, so the obvious thing to write is

map f xs = [f x | x <- xs]

(Yes, you could be a wise guy at the next level up and write

map f xs = reverse [f x | x <- xs]

but again, your conscience should bother you.)

Well, it turns out that at least sometimes, a compiler can do some of that kind of reasoning for you. Not in Haskell (though there's been a proposal), but in languages that support what are called "dependent types". Dependent types depend on a value; the canonical example is parametrizing lists by their length. That lets the language's type checker catch more errors.

"Hey, wait!" you say, "Does that mean I can't write my cool

fibs = 1 : 2 : (zipWith (+) fibs (tail fibs))

to neatly specify the Fibonacci sequence?" Alas, I suspect it does--after all, it doesn't have a finite length. There may be a way around that in this case, but the parametrization means you have to do calculations when type checking: "is this list empty?" "is this list at least as long as that list?" and in the general case, it can be undecidable.

All that said, it's still pretty darned impressive what can be done, and there's an excellent video from David Raymond Christiansen that shows it being done in the language Idris (which recently had a new version released). Check it out.