TypeFamilies vs. FunctionalDependencies & type-level recursion

Simon Peyton-Jones simonpj at microsoft.com
Tue Aug 2 17:10:09 CEST 2011

| 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.


More information about the Haskell-prime mailing list