Re: [Haskell-cafe] Re: Type-level arithmetic

15 Oct 2007


      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* mailto:chak@cse.unsw.edu.au> wrote:
Dan Piponi wrote,
     > On 10/12/07, Brandon S. Allbery KF8NH < allbery@ece.cmu.edu
    mailto:allbery@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