Does the Either type constructor contain a phantom type each for the left/right case?

Admin 1
Viewed 178

AFAIK, only types are inhabited by values in Haskell, not type constructors. Either is a binary type constructor of kind * -> * -> *. Left and Right both apply this type constructor to a single type, which is provided by the passed value. Doesn't that mean that in both cases Either is merely partially applied and thus still a type constructor awaiting the missing type argument?

let x = Right 'x' -- Either a Char

x has the type Either a Char. I would assume that this type would have the kind * -> *. This is clearly a polymorphic type, not a ground one. Yet Either a Char can be inhabited by values like 'x'.

My suspicion is that the type variable a is a phantom type for the Right case resp. b for Left. I know phantom types in connection with Const, where the respective type variable isn't used at all. Am I on the right tack?

type-constructor higher-kinded-types polymorphism haskell
3 Answers

AFAIK, only types are inhabited by values in Haskell, not type constructors.

Spot on.

Left and Right both apply this type constructor to a single type

You can't say that. Left and Right don't live in the type language at all, so they don't apply anything to any types, they only apply themselves to values.

x has the type Either a Char. I would assume that this type would have the kind * -> *

You need to distinguish between function/constructor arguments, and type variables. It's basically the distinction between free and bound variables. Either a Char still has kind *, not * -> *, because it is already applied to a. Yes, that's a type variable, but it still is an argument that's already applied.

Yet Either a Char can be inhabited by values like 'x'.

Not quite – it can be inhabited by values like Right 'x'.

My suspicion is that the type variable a is a phantom type for the Right case resp. b for Left

kind of, but I wouldn't call it “phantom” because you can't just count out Left or Right. At least not unless you choose Either Void b, but in that case you don't have the a variable.

user_7459030

I would argue that a type variable is phantom if and only if the choice of the type variable does not restrict what values can be passed to the type's constructors. The important part is that this is a type-centric definition. It is determined by looking only at the type definition, not at some particular value of the type.

So does it matter that no value of type String appears in the value Left 5 :: Either Int String? Not at all. What matters is that the choice of String in Either Int String prevents Right () from type-checking.

user_3832000

Haskell has "implicit universal quantification", which means that type variables have an implicit forall. Either a Int is equivalent to forall a. Either a Int.

One way to consider a forall is that it's like a lambda, but for type variables. If we use the syntax @ for type application, then, you can "apply" a type to this and get a new type out.

let foo = Right 1 :: forall a. Either a Int
foo @Char   :: Either Char Int
foo @Double :: Either Double Int
user_37802030
Related