[Haskell-cafe] Type-Level Programming

[Gregory Crosswhite]

Are any of those compatible with Haskell, so that we could mix code in 
that language with Haskell code?

Cheers,
Greg

On 6/25/10 9:49 PM, wren ng thornton 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.
>
> 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/
>