On Thu, 25 May 2006, David Roundy wrote:
Hi all,
I've been thinking about extending some (experimental) GADT-based proof code that verifies that the darcs patch theory code is properly used. A given patch has type (Patch a b), and I'd like to be able to write something like
commute :: (Patch a b, Patch b c) -> (Patch a d, Patch d c)
in such a way that the type system know that the type d is one particular type, uniquely determined by the types a, b and c. Currently, which I do is to make d be existential with
data Pair a c where (:.) :: Patch a d -> Patch d c -> Pair a c
commute :: Pair a c -> Pair a c
which prevents misuse of the returned pair, but doesn't allow proper use, for example we ought to be able to compile:
test (a :. b) = do (b' :. a') <- return $ commute (a :. b) (b'' :. a'') <- return $ commute (a :. b) (a''' :. b''') <- return $ commute (b' :. a'') return ()
but this will fail, because the compiler doesn't know that b' and b'' have the same type.
So I'd like to write something like
class Commutable a b d c
commute :: Commutable a b d c => (Patch a b, Patch b c) -> (Patch a d, Patch d c)
But for this to work properly, I'd need to guarantee that
1. if (Commutable a b d c) then (Commutable a d b c)
2. for a given three types (a b c) there exists at most one type d such that (Commutable a b c d)
I have a feeling that these may be enforceable using fundeps (or associated types?), but have pretty much no idea to approach this problem, or even if it's soluble. Keep in mind that all these types (a, b, c and d) will be phantom types.
Hi David, I've quickly tried to a few alternatives in Hugs using FDs, but I've not been able to fully implement your requirement 1: 1) only FDs class Commutable a b c d | a b c -> d, -- 2. a d c -> b -- based on 1. + 2. but this does not enforce the existence of mirror instance Commutable a d c b. 2) FD + cyclic class hierarchy Alternatively, I wanted to write the following to capture 1.: class (Commutable a d c b) => -- 1. Commutable a b c d | a b c -> d, -- 2. but this is not accepted by Hugs (or GHC) because their type inference algorithms would go into a loop: Class hierarchy for "Commutable" is not acyclic Perhaps some cycle detection techniques would allow type inference to deal with this sort of code? 3) FDs + Overlapping instances class CommutativePartners b d => Commutable a b c d | a b c -> d -- b and d commute class Partners b d -- commutative closure of Partners class class CommutativePartners b d instance Partners b d => CommutativePartners b d instance Partners b d => CommutativePartners d b The last two instances are overlapping. GHC has a flag -fallow-overlapping-instances to allow this. This approach is not entirely safe if additional instances of CommutativePartners can be declared. Support for closed type classes is needed to prevent this. I'm not sure whether there is a way to fully realise requirement 1. AFAIK associated types are no more expressive than FDs. Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm