TypeFamilies vs. FunctionalDependencies & type-level recursion

[Simon Peyton-Jones]

| GHC trac ticket on the feature, as you probably saw.  After a
| discussion with other people here at
| HacPhi, I've decided that what I'm going to attempt is to add
| type-level Maybes 

Hang on!  Julien Cretin (from INRIA) is doing an internship here at Cambridge with Dimitrios and me.  The primary goal is to support *typed* type-level programming; that is, to add a proper kind system to GHC.

Broadly our approach is like Conor's SHE system, with minor syntactic differences.  So type-level Maybes will appear automatically, as a special case, so it's probably a bit of a waste to implement them separately.  

There'll also be support for poly-kinded type-level functions, of course.

The stuff will be on a branch in the main ghc repo soon.

Julien: we should start a wiki page (see http://hackage.haskell.org/trac/ghc/wiki/Commentary, and look for the link to "Type level naturals"; one like that).  On the wiki you should 
 * add a link to the latest version of our (evolving) design document.
 * specify the branch in the repo that has the stuff
 * describe the status

Iavor's stuff is still highly relevant, because it involves a special-purpose constraint solver.  But Iavor's stuff is no integrated into HEAD, and we need to talk about how to do that, once you are back from holiday Iavor.

Simon