GADTs and functional dependencies

Claus Reinke claus.reinke at talk21.com
Wed Sep 24 14:26:31 EDT 2008


>> This has never worked with fundeps, because it involves a *local* type equality (one that holds 
>> in some places and not others) and my implementation of fundeps is fundamentally based on 
>> *global* equality.  Prior to GADTs that was fine!

Actually, how does that relate to reasoning under assumptions?

    class FD a b | a -> b

    f :: (FD t1 t2, FD t1 t3) => ..
    f = ..

There is no instance of 'FD', so no equalities can be derived from there
outside of 'f', and no equalities should be derived globally from instances
that are only local hypotheses in 'f' . But inside 'f', we assume that those
two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of
the implication.

Isn't that decidedly local?
Claus




More information about the Glasgow-haskell-users mailing list