[Haskell-cafe] help with MPTC for type proofs?
Tom Schrijvers
Tom.Schrijvers at cs.kuleuven.be
Fri May 26 09:55:46 EDT 2006
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
More information about the Haskell-Cafe
mailing list