On GADT, phantom types, etc. terminology

29 May 2006

      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.

oleg＠pobox.com

David Roundy

tags

participants (2)