[Haskell-cafe] Type-Level Programming
wren ng thornton
wren at freegeek.org
Fri Jun 25 21:49:27 EDT 2010
Jason Dagit wrote:
> On Fri, Jun 25, 2010 at 2:26 PM, Walt Rorie-Baety <black.meph at gmail.com>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)?
> I'm not a prolog programmer, but I've heard that using type classes to do
> your computations leads to code that resembles prolog.
Indeed. If you like the look of Haskell's type-level programming, you
should look at logic programming languages based on Prolog. Datalog
gives a well understood fragment of Prolog. ECLiPSe extends Prolog
with constraint programming. Mercury, lambda-Prolog, and Dyna give
a more modern take on the paradigm.
If you're just a fan of logic variables and want something more
Haskell-like, there is Curry. In a similar vein there's also
AliceML which gives a nice futures/concurrency story to ML. AliceML
started out on the same VM as Mozart/Oz, which has similar futures,
though a different overall programming style.
And, as Jason said, if you're just interested in having the same
programming style at both term and type levels, then you should look
into dependently typed languages. Agda is the most Haskell-like, Epigram
draws heavily from the Haskell community, and Coq comes more from the ML
tradition. There's a menagerie of others too, once you start looking.
 http://eclipse-clp.org/ is currently down, but can be accessed at
More information about the Haskell-Cafe