# Notes (TLPH 02/15): Terms, Types and Kinds

# 2.1 The Kind System

A **kind** is a type of types. Compile-time is runtime for the compiler, and values the compiler runs computation on are types.

## 2.1.1 The Kind of “Types”

Roughly, a “type” are type-level terms, a subset of which are “value types”, which can be inhabited by runtime values and correspond to the Haskell kind `*`

or `Type`

. For example `Maybe`

is a type, but not a `Type`

, because it has kind `Type -> Type`

.

## 2.1.2 Arrow Kinds

Higher-kinded types are type constructors. `Maybe`

is an HKT, because its kind is `Type -> Type`

.

## 2.1.3 Constraint Kinds

## Exercise 2.1.3 (i)

`Show`

has kind `Type -> Constraint`

## Exercise 2.1.3 (ii)

`Functor`

has kind `(Type -> Type) -> Constraint`

, since it operates on unary type constructors (like `[]`

, `Maybe`

etc.).

## Exercise 2.1.3 (iii)

`Monad`

has kind `(Type -> Type) -> Constraint`

## Exercise 2.1.3 (iv)

The definition of `MonadTrans`

is:

```
class MonadTrans t where
lift :: Monad m => m a -> t m a
```

From the class declaration, which must be a `Constraint`

, we can see that `MonadTrans`

has kind `T -> Constraint`

, where `T`

is the kind of the `t`

type variable.

We can expand the kind of `T`

by noticing that in the type signature for `lift`

, `t`

is a type constructor that takes two arguments `m`

and `a`

, therefore it’s kind must be `M -> A -> Type`

, where `M`

is the kind of `m`

and `A`

is the kind of `A`

. Only `Type`

kinds can appear in type signatures.

In the constraint on `lift`

, the type variable `m`

is an argument to `Monad`

, which has kind `(Type -> Type) -> Constraint`

.

Therefore kind `M`

is `Type -> Type`

, and since `m a`

has kind `Type`

, the kind of `a`

is `Type`

.

Therefore the kind of `t`

is `(Type -> Type) -> Type -> Type`

, and the kind of `MonadTrans`

is

`Type -> Type) -> Type -> Type -> Constraint (`

# 2.2 Data Kinds

`-XDataKinds`

allows lifting of data constructors into type constructors.

Seems like there are some bugs with the `UserType`

example given in the text if naively copied into a source file, but perhaps that wasn’t the author’s intent. Regardless, was a simple fix:

```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data UserType = UserK | AdminK
data Proxy (a :: UserType) = Proxy
data User = User { userAdminToken :: Maybe (Proxy 'AdminK) }
doSensitiveThings :: Proxy 'AdminK -> IO ()
= undefined doSensitiveThings
```

Which kind-errors on `doSensitveThings (a :: Proxy 'UserK)`

# 2.4 Type-Level Functions

For exercise solutions, see `02/TypeLevelFunctions.hs`