k.schupke at imperial.ac.uk
Tue Aug 16 15:17:30 EDT 2005
Attached are 3 Haskell modules used for type level programming. These
were developed as background work for the HList paper, but are not in
the final libraries as they are 'off topic' as it were. They were
however useful in testing type-level programming concepts.
Control.hs - This contains type level control structures like 'apply'
which is like Prolog's apply.
Logic.hs - This contains a Modal logic designed for type level computation:
data AllTrue = AllTrue
data SomeTrue = True | NotTrue
data SomeFalse = False | NotFalse
data AllFalse = AllFalse
Peano.hs - Contains type level numeric operators and constants, this is
the bit you are interested in, but its implementation depends on the
other modules... for example equality requires the type-level logic, and
division, foldN and reify require Control constructs to work.
run like this:
*Lib.TIR.Peano> :t three
three :: Three
*Lib.TIR.Peano> :t nine
nine :: Nine
*Lib.TIR.Peano> add three nine
*Lib.TIR.Peano> :t (add three nine)
(add three nine) :: Suc (Suc (Suc (Suc Eight)))
The general 'trick' if you will is to imlement each funtion as a type
class, pattern matching the
types to instances in a type-level analogue of the value level function.
Dirk Reckmann wrote:
>Am Dienstag, 16. August 2005 13:48 schrieb Keean Schupke:
>>Picked up on this late... I have working examples of add etc under
>>I can't remeber all the issues involved in getting it working, but I can
>>code for add if its any use?
>Yes, that would be nice. I'd like to see 'add' working... However, after each
>answer to my posting, I get more confused. Simon Peyton-Jones took all of my
>hope to get it working, because ghc doesn't like universal quantified but
>uniquely idetified types (at least, this is my understanding of his email).
>Now you have a working 'add' typelevel program. And the most confusing part
>for me is, that my fibonacci number program works, even though it makes use
>of the not working version of add.
>So, I'm really looking forward to your version!
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5442 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/glasgow-haskell-users/attachments/20050816/6f522b6e/tir.bin
More information about the Glasgow-haskell-users