Terms, Types, and Kinds in Haskell

In Haskell, we have three terminologies, term, type, and kind. Understanding their definitions are crucial to understanding Haskell as a practitioner.

List of purely functional programming languages (Image taken from https://www.fpcomplete.com/)

Terms are runtime values, some examples are 1 , True and "Hello" .
Types are the type of terms, the type of 1 is Int, the type of True is Boolean, the type of "Hello" is String and so on.
Kinds are the types of types. For example, the kind of type Int is Type .
Terms have type while types have kind.

Let’s start with the simplest data type which is defined in Haskell.

data Unit = Unit

The keyword data is used to defined a data type , here we introduce two terminologies , type constructor and data constructor.

A data constructor takes zero or more terms to return a concrete term, a concrete term is a term that doesn’t take any parameters and has a concrete type as type signature.
A type constructor takes zero or more types to return a concrete type, a concrete type is a type that doesn’t take any parameters and has Type as kind signature.
Data constructor has type signature while type constructor has kind signature.

In this example, Unit on the left-hand side is a type constructor which takes zero arguments to return a concrete type of kind Type , :k is a command in Haskell to check for the kind signature of type constructor.

:k Unit
Type

Unit on the right-hand side is a data constructor which takes zero arguments to return a concrete term of type Unit , :t is a command in Haskell to check for type signature of data constructor, or function in general.

:t Unit
Unit

It is important to note that type constructors and data constructors are in different namespaces, so the Unit on the left-hand side is not the same as the Unit on right-hand side. The Unit on the left-hand side happens to be both a type constructor and a concrete type, while Unit on the right-hand side happens to be both a data constructor and a concrete term.

When a data type has more than one data constructor, it is a sum type, the symbol | is used to separate two data constructors.

data Boolean = True | False

Similiar to the first example, Boolean is a type constructor which takes zero arguments to return a concrete type of kind Type .

:k Boolean
Type

True and False on the right-hand side are both data constructors which take zero arguments to return a concrete term of type Boolean .

:t True
Boolean
:t
Boolean

Similar to the first example, Boolean is both a type constructor and a concrete type.
Both term True and False have the same type Boolean , and both happen to be data constructors and concrete terms.

When the type constructor of a data type takes arguments, it is a higher kind type.

data Maybe a = Just a | Nothing

In Haskell, any word which starts with a lower case letter that appears in the data type definition is a variable.It is a type variable if appears on the left-hand side and a term variable if appears on the right-hand side.

Maybe is a type constructor which takes a type variable a of kind Type to return a concrete type. Maybe has a kind signature of Type -> Type .

:k Maybe
Type -> Type

Just is a data constructor which takes a term variable a of type a to return a concrete term of type Maybe a .It is important to note that the a inside a -> Maybe is the a from data Maybe a , not Just a .

:k Just
a -> Maybe a

In this example, Maybe is just a type constructor and not a concrete type, we need to apply a type to it to return a concrete type Maybe a.Similarly, Just is just a data constructor and not a concrete term, we need to apply a term to it to return a concrete term.

By now you should know the type signature of Nothing so I would skip that.

When we substitute a with an actual data type, we do it differently for both side, in the example below, we substitute a type Boolean to the left-hand side and the associated term True or False to the right-hand side.

:k Maybe Boolean
Type
:t Just True
Maybe Boolean
data Maybe Boolean = Just (True | False) | Nothing
is the same as 
data Maybe Boolean = Just True | Just False | Nothing

Just True is a term of type Maybe Boolean while Maybe Boolean is a type of kind Type .

Now I am going to introduce a terminology called Generalized Algebraic Data Types, if you understand the concept of the term, type, and kind, you would have no issue in understanding GADTs.

The way a data type gets defined in GADTs is a bit different.

data Maybe a = Just a | Nothing
is the same as 
data Maybe a where
   Just :: a -> Maybe a
   Nothing :: Maybe a

Let’s have a look at the following examples which I took from the internet.

data Term a where
      Lit    :: Int -> Term Int
      Succ   :: Term Int -> Term Int
      IsZero :: Term Int -> Term Bool 
      If     :: Term Bool -> Term a -> Term a -> Term a
      Pair   :: Term a -> Term b -> Term (a,b)

In this example, we have one type constructor Term and five data constructors Lit , Succ , IsZero , Ifand Pair .

Lit 1 is a term of type Term Int , Succ takes a term of type Term Int to return a concrete term of type Term Int .Since Lit 1 has type Term Int, Succ can take Lit 1 as an argument to return a term Succ(Lit 1) of type Term Int .Furthermore, Succ could take Succ (Lit 1) of type Term Int to return a term Succ (Succ (Lit 1)) of type Term Int , and it goes on.

In this article, I explain what are terms, types, and kinds. Many concepts in Haskell require an understanding of these terminologies. In case you face difficulty in understanding any concept, try to think of their definitions.Trying to understand the mathematical theory behind them or even worse, trying to find analogies in mainstream programming languages are likely to get you lost.

With these, it is not hard to tell what is the type of If (IsZero(Succ(Succ(Lit 1)))) (Succ(Lit 1)) ( Succ(Succ(Succ(Lit 1)))) .

PS: Any correction is welcomed.