Phantom Type Definition - Cannot Compile Examples

Question

I am trying to learn more about Phantom types. I am trying to read Fun with Phantom types from Ralf Hinze. It uses the with keyword, which I have not seen before, and that I cannot compile it. I get a parsing error on = when I try to do this.

 data Type t = RInt with t = Int | RChar with t = Char | RList (Type a) with t = [a ] | RPair (Type a) (Type b) with t = (a, b) 

He said earlier in the document that the “c” instructions are not strictly necessary, you can set a = t instead, but I cannot figure out how to define this data type without them. The following errors: Not in scope: type variable 'a'

 data Type t = RInt | RChar | RList (Type a) | RPair (Type a) (Type b) 

What am I missing?

Answer 1

I assume that the definition of sans- with proposed in the article is

 data Type t = RInt | RChar | RList (Type t) | RPair (Type t) (Type t) 

Above, the parameter t never used. This is really a phantom.

This means, for example,

 RInt :: Type a 

for any type a . In contrast, if the with constraints were respected, it would be impossible to have RInt :: Type t for any t, but for t ~ Int .

The with syntax is missing in the GHC, but the GADTs play essentially the same role.

 {-# LANGUAGE GADTs #-} data Type t where RInt :: t ~ Int => Type t RChar :: t ~ Char => Type t RList :: t ~ [a] => Type a -> Type t RPair :: t ~ (a,b) => Type a -> Type b -> Type t 

Note that with is replaced by an equality constraint in each constructor. It is basically the same thing written in different ways.

More compactly, we can rewrite the above into

 data Type t where RInt :: Type Int RChar :: Type Char RList :: Type a -> Type [a] RPair :: Type a -> Type b -> Type (a,b) 

where the constraints were "embedded" in the final type.

Answer 2

Despite the ugliness, the following will work and can be considered a little closer to this notation in spirit. This essentially devalues ​​GADTs in types (which don't seem to have their own extension, so you need either GADTs or TypeFamilies to include them) and existential objects.

 {-# LANGUAGE ExistentialQuantification, TypeFamilies #-} data Type t = t ~ Int => RInt | t ~ Char => RChar | forall a. t ~ [a] => RList (Type a) | forall a b. t ~ (a, b) => RPair (Type a) (Type b)