===== Haskell type system =====
==== Note ====
Haskell has a two-level type system. There //kinds// which are inhibited by //types//, and these types are further inhibited by //terms//. Kind and type inference can be done in the Haskell ghci-environment via ':k' and ':t', respectively.

=== Kinds ===
The syntax for kinds is pretty simple. The most relevant kind to discuss is $\star$, the kind of //data types//. There is furthermore an important 2-ary symbol $k_1\longrightarrow k_2$. If $k_1,k_2$ are kinds of finite depth, then $k_1\longrightarrow k_2$ is a kind with inhabitants called //type constructors//. 

== Examples for kinds and their inhibiting types ==
$\mathrm{Int}\ :\ \star\hspace{1cm}$ ... type of integers

$[]\ :\ \star\longrightarrow\star\hspace{1cm}$ ... list type constructor

$[\mathrm{Int}]\ :\ \star\hspace{1cm}$ ... type of lists of integers

$(\to)\ \mathrm{Int}\ :\ \star\longrightarrow\star\hspace{1cm}$ ... functions from integers type constructor

$(\to)\ \mathrm{Int}\ \mathrm{Int}\ :\ \star\hspace{1cm}$ ... type of functions from integers to integers, which is also written in infix notation, $\mathrm{Int}\to\mathrm{Int}$

$(\to)\ :\ \star\longrightarrow\star\longrightarrow\star$

Next to $\star$, another relevant 0-ary kind is $\mathrm{Constrained}$. We'll come back to it in the section on type classes.

=== Data Types ===
Haskell has some in-build data types ($\mathrm{Int}$, $\mathrm{Bool}$, ...), see [[http://hackage.haskell.org/package/base-4.5.0.0/docs/Prelude.html|Prelude]]. Some possibilities to create new ones is discussed in the following.

To keep things simple, the following examples don't employ type polymorphism. Hence, all type variables $a,b$ should be thought of as replaced by concrete types.

== Function types ==
Type theoretically (on the kind level): 
${\large\frac{a\ :\ \star \hspace{.5cm} b\ :\ \star}{a\to b\ :\ \star}}$ 

Haskell syntax:
<code/Haskell>
a->b
</code>

Type theoretically: 
${\large\frac{x\ :\ a \hspace{.5cm} g\ :\ b}{\lambda x.g\ :\ a\to b}}$ 

<code/Haskell>
((\x->g) :: a->b)
</code>
for example
<code/Haskell>
((\n->n^2) :: Int->Int) 3
</code>

{{haskell_trivial_1.png?X300}}

Due to Haskells type inference, the annotation "::a->b" is often optional.

And there are many in-build functions such as the logical 'and' or the arithmetic '+'.

== Product types ==
There is the product type $a\times b$ (Cartesian product/direct product/logical and), written
<code/Haskell>
(a,b)
</code>
But notice that there is automatical currying and so it doesn't appear in function declaration as often as one might guess.
Here an example with only one type $a$. Let's write $\mathrm{TripleType}(a)\equiv a\times a\times a$. Then

${\large\frac{a\ :\ \star}{\mathrm{TripleType}(a)\ :\ \star}}$,
 
${\large\frac{x,y,z\ :\ a}{\langle x,y,z\rangle\ :\ \mathrm{TripleType}(a)}}$

Haskell syntax is
<code/Haskell>
type TripleType a = (a,a,a)
</code>
Now we can ask ':k TripleType' and ':k TripleType Int' and find $\star\longrightarrow\star$ and $\star$, respectively.

== Algebraic data types ==
Algebraic data types are a more free means to create types. In general one specifies a kind of type sum (disjoint union/direct sum/logical or) of one or more alter- natives, where each alternative is a product of zero or more slots.
Uppercase words for are used for constructions, for example, there is $\mathrm{Either}$. 

The standard example is this: Let $a$ be a type variable. Say we want to make a type of binary tree graphs for $a$, where a term is either a term of $a$ or forking branch. In type theoretic notation:

${\large\frac{a\ :\ \star}{\mathrm{Tree}(a)\ :\ \star}}$

${\large\frac{x\ :\ a}{\mathrm{Leaf}(x)\ :\ \mathrm{Tree}(a)}}$, ${\large\frac{s,t\ :\ \mathrm{Tree}(a)}{\mathrm{Branch}(s,t)\ :\ \mathrm{Tree}(a)}}$

<code/Haskell>
data Tree a = Leaf a | Branch (Tree a) (Tree a)
</code>
The introduced key words $\mathrm{Leaf}$ and $\mathrm{Branch}$ are further used for pattern maching. E.g. in the function definition
<code/Haskell>
size :: Tree a -> Int
size (Leaf x) = 1
size (Branch t u) = size t + size u + 1
</code>

== Polymorphic types ==
Haskell also supports types with $\forall$-quantified type variables, e.g. $\forall a.a\to a$, like [[http://en.wikipedia.org/wiki/System_F|System F]]. An example for a defintion for a terms polymorphic type is
<code/Haskell>
map :: forall a b. (a -> b) -> [a] -> [b]
</code>
This type is //parametrically polymorphic//. 

== Type checking (and "Kind checking", if you will) examples in ghci ==

{{haskell_type_checking.png?X400}}

=== Type classes ===
We introduce the 'class' keyword. It lets us specify subsets of types or type constructors by demanding implementations of associated functions. Members of these subsets are then instantiated with the 'instance' keyword, where you write specific implementations of the function. This is called //ad hoc polymorphism//, the less nice polymorphism.

== Example ==
The class $\mathrm{Integral}$ contains $\mathrm{Int}$ and $\mathrm{Integer}$. It is a subset of $\mathrm{Real}$, which also contains $\mathrm{Float}$ and $\mathrm{Double}$. Which in turn is a subset of $\mathrm{Eq}$, which contains many more types. 
For any two terms $x,y$ of a type in $\mathrm{Eq}$, the function application of $==$ makes sense. To quote the definition of the simple $\mathrm{Eq}$-class:

<code/Haskell>
class Eq a  where
   (==), (/=) :: a -> a -> Bool
</code>

While 'class' is a keyword, $\mathrm{Eq}$ is an operation with kind $\star\longrightarrow\mathrm{Constraint}$.

For $\mathrm{Eq}$ instance, it's worth pointing out that if you skip writing one of of the two function instances, Haskell will try
<code/Haskell>
   x /= y     =  not (x == y)
   x == y     =  not (x /= y)
</code>

=== Category theory ===
The kind $\star$ can be viewed as the objects of certain category, see [[Hask]]. The kind $\star\longrightarrow\star$ can be viewed as the object map of Hask-endofunctors. Indeed, functors are formalized in Haskell as the class of type constructors $\star\longrightarrow\star$ for which an associated function map 'fmap' is implemented.

<code/Haskell>
class  Functor f  where
    fmap :: (a -> b) -> (f a -> f b)
</code>

(See [[Functor . Haskell]])

The operation Functor is of kind $(\star\longrightarrow\star)\longrightarrow\mathrm{Constraint}$. Hence any instance $f$ will be of kind $\star\longrightarrow\star$.

There is no Haskell-mechanism which enforces laws on class members, so one should only instantiate a member of $\mathrm{Functor}$ if it does respect the identity and composition law. 

=== Examples ===
This is the example of the fairly obvious $\text{fmap}$-implementation for the List-Functor ("List" has it's own name, namely "[]"):

<code/Haskell>
instance Functor [] where
  fmap _ []     = []
  fmap g (x:xs) = g x : fmap g xs
</code>

{{haskell_trivial_2.png?X350}}

The type system derives which fmap to use from the fact that we apply the construction to a list.

The following example is the functor whose object map maps each type to a type, where each of the old terms have a clone with the prefix '$\text{Just}$', and there is more over an additional term called nothing '$\text{Nothing}$':

<code/Haskell>
instance Functor Maybe where
  fmap _ Nothing  = Nothing
  fmap g (Just a) = Just (g a)
</code>
This can be used to deal with exceptions.

For all types $a$, the constructor $(\to)\,a$ is the object map of $\mathrm{Hom}_\mathrm{Hask}(a,-)$. 

In fact, all of the functors mentioned can be made into [[monad_._haskell|monads]], and they are known as list, maybe and reader monad.

=== Reference ===
Wikipedia: [[http://en.wikipedia.org/wiki/Kind_%28type_theory%29|Kind (type theory)]]

-----
=== Related===
[[Hask]]

=== Requirements ===
[[Type theory]], [[Haskell]]