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/