In statically typed languages, each *expression* has a known *type*. Types describe the form of values the expression can reduce to. For example, the expression `"hello"++" "++"world"`

has the type `String`

, expressing the fact that evaluating this expression will result in a string. Similarly, `length [1,2,3]`

has the type `Int`

, telling us that result of that calculation will be a machine representable integer.

Types are used in many languages, including Haskell, as a tool for ensuring correctness of the programs. By stating the type of a complex expression the compiler can verify that that our expression will reduce into a value of the right sort, which protects us from numerous programming errors.

Haskell programs can contain very complex expressions, which makes the added security given by the type system important. In contrast to mainstream languages, such as Java or C#, the Haskell type system is also much more flexible, allowing the programmer to specify more precisely the intent of the program. Further, Haskell supports *type-inference*, meaning that the programmer does not need to specify the types of expressions if the type is otherwise apparent from the context. Often, Haskell programmers specify types for *top-level expressions* only, and usually for reasons of documentation.

In this section, we will learn how to read most the type declarations that appear in Haskell programs.

Types are written with their own, simple, language, which is different from the language of the value level expressions we have previously encountered. The reason for the difference between the type-expressions and value-expressions is that value expressions, such as `1+2`

or `(\x->x+x) 5`

, describe what the computer computes, while type-level expressions, such as `Int -> Int`

, are statements **about** the properties of the value level expressions in your program.

Type declarations often appear above declarations, or they can be attached directly subexpressions of the program.

```
x :: Int -- Top level declaration:
-- "x has type Int"
x = 7
y = 8 :: Int -- Type declaration attached to
-- subexpression: "8 has type Int"
```

(If you want more details, a formal description of syntax of types is written here.)

These types will be used throughout the exercises and they are fundamental for Haskell programs

```
-- Type level -- Value level
Int -- 2, 42, 1921...
Bool -- True, False...
Double -- 1.01, pi, 9192.91...
Char -- 'a','b','c'...
String -- "cat", "this is a string"...
```

All type names begin with an uppercase letter.

Similarly to value level operators such as `+`

, type level expressions also have (type) operators, the most common of which is the function arrow `->`

.

```
Int -> Bool -- A Function from ints to booleans
String -> Bool -- A Function from strings to booleans.
String -> (String -> Bool) -- A function from strings into
-- functions from strings to bools
(String -> String) -> Bool -- A function from 'functions from strings to strings'
-- to booleans.
```

The function arrow is right associative, which means that `Int -> Int -> Int`

is the same as `Int -> (Int -> Int)`

. Similar to value level operators, we sometimes need to use parenthesis to express the exact meaning we have in mind. There is a difference between `Int -> (Int -> Int)`

and `(Int -> Int) -> Int`

. The first is a type for a function from `Int`

to a function from `Int`

s to `Int`

s. The second is a type that takes a *function* as an argument and returns an `Int`

.

**Check your understanding.** Which of the types below have the same meaning as `Int -> Int -> Int -> Int`

?

We often need "enhanced" types when programming, like an `Int`

that might not exist, or a type that could be one of two types, or a list of values of some type. Haskell's type system allows us to express this extra information at the type level (see simple usage examples in Sum types section).

```
-- Type level -- Value level
Maybe Int -- Just 42, Just 81, Nothing
Either String Int -- Left "Division by zero", Right 12, Right 42...
```

Lists and pairs are so widely used that they have their own special syntax to make writing them easier:

```
-- Type level -- Value level
[Bool] -- [True,True,False], [True,False]...
(Int,Char) -- (15,'x'), (42,'a')...
(Int,Int) -- (1,2), (42,15)...
```

Polymorphism is a word used to describe expressions that work the same on many different types. For example, length of a list can be calculated for any list regardless what type of values it contains.

Polymorphic expressions are declared with type variables, which are written with lower case letters. Many Haskell programmers use single letter variables such as 'a', 'b', or 'c'. But any word beginning with a lower case letter is considered a type variable by the Haskell compiler.

```
-- Type level -- Value level
a -> Int -- \x -> 14, \x -> 1+2, const 4,..
[a] -> Int -- length...
Maybe a -> Bool -- isJust, isNothing..
[a] -- [] (the empty list)
```

Another way of looking at type variables is that when a polymorphic type is used, its type variables can be replaced with any type you want. If you have a function of type `[a] -> Int`

, you can then choose `a`

to be a `Bool`

and use the function as if it had a type `[Bool] -> Int`

.

As you can guess from the previous examples, unrestrained polymorphism keeps us from writing functions that know anything about the values of type `a`

. This works well for calculating the length of a list, but consider calculating the sum of a list of numbers. We certainly wouldn't want to write a different function for summing lists of `Double`

s and another one for summing lists of `Int`

s. Summing function needs to be polymorphic, but it cannot take type `[a]`

as argument because then it would have to work on *all* types, such as lists of strings. We need to add a constraint to specify that only numbers are accepted:

```
Num a => [a] -> a -- This function takes a list of numbers and returns
-- a number. This could sum a list of numbers.
```

You can have multiple constraints on the same type expression like this:

```
(Integral a, Num b) => a -> b -- This function takes any `a` that is `Integral` and
-- and returns any `b` that is `Num`.
```

**Check your understanding.** Which of the following are types for a function that could return maximum element in a list?

Recall here the discussion about function literals and 'currying` in the section about function values and function literals. Understanding that chapter is essential for understanding function types.

Function types are written as '*type* `->`

*type*' where the first *type* is the type of the argument for the function and the second *type* is the type of the return value. For example, the function `\x -> x == "cat"`

has the type `String -> Bool`

, since `x :: String`

and `(x == "cat") :: Bool`

. As another example, we have `length :: [a] -> Int`

, which takes as an argument a list containing any type of a value (`[a]`

) and returns an `Int`

.

Notice that the function type allows only a single parameter, which mirrors the situation with function values discussed earlier. With values, we constructed a multiparameter functions by taking one argument and returning another function to handle the rest:

```
(\height -> (\width -> width * height))
```

Supposing for a moment that `height`

and `width`

are `Int`

s, the type of the above expression will be `Int -> (Int -> Int)`

. This is because the outermost function has the type `Int -> :t (\width -> width * height)`

, where the type of the inner function is `Int -> Int`

.

The arrow `->`

is right associative, so writing `Int -> (Int -> Int)`

is same as writing `Int -> Int -> Int`

.

Notice that the shorthand syntax for multiparameter function literals (i.e. `\width height -> width * height`

) has exactly the same type as the longer syntax. Similarly, the function definitions (see here and link-TBD), such as

```
rectangleArea :: Int -> (Int -> Int)
rectangleArea height width = width * height
```

follow the above rule just as if they would have been written as function literals.

**Check your understanding.** Which of the types below are equivalent to `Int -> Int -> Bool`

Suppose that you have a function `f`

with type `Int -> Bool`

and value `x`

with type `Int`

. Then you can write the expression `f x`

. What is the type of this expression? In the value level, the computation proceeds as follows:

```
f x
== {- Suppose that f is \y -> y < 5, and that x is 3 -}
(\y -> y < 5) 3
== {- Function application, y:=3 -}
3 < 5
== {- Three is less than five -}
True
```

Since type of `True`

is `Bool`

and `f x`

is equal to `True`

the type of `f x`

must also be `Bool`

.

In general, if a function is applied, the application has the type that is written on the right of the function arrow `->`

. Contrast this with the function literals; there also the result of the function is written on the right of the arrow.

**Check your understanding.** If type of `f`

is `Int -> String`

, `x`

is an `Int`

and `y`

is a `String`

, which of the below type declarations are correct?

**Check your understanding.** Let `f`

be a value of type `(a,b,a) -> a`

and `x`

be an arbitrary value of some type given below. Which of these types allow you to write `f x`

?

The Haskell type system is a somewhat complex and hard to demonstrate using plain Haskell syntax. In this course, we use an experimental way of teaching how to work with types using step-by-step derivations. We hope that by using this trick, we can better illustrate why some expression carries the type it does.

To do this, we demonstrate how you can deduce the type of a value expression in mechanical way. We **do** know that reading and doing derivations is painful. Just keep in mind that they are only a tool for you to build up your grasp about types. Programming in Haskell won't require doing stuff like this after you have firm idea of how types work.

We also note that if you are familiar with how the type system works or if you have a good intuition about formalisms, mathematical or otherwise, you might not actually need this detailed introduction.

We use the following notation to explain the behaviour of types.

- ":t x" means "the type of x", and
- "«τ»" means "some value of type τ". For example,
`«Int»`

means 'some value of type`Int`

'.

This notation allows us to concisely describe the behaviour of types. Instead of writing difficult to read statements like 'the type of `\x->x+x`

is the 'type of `x`

' `->`

'the type of `x+x`

', we can write

```
:t \x -> x+x
==
(:t x) -> (:t x+x)
```

**Notice:** This is **not** part of the Haskell language but a tool for learning. The compiler will **not** understand this syntax.

**Check your understanding.** Which of the types below would be accepted by a Haskell compiler

**Check your understanding.** Which of the following are *types* in the syntax described above?

Deducing types is based on following these rules:

**Function literals**have the type`(:t a) -> (:t b)`

:`:t (\x -> e) == {- Type of function literal -} (:t x) -> (:t e)`

**Type of function application**is the type of the return value:`:t «a -> b» «a» == {- Type of application -} :t «b»`

(

*"Give what is left of the arrow, get what is on the right"*)Setting of

**type variables**. You can replace any type variable with another type as long as you replace*all*variables with the same name with the same type.`:t a == {- Variables can be replaced. -} :t b`

**Known symbols**(such as`length`

) and literals (such as`"cat"`

) can be replaced with the known type in «»-brackets.Make sure that doing this doesn't introduce type variables that already appear in the expression, otherwise you might get stuck. (See the next section.)

**Constraints**. All instances of the same type variable must have the same constraints. This can be often achieved by floating the constraints to the left of the expression.I.e. you can't have an expression

`:t «b -> b» «Eq b => b»`

. Instead write:`Eq b => (:t «b->b» «b»)`

.. I.e. type of 'something of a type`:t «x» == x`

`x`

', is`x`

.**Type of a bound variable**(i.e.`x`

in`\x -> x+15`

) can be set to`a`

or another unused type variable,*if*all occurrences of the variable are set the same.

These rules allow you to deduce the types of most basic expressions, but they do not cover things like types of pairs, or lists. Also, the above rules only work in cases where the expression is well typed. As an example of the alternative, we might end up with expression like `:t «Int -> Int» «String»`

, which isn't a type, and for which there is no rule which allows further simplification. This signals a type error in the program.

`length "panama"`

Suppose we wanted to know what is the type of the expression `length "panama"`

, we could proceed in the following fashion:

First, we look up the type of

`length`

, which is`[a] -> Int`

. Then we figure out that`"panama"`

is a`String`

and`String`

is just an alias for`[Char]`

. Now, we notice that we are trying to pass a`[Char]`

as a parameter to a function of type`[a] -> Int`

. Since`a`

is atype variable, we can choose it to be`Char`

and get`length :: [Char] -> Int`

. Giving`length`

the thing on the left of the arrow, we get the thing on the right of the arrow, which is`Int`

. Thus, the type of the expression`length "panama"`

is`Int`

.

Writing out our reasoning like this is very hard to read and the explanations get quite long. Instead, we use the following formal notation to explain this same thing:

```
:t length "panama"
== {- Type of `length` is [a] -> Int -}
:t «[a] -> Int» "panama"
== {- Type of `"panama"` is [Char] -}
:t «[a] -> Int» «[Char]»
== {- a := Char. Otherwise the argument and the parameter don't match -}
:t «[Char] -> Int» «[Char]»
== {- Function application. «a -> b» «a» = «b» for any a and b. -}
:t «Int»
== {- Type of something of a type Int is Int-}
Int
```

Here, each step is short and carries with it an explanation of why it could be taken. If you are unaccustomed to formal notations, reading the above example might seem bit awkward, but spending bit of an effort to understand it will pay off in the future.

`\x -> (\y -> y ++ y)`

This example demonstrates Rule 7. We know that

```
(++) :: [a] -> [a] -> [a]
```

so we can deduce

```
:t \x -> (\y -> y ++ y)
== {- Rule 1. Type of function literal -}
(:t x) -> (:t \y -> y ++ y)
== {- Rule 7. (:t x) := c (we use c to avoid conflicting with type of ++) -}
c -> (:t \y -> y ++ y)
== {- Rule 1. Type of function literal -}
c -> ((:t y) -> (:t y ++ y))
== {- For clarity, convert operator '++' into function form. -}
c -> ((:t y) -> (:t (++) y y))
== {- Replace (++) and y with their types -}
c -> ((:t y) -> (:t «[a]->[a]->[a]» «:t y» «:t y»))
== {- Rule 7, type of a variable, :t y := b -}
c -> (b -> (:t «[a]->[a]->[a]» «b» «b»))
== {- Rule 3, b := [a], so we can use application later on -}
c -> ([a] -> (:t «[a]->[a]->[a]» «[a]» «[a]»))
== {- Rule 2, the application -}
c -> ([a] -> (:t «[a]->[a]» «[a]»))
== {- Rule 2, again -}
c -> ([a] -> (:t «[a]»))
== {- Rule 6, :t «[a]» = [a] -}
c -> ([a] -> [a])
== {- Associativity of -> -}
c -> [a] -> [a]
```

`(length "cat", length [1,2])`

This example demonstrates the Rule 4. Suppose that we know that

```
"cat" :: [Char]
[1,2] :: [Int]
length :: [a] -> Int
```

then we could deduce the type of this pair like so:

```
:t (length "cat",length [1,2])
== {- Rule 4. Types of "cat" and [1,2] -}
:t (length «[Char]», length «[Int]»)
== {- Rule 4. Type of first length -}
:t («[a] -> Int» «[Char]», length «[Int]»)
```

Suppose that we would show the type of the second `length`

next. Without respecting the rule 4, we would get `:t («[a] -> Int» «[Char]», «[a] ->Int» «[Int]»)`

, which is incorrect, since now we'd need `a`

to be a `Char`

for the first application and an `Int`

for the second. Instead we must make sure we don't accidentally use same names in two different meanings:

```
:t («[a] -> Int» «[Char]», length «[Int]»)
== {- Rule 3, set a := b -}
:t («[b] -> Int» «[Char]», length «[Int]»)
== {- Rule 4, Type of second length -}
:t («[b] -> Int» «[Char]», «[a] -> Int» «[Int]»)
== {- Rule 3, b := Char -}
:t («[Char] -> Int» «[Char]», «[a] -> Int» «[Int]»)
== {- Rule 2, Function application -}
:t («Int», «[a] -> Int» «[Int]»)
== {- Rule 3, a := Int -}
:t («Int», «[Int] -> Int» «[Int]»)
== {- Rule 2, Function application -}
:t («Int», «Int»)
== {- Rule 6, Type of 'a pair of Ints' is (Int,Int) -}
(Int,Int)
```

The above example is a bit tedious since we have been to meticulous in writing down each and every step separately. In practice, you can avoid the renaming stuff by directly replacing the first `length`

with `«[Char] ->Int»`

and the second with `«[Int] -> Int»`

or by choosing the right order for function applications.

`\y -> y == 0`

?This example demonstrates the use of the Rule 5, constraints.

Let us deduce the type for the following expression:

```
\y -> y == 0
```

The types of the constituent parts of the definition, which can be found with either ghci or looked up from the documentation, are:

```
(==) :: Eq b => b -> b -> Bool
0 :: Num a => a
```

The deduction proceeds as follows:

```
:t (\y -> y == 0)
== {- Rule 1: Type of a function \z -> h is `« «:t z» -> «:t h» »`-}
:t «(:t y) -> (:t y==0)»
== {- Turn the `==` operator into a function -}
:t «(:t y) -> (:t (==) y 0)»
== {- Parenthesise the function application -}
:t «(:t y) -> (:t ((==) y) 0)»
== {- Replace known symbols with arbitrary values of same type -}
:t «(:t y) -> (:t («Eq b => b -> b -> Bool» y) «Num a => a»)»
== {- Float constraints to left to satisfy rule 5 in the next step. -}
:t «(Eq b, Num a) => (:t y) -> (:t (b -> b -> Bool» y) «a»)»
== {- Rule 3.Type of `y` must be `b` or else it couldn't be passed as a parameter -}
:t «(Eq b, Num a) => b -> (:t («b -> b -> Bool» «b») «Num a => a»)»
== {- Rule 2. function app.. -}
:t «(Eq b, Num a) => b -> (:t («b -> Bool») «a»)»
== {- Rule 3. Set a:=b to make the types match-}
:t «(Eq b, Num b) => b -> (:t (« b -> Bool») «b»)»
== {- Rule 2. Function application -}
:t «(Eq b, Num b) => b -> (:t «Bool»)»
== {- Rule 6. :t «Bool» = Bool-}
:t «(Eq b, Num b) => b -> Bool»
== {- Rule 6. Type of a "something of type T" is T -}
(Eq b, Num b) => b -> Bool
```

Notice that we can nest `:t`

's and `«x»`

's.

`g f = map x . concat . words`

?Let us deduce the type for `example`

in:

```
g f = map f . concat . words
```

First, we need to find out the types of each of the component functions. To avoid mixing things up later, we assign each of them unique type variable names. We also replace the `String`

type alias with its definition `[Char]`

to make things more clear later on.

```
map :: (q->w) -> [q] -> [w]
concat :: [[a]] -> [a]
words :: [Char]-> [[Char]]
(.) :: (u -> h) -> (k -> u) -> k -> h
```

Now we can deduce as follows:

```
:t g
== {- Example is a function from f to something -}
:t «(:t f) -> (:t map f . concat . words)»
== {- Replace map -}
:t «(:t f) -> (:t «(q->w) -> [q] -> [w]» f . concat . words)»
== {- :t f must be (q->w) -}
:t «(q->w) -> (:t «(q->w) -> [q] -> [w]» «q->w» . concat . words)»
== {- Function application -}
:t «(q->w) -> (:t «[q] -> [w]» . concat . words)»
== {- Replace concat -}
:t «(q->w) -> (:t «[q] -> [w]» . «[[a]] -> [a]» . words)»
```

At this point we could convert `.`

to `«(u -> h) -> (k -> u) -> k -> h»`

, but this would make things *very* complicated. Instead we note that `«u->h» . «k->u» = «k->h»`

holds for all `u`

, `h`

and `k`

and go our merry way. (You need to prove that this actually holds in the exercise section).

```
:t «(q->w) -> (:t «[q] -> [w]» . «[[a]] -> [a]» . words)»
== {- q := a -}
:t «(a->w) -> (:t «[a] -> [w]» . «[[a]] -> [a]» . words)»
== {- «u->h» . «k->u» = «k->h» -}
:t «(a->w) -> (:t «[[a]] -> [w]» . words)»
== {- Replace words -}
:t «(a->w) -> (:t «[[a]] -> [w]» . «[Char]->[[Char]]»)»
== {- a := Char-}
:t «(Char->w) -> (:t «[[Char]] -> [w]» . «[Char]->[[Char]]»)»
== {- «u->h» . «k->u» = «k->h» -}
:t «(Char->w) -> (:t «[Char] -> [w]»)»
== {- Eliminate :t's and «»'s-}
(Char->w) -> ([Char] -> [w])
```

Type of the function `length`

is an example of a type declaration in which a type variable is used:

```
length :: [a] -> Int
```

The meaning of the above type definition is to say that `length`

is a function that returns an `Int`

when given a list containing **any** type chosen by the caller of this function. For example, we can choose `a`

to be an `Int`

, which allows us to write `length [1,2,3]`

, or we can choose `a`

to be `String`

, which allows us to write `length ["a","cat"]`

.

The code implementing `length :: [a] -> Int`

contains no information of what `a`

will be when the `length`

is called. This means that the `length`

cannot really do anything with any value of type `a`

and that the *values of the list* have **no influence** on the result of the `length`

function. Polymorphism is a powerful tool in ensuring correctness of programs. As a simplistic example, consider a function of type `(a,b) -> a`

. This function maps a pair of `a`

and `b`

into an `a`

. This ensures us that `b`

can have no effect at all in the result of the function. If we instead would have written `(Int,Int) -> Int`

we have no such guarantee -- the function might return any combination of the elements of the pair, or something totally unrelated, such as `0`

.

Polymorphic function has less implementations than one where the types are fixed. Also, such function can be used in more occasions than one with fixed types.

**Check your understanding.** Which of the following type declarations are correct?

Complete the worked example above, by showing that `«u->h» . «k->u» = «k->h»`

holds for all `u`

, `h`

and `k`

, by filling in the following calculation:

```
«u->h» . «k->u»
== {- Use (.) instead of .-}
(.) «u->h» «k->u»
==
-- Complete this part.
==
«k->h»
```

The type of the operator `(.)`

is `(.) :: (b -> c) -> (a -> b) -> a -> c`

Upload answer

(Firefox temporarily unsupported. Use chrome)

What would be the types for the following functions:

- Function that reverses each word in a string?
- Function that counts the number of empty lines in a string?
- Function that applies a some operation to every word in a string?
- Function that sorts a list using user specified sorting order?

Upload answer

(Firefox temporarily unsupported. Use chrome)

- What is the type of
`f = unwords . map reverse . words`

- What is the type of
`f str = maximum (map length (words str))`

- What is the type of
`f a b = max 0 (min a b)`

You *can* use the command `:type`

to find out the types of the above symbols, such as `unwords`

or `max`

, but please do the derivation yourself.

Include derivations or other justification for each type in your answer.

Upload answer

(Firefox temporarily unsupported. Use chrome)

Which of the following are well typed declarations ^{1} ? What are their (most general) types?

```
a = 42
b = (\x -> x) 3
c x = \y -> False
d = \x -> \y -> False
e = \x -> snd x
f = \x -> snd (head x)
g xs = map map xs
h a xs = foldl foldl a xs
i = map . map
```

You *can* use the command `:type`

to find out the types of the above symbols, such as `42`

or `map`

, but please do the derivation yourself.

Include derivations or other justification for each type in your answer.

Upload answer

(Firefox temporarily unsupported. Use chrome)

Consider the following types:

```
foo :: Num b => [a] -> b
foo xs = ..
bar :: (Num a, Num b) => [a] -> b
bar xs = ..
baz :: [a] -> b
baz xs = ..
```

Which of the types is the most restrictive in what the implementation could do? Which is the least restrictive? Why?

Upload answer

(Firefox temporarily unsupported. Use chrome)

Well typed means that the expression has a proper type. For example,

`1+1`

is well typed, since`(+)`

works with numbers and`1`

is a number. Expression`1 + True`

, however, is not well typed since`Bool`

is not a number and thus cannot be added to`1`

.↩

⊗
## Give feedback on:

## Comments on this section

[TOPIC]

Clarity of presentation

Difficulty of the topic (1 star=easy, 5 stars=very hard)

Interestingness of the topic

Detailed comments/Criticisms