Phantom Types and Generalized Algebraic Data Types


Phantom Types

A phantom type is a parameterized type in the left hand side type constructor which does not get used in the in the right hand side data constructor. The type has no values associated with it.

Length is a phantom type because a does not appear on the right hand side. It helps track a type.

Data Kinds

Generalized Algebraic Data Types

weak approximations of inductive families from dependently typed languages

A data constructor allows us to define a type constructor on the left hand side and a data (value) constructor on the right hand side. Generalized Algebraic Data Types (GADTs) allow us to explicitly write down the type signatures of data constructors. In GADTs, the return type of the data constructor does not have to match the type constructor.

We can expand on our example from above:

Here is another motivating example from the GHC Users Guide:

We can then pattern match on all of the constructors of Term.

GADTs allow type refinement. Type a is refined to Int in the case of the Lit constructor because of the signature in the GADT definition Lit :: Int -> Term Int.