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: ghci Lib/TIR/Peano.hs *Lib.TIR.Peano> :t three three :: Three *Lib.TIR.Peano> :t nine nine :: Nine *Lib.TIR.Peano> add three nine 12 *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. Regards, Keean. Dirk Reckmann wrote:
Hello Keean!
Am Dienstag, 16. August 2005 13:48 schrieb Keean Schupke:
Picked up on this late... I have working examples of add etc under ghc/ghci... I can't remeber all the issues involved in getting it working, but I can post the 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!
Ciao, Dirk