[Haskell-cafe] Re: Type-level arithmetic

[Manuel M T Chakravarty]

Lennart Augustsson wrote,
> And Haskell embedded a logical programming language on accident.

Well, we are just trying to fix that :)

> On 10/15/07, *Manuel M T Chakravarty* <chak at cse.unsw.edu.au 
> <mailto:chak at cse.unsw.edu.au>> wrote:
> 
>     Dan Piponi wrote,
>      > On 10/12/07, Brandon S. Allbery KF8NH < allbery at ece.cmu.edu
>     <mailto:allbery at ece.cmu.edu>> wrote:
>      >
>      >> He wants to write entire programs in the type system,
>      >> something like the crazies who write programs in C++ templates such
>      >> that template expansion does all the work at compile time
>      >
>      > Crazies? :-)
>      > http://homepage.mac.com/sigfpe/Computing/peano.html
>      >
>      > Having switched from C++ to Haskell (at least in my spare time) I
>      > thought I'd escaped that kind of type hackery but it seems to be
>      > following me...
> 
>     The way I see, we are trying to come up with a clean way of
>     providing type-level computations (ie, we use and extend the
>     standard theory of HM type systems).  C++ embedded a functional
>     language in the type systems mostly by accident, whereas we do it on
>     purpose.
> 
>     Manuel