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: [EMAIL PROTECTED]
Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
