David Roundy wrote:
data CommuteResult a b c where CR :: C a b c d => (P a d, P d c) -> CommuteResult a b c ... or that somehow GADTs aren't interacting with FDs as I'd like
It must be emphasized that there are *NO* GADTs is the above code. Except Stefan Monnier's message, no code posted in the thread `help with MPTC for type proofs?' had any GADTs, the notation |data ... where| notwithstanding. In particular, the data type |CommuteResult a b c| is the ordinary algebraic datatype, and can be written in the traditional notation as
data CommuteResult a b c = forall d. C a b c d => CR (P a d, P d c)
To recall, the datatype
data MEither a b where MLeft :: a -> MEither a b MRight :: b -> MEither a b
is the ordinary algebraic datatype
data MEither a b = MLeft a | MRight b
The two notations are totally equivalent. The constructors MLeft and MRight create the values of the type |MEither a b| -- which is just as general as the type being defined |MEither a b|. OTH,
data MEither2 a b where MLeft2 :: Int -> MEither2 Int b MRight2 :: b -> MEither2 Char b
is truly _generalized_ ADT, because the values created by the constructors MLeft2 and MRight2 have the types that span only the subset of the type family |MEither2 a b|. Thus, to tell if something written in the |data ... where| notation is GADT or not, we just look at the result type. If it is the same as what follows the |data| keyword, we have the ordinary ADT. Incidentally, I strongly prefer writing ordinary algebraic data types in the traditional notation (precisely to avoid the confusion with GADTs and to keep the code portable). Because David Roundy's example had no GADTs, it is not fair to blame GADT's interacting with FD. There are indeed issues, at present, with GADT and FD. But those issues do not bear on the problem at hand. Therefore, waiting for GHC 6.8 is, alas, hopeless in this respect. David Roundy wrote:
I want the return type "d" to be a phantom type of some sort (although I'm not clear on the distinction between phantom and existential types).
Well, they are, in a sense, dual to each other. In the declaration,
data Patch a b = P a
the type variable 'b' appears only on the left-hand side of the definition. The corresponding type is phantom. In the declaration
data PatchW a = forall b. PW (Patch a b)
the type variable 'b' appears only on the right-hand side of the defining equation. So, informally, the type |PatchW a| is existential, abstracting over |b|. Perhaps the |where| notation makes things clearer:
data Patch a b where P :: a -> Patch a b data PatchW a where PW :: Patch a b -> PatchW a
Here, the type variable |b| shows up only in the result of |P|. It is phantom. The type variable |b| shows up only in the argument of |PW|. It is existential. David Roundy wrote:
when I realized that the problem could be solved much more elegantly using GADTs as a type witness (with unsafeCoerce#, admittedly)
That is quite puzzling: the whole advantage of GADTs is that we don't need to coerce values because type coercion, after checking the run-time evidence (that is, successful pattern-match) is the very essence of GADTs. Incidentally, to coerce phantom types, there is no need to resort to unsafeCoerce#. The access to the data constructor suffices. David Roundy wrote:
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
When we abstract over |d|, there is generally no way to get the original type back (short of various casts, which generally require run-time evidence). One can think of it as upcast/downcast problem in OO: we can always pretend that an object of the type A is an object of a more general type ASuper (and any object is an object of the Top type). However, downcasting from a value of a more general type to the value of a more specific type requires some run-time evidence (even if the more general value was obtained by the upcast from the desired specific type). The nature of abstraction is to irreversibly forget -- hence the encapsulation guarantee. If that is not desired, we can use some other translucent, type-preserving, ways. For example,
{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-} module MPTC where
data P a b = P deriving (Show)
data CommuteResult a b c = forall d. CR (P a (d b), P (d b) c)
commute :: (P a (d b), P (d1 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 ()
which type-checks... David Roundy wrote:
I guess what hasn't been addressed is the question I didn't know to ask...
It would help me personally to see the `ideal' code -- the code that you wish to write and to typecheck. The code should be sufficiently realistic (the IO can be stubbed though). I'll be out of town for a week so unable to reply promptly.