[Haskell-cafe] Re: help with MPTC for type proofs?

[Tom Schrijvers]

> David Roundy wrote:
>> 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)
>
> The problem seems easily solvable, exactly as described. We need to
> take care of the two requirements separately.
>
>
>> {-# OPTIONS -fglasgow-exts #-}
>> {-# OPTIONS -fallow-undecidable-instances #-}
>>
>> module D1 where
>>
>> data Patch a b = Patch String deriving Show
>>
>> -- This is identical to what Tom Schrijvers wrote
>> class Commutable a b c d |
>>                 a b c -> d,     -- 2.
>>                 a d c -> b      -- based on 1. + 2.
>>
>> -- But how do we make sure that Commutable a d c b exists whenever
>> -- Commutable a b c d does? very easily: with the help of another
>> -- type class
>> instance (Commutable' a b c d, Commutable' a d c b)
>>     => Commutable a b c d

I had not thought of using a double constraint. Very clever.

Why not also put this constraint in the class declaration? You don't want 
any other instances of Commutable (or do you?):

  	class (Commutable' a b c d, Commutable' a d c b)
 		=> Commutable a b c d |
 	                 a b c -> d,     -- 2.
 	                 a d c -> b      -- based on 1. + 2.

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 at cs.kuleuven.be

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm