Shape of a type, possibly with type variables.

>>> :kind Kon [] :@: Var0 -- the type [a] for unknown a
Kon [] :@: Var0 :: Atom (* -> xs) *

Representation of type families

n + m         -- using (+) from GHC.TypeNats
~
Eval (n + m)  -- using Eval from Fcf.Core and (+) from Fcf.Data.Nat

Eval ((Kon (+) :@: Var0) :@: Var1)  -- Eval as Atom's constructor
  :: Atom (Nat -> Nat -> Type) Nat

n + m
~
Eval (NDFamily (MkName "base" "GHC.TypeNats" "+") P0 '(n, '(m, '())))

Eval (Kon (NDFamily (MkName "base" "GHC.TypeNats" "+") P0)
        :@: ((Kon '(,) :@: Var0) :@: ((Kon '(,) :@: Var1) :@: Kon '())))
  :: Atom (Nat -> Nat -> Type) Nat

Represents an applied constructor. Instead of Kon [] :: Var0$ you can write @[] :$: Var0$.

Represents (homogeneous) type equality.

Represents heterogeneous type equality.

Well-scoped de Bruijn representation of type variables. TyVar d represents all the possible type variables which can refer to the holes in kind d.

We recommend using the aliases Var0, Var1, ... instead of the constructors, for further clarity.

Replaces the holes in the Atom t by the elements of the list of types tys. The amount and kind of types in tys must match statically those required by the Atom.

>>> :kind! Interpret ([] :$: Var0) (LoT1 Int)
Interpret ([] :$: Var0) (LoT1 Int) :: *
= [Int]

Obtains the type in the list tys referenced by the type variable t.

>>> :kind! Interpret Var0 (LoT2 Int Bool)
Interpret Var0 (LoT2 Int Bool) :: *
= Int
>>> :kind! Interpret Var1 (LoT2 Int Bool)
Interpret Var1 (LoT2 Int Bool) :: *
= Bool

Interprets a list of Atom representing constraints into the actual constraints. This is a specialization of Interpret for the case of constraints.

>>> :kind! Satisfies '[Eq :$: Var0, Show :$: Var0] (LoT1 Int)
Satisfies '[Eq :$: Var0, Show :$: Var0] (LoT1 Int) :: Constraint
= (Eq Int, (Show Int, () :: Constraint))

Determines whether a given type variable v is used within an Atom t. If not, we know that the atom is constant with respect to that variable.

Auxiliary type for interpretation of the ForAll atom. Required because a type family like Interpret cannot return a polymorphic type.

Auxiliary type for interpretation of the (:=>>:) atom. Required because a type family like Interpret cannot return a type with constraints.

Records a value of type f applied to the list tys.

>>> :t WrapI [1] :: WrappedI ([] :$: Var0) (LoT1 Int)
WrapI [1] :: WrappedI ([] :$: Var0) (LoT1 Int)