[Haskell-cafe] Re: help with MPTC for type proofs?
David Roundy
droundy at darcs.net
Sat May 27 06:36:06 EDT 2006
Can someone explain to me why this doesn't work?
> {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
> module MPTC where
>
> class C a b c d | a b c -> d, a d c -> b
>
> instance (C a b c d) => C a d c b
>
> data P a b = P deriving (Show)
>
> data CommuteResult a b c where
> CR :: C a b c d => (P a d, P d c) -> CommuteResult a b c
>
> commute :: (P a b, P b c) -> CommuteResult a b c
> commute (P, P) = CR (P, P)
>
> test (x,y) = do CR (y',x') <- return $ commute (x,y)
> CR (y'', x'') <- return $ commute (x,y)
> CR (x''',y''') <- return $ commute (y',x'')
> return ()
By my logic, it seems that if
x :: P a b
y :: P b c
then y' and x'' must have types
y' :: C a b c d => P a d
x'' :: C a b c e => P e c
but the functional dependencies of C tell us that e and d must be the same
type, so the code should typecheck (which it doesn't)!
I'm thinking that either the functional dependency constraint is weaker
than I thought, or that somehow GADTs aren't interacting with FDs as I'd
like, but I'm not sure which. Or, of course, it may be that my recursive
instance is not doing what I like. Or I may be just plain confused, as is
pretty clearly the case...
--
David Roundy
http://www.darcs.net
More information about the Haskell-Cafe
mailing list