Type is an extensible GADT

We can define new types in Haskell, so the kind of types is clearly extensible. Looking closer, it turns out that it is also oddly similar to a GADT. ¹

(Type is the better name for *. It can be imported from Data.Kind.)

Type is an ADT

Declaring a new type using the data or newtype keyword introduces a new type constructor². This suggests a view of Type as a “type”:

data Type
  = Int
  | Bool
  | Maybe Type
  | IO Type

  -- A couple of fancier types
  | Fix (Type -> Type)
  | ReaderT Type (Type -> Type) Type  -- transformers
  | HList [Type]                      -- (heterogeneous lists)
  | V Nat Type                        -- linear (fixed-length vectors)
  | Header' [Type] Symbol Type        -- servant

  ...  -- very open

Constructions can be destructed, this is true of both the term level and the type level. In particular, type families give us type-level pattern matching. One difference with pattern matching as we’re used to at the term level is that there is no way to handle every case individually. The upside is that clauses are defined independently. They can be in any order, or in different modules.

For example, the UnMTL type family below unfolds stacks of common monad transformers to equivalent but more basic types. (gist)

type family   UnMTL (a :: Type) :: Type
type instance UnMTL (ReaderT r m a) = r -> UnMTL (m a)
type instance UnMTL (StateT  s m a) = s -> UnMTL (m (a, s))
type instance UnMTL (ExceptT e m a) = UnMTL (m (Either e a))
type instance UnMTL (Identity a) = a
type instance UnMTL (IO a) = IO a

If a type family is applied to a type it can’t handle, nothing really happens, until the type checker tries to unify it with another type for example, causing an error at compile-time. (“Stuck” types don’t unify.)

ghci> :kind! UnMTL (StateT Int (Except String ()))
Int -> Either String (Int, ())
ghci> :kind! UnMTL Double  -- not a transformer stack
UnMTL Double               -- not an error

Type is an existential type

The main common point of Type with GADTs is that constructors can quantify variables that don’t appear in their result types, which are then said to be “existential types”.

Standard examples of polykinded type constructors:

data Proxy  :: forall   k.      k -> Type  -- Data.Proxy
data (:~:)  :: forall   k. k -> k -> Type  -- Data.Type.Equality
data (:~~:) :: forall j k. j -> k -> Type  -- idem

(We’ll keep the forall implicit from now on.)

We need the PolyKinds extension to quantify over kinds at all. But since there’s no place for type variables in Type, any polykinded type constructor makes Type an existential type.

data Type where
  Proxy  ::                  k -> Type
  (:~:)  ::             k -> k -> Type
  (:~~:) ::             j -> k -> Type
  Rec    :: (u -> Type) -> [u] -> Type  -- vinyl
  ...

A note about indexed types

GADTs are also a form of indexed types: types with parameters that may depend on the constructor.³ For example, singleton types are types indexed by values:

data SBool (_ :: Bool) where
  --        ^-------------------+- indices
  STrue  :: SBool 'True   -- <--|
  SFalse :: SBool 'False  -- <--/

Each constructor of SBool corresponds to one constructor for the index. SBool is a “singleton type” because for every index i :: Bool, there is exactly one value of type SBool i.

But Type has no index, why am I talking about indexed types? You’ve been tricked into reading so far, Type is not the most interesting GADT in this post!

To get there, we must take another small detour. An interesting feature of type families is that constructors don’t need to be fully applied to be matched. This is a notable difference between the kind-level (->) and the type-level (->).⁴

type family   IsOnlyJust (x :: a -> Maybe a) :: Bool
type instance IsOnlyJust 'Just = 'True

{- -- Term-level equivalent:
   case (x :: a -> Maybe a) of
     Just -> True
   -- !? -}

type family   IsOnlyMaybe (t :: Type -> Type) :: Bool
type instance IsOnlyMaybe Maybe = 'True
type instance IsOnlyMaybe IO    = 'False

Thus a type constructor, such as Maybe and IO, somehow also behaves like a constructor of Type -> Type. For the same reasons as given above for Type, Type -> Type is also GADT-like if we consider it as an atom:

data Type->Type where
  Maybe   ::                           Type->Type
  (,)     ::                  Type  -> Type->Type
  ReaderT :: Type -> (Type -> Type) -> Type->Type
  ...

More generally, the left hand side of an arrow can be different from Type, so this is a thing:

data (Type->Type)->Type where
  Fix, Mu, Nu ::             (Type->Type)->Type  -- recursion-schemes
  (:~>) :: (Type -> Type) -> (Type->Type)->Type  -- natural-transformation
  ...

_ -> Type is a GADT

Now consider the kind of unary type constructors, indexed by the kind of their single type parameter.

type TyCon k = k -> Type

Well, doesn’t this look like a fine GADT:

data TyCon k where
  IO      ::                        TyCon Type
  Fix     ::                        TyCon (TyCon Type)
  Proxy   ::                        TyCon k
  (:~:)   ::                   k -> TyCon k
  Const   ::                Type -> TyCon k
  Compose :: TyCon j -> (k -> j) -> TyCon k
  Product :: TyCon k -> TyCon k  -> TyCon k
  Rec     ::         (u -> Type) -> TyCon [u]
  ...

One application of this observation is to implement type functions in Haskell via typed defunctionalization (Defunctionalization for the win). It makes abstract sense because GADTs are great to embed typed languages in typed languages.

In fact, this post was split off from an upcoming one about defunctionalization.