Editing GHC/Typed holes (section)

== Notes on parametricity, free theorems and Agda ==

These examples hint at what people mean when they say they use the type system to drive development: it can help write your code, too!

This is of course very powerful for general, polymorphic types like above, because a polymorphic function may only be written so many ways. In fact, the above definition is the only legitimate <tt>Monad</tt> instance for <tt>Free</tt>!

A polymorphic type variable says what you cannot do to it: touch! You can't break the parametric nature of it by scrutinizing the variable in any way. A useful implementation of a polymorphic function has a small 'design space', naturally. It is not so, when defining monomorphic functions. A function like <tt>f :: Int -> Double</tt> could have many possible definitions, but we can always be sure for example, that <tt>f :: a -> a</tt> only has one valid definition, or that if <tt>f :: [a] -> [a]</tt>, then 'trivially' we can see that <tt>f [] = []</tt> must hold as a law.

This notion of "what information may be calculated based on the type" like we're doing here can be formalized to what we call 'Free Theorems', pioneered by Philip Wadler in his paper '[http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf Theorems for Free!]'

Free theorems fall out of the parametricity theorem (also called Reynolds' abstraction theorem,) which essentially states how polymorphic types relate to each other. Free theorems just state that, given a polymorphic type, it's possible to derive useful theorems and laws, based only on that type alone (so if <tt>f :: [a] -> [a]</tt> as we said earlier, then we get the free theorem <tt>f [] = []</tt> by definition - try writing that case another way! You can't!)

At this point, you're getting into much deeper territory, but I say all this because you have probably intuitively thought some of these things, when writing polymorphic functions yourself - that you must write them in such a way that the terms are all properly abstracted over correctly. This kind of design 'forces' only a few definitions to be possible.

Holes for GHC were inspired by the equivalent feature in its (twice removed) sister language, [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda]. Holes are considerably more powerful in Agda, mostly due to the fact it is total, the compiler infers less, and thus Agda programs are <i>rich</i> with evidence, giving witness to many facts the compiler can use. As a result, it can derive more code for you. In particular, Agda can literally <i>write</i> your code based on holes. It's able to do things like write case-analysis' for you, based only on type structure, and what's in scope, and discharge all the 'trivial' cases. You do this in emacs, in one or two keystrokes. It's essentially a semi-automated feedback loop for development, and it makes sense because the tool is really working with a meaningful model of your code, only in sensible ways that type-check. It's great.

There is not necessarily a reason why this could not exist for e.g. the Emacs mode for Haskell. Just because Haskell is not total, doesn't mean we couldn't calculate useful code based on the type - it is just much harder, especially considering the multitudes of features and extensions GHC supports.

* When I say 'legitimate' or 'useful', I mean, 'modulo divergent definitions.' Because Haskell is not total, it is possible to write divergent terms like <tt>let x = x in x</tt>, and the type of this expression is <tt>forall a. a</tt>, meaning I can prove <i>anything</i> with it. In the domain of Haskell semantics, this expression is in fact equivalent to <tt>undefined</tt> as well, because all bottoms are equal. I can prove that Blue is Green this way, or that Freedom is Slavery - I can inhabit any type, using these nonsensical terms. Logistically, you could say Haskell terms are complete, but not coherent/consistent. But divergent definitions here are not very legitimate, interesting, or useful, obviously, so ignore them (cue, [http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html "Fast and Loose reasoning is morally correct."])