Functional Dependencies

[Keean Schupke]

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
>  
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: tir.tgz
Type: application/x-compressed-tar
Size: 5442 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/glasgow-haskell-users/attachments/20050816/6f522b6e/tir.bin