[Haskell-cafe] Type-Level Programming
byorgey at seas.upenn.edu
Mon Jun 28 05:19:20 EDT 2010
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
> 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  (which was until recently the only way to
Type-level programming using the newer type families  (which are
equivalent in power ) 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
, 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 . 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.
 Leaving out GHC's special ? and ?? kinds which aren't really of
interest to the type-level programmer.
More information about the Haskell-Cafe