[Haskell-cafe] Type-Level Programming

[Brent Yorgey]

On Fri, Jun 25, 2010 at 02:26:54PM -0700, Walt Rorie-Baety wrote:
> I've noticed over the - okay, over the months - that some folks enjoy the
> puzzle-like qualities of programming in the type system (poor Oleg, he's
> become #haskell's answer to the "Chuck Norris" meme commonly encountered in
> MMORPGs).
> 
> Anyway,... are there any languages out there whose term-level programming
> resembles Haskell type-level programming, and if so, would a deliberate
> effort to appeal to that resemblance be an advantage (leaving out for now
> the hair-pulling effort that such a change would entail)?

As several people have pointed out, type-level programming in Haskell
resembles logic programming a la Prolog -- however, this actually only
applies to type-level programming using multi-parameter type classes
with functional dependencies [1] (which was until recently the only way to
do it).

Type-level programming using the newer type families [2] (which are
equivalent in power [3]) actually lets you program in a functional
style, much more akin to defining value-level functions in Haskell.

However, all of this type-level programming is fairly *untyped* -- the
only kinds available are * and (k1 -> k2) where k1 and k2 are kinds
[4], so type-level programming essentially takes place in the simply
typed lambda calculus with only a single base type, except you can't
write explicit lambdas.

I'm currently working on a project with Simon Peyton-Jones, Dimitrios
Vytiniotis, Stephanie Weirich, and Steve Zdancewic on enabling *typed*
functional programming at the type level in GHC, very much inspired by
Conor McBride's SHE preprocessor [5].  I've got a blog post in the
works explaining our goals in much more detail, hopefully I'll be able
to get that up in the next day or two.

-Brent


[1] http://haskell.org/haskellwiki/Functional_dependencies
[2] http://haskell.org/haskellwiki/Type_families
[3] http://www.haskell.org/pipermail/haskell-cafe/2009-February/055890.html
[4] Leaving out GHC's special ? and ?? kinds which aren't really of
    interest to the type-level programmer.
[5] http://personal.cis.strath.ac.uk/~conor/pub/she/