[Haskell-cafe] Type-Level Programming

[Gábor Lehel]

On Sat, Jun 26, 2010 at 3:49 AM, wren ng thornton <wren at freegeek.org> wrote:
> 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
>>> 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)?
>>
>> 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[1] extends Prolog with constraint
> programming. Mercury[2], lambda-Prolog[3], and Dyna give a more modern take
> on the paradigm.

It's interesting how C++ is imperative at the term level and
functional at the type level, while Haskell is functional at the term
level and similar to logic programming at the type level. Given
imperative, functional, and logic programming, that's nine possible
combinations of paradigms at the term and type level. How many of them
do we have examples for?

imperative/functional: C++
functional/logic: Haskell
functional/functional: Agda etc. (?)
imperative/imperative: Smalltalk/Ruby?


>
> If you're just a fan of logic variables and want something more
> Haskell-like, there is Curry[4]. In a similar vein there's also AliceML[5]
> which gives a nice futures/concurrency story to ML. AliceML started out on
> the same VM as Mozart/Oz[6], 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.
>
>
> [1] http://eclipse-clp.org/ is currently down, but can be accessed at
> http://87.230.22.228/
> [2] http://www.mercury.csse.unimelb.edu.au/
> [3] http://www.lix.polytechnique.fr/~dale/lProlog/
> [4] http://www-ps.informatik.uni-kiel.de/currywiki/
> [5] http://www.ps.uni-saarland.de/alice/
> [6] http://www.mozart-oz.org/
>
> --
> Live well,
> ~wren
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Work is punishment for failing to procrastinate effectively.