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

[Tom Schrijvers]

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

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