Types

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.

What does a type look like?

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.)

Some base types

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.

The function type and type level operators

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 Ints to Ints. The second is a type that takes a function as an argument and returns an Int.

Drill

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

Type applications

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)...

Type variables and polymorphism

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.

Constraints

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 Doubles and another one for summing lists of Ints. 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`.

Drill

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

Function types

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 Ints, 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.

Drills

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

Types resulting from function application

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.

Drill

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?

Deducing types

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.

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.

Drills

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:

  1. Function literals have the type (:t a) -> (:t b):

    
       :t (\x -> e)
    == {- Type of function literal -}
       (:t x) -> (:t e)
    
  2. 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")

  3. 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
    
  4. 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.)

  5. 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»).

  6. :t «x» == x. I.e. type of 'something of a type x', is x.

  7. 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.

Worked Example: What is the type of 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 a type 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.

Worked Example: \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]

Worked Example: (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.

Worked Example: What is the type of \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.

Worked Example: What is the type of function 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])

Note on meaning of Type variables

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.

Drills

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

Exercises

Exercise -- Typing the function composition.

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)

Exercise -- What types

What would be the types for the following functions:

  1. Function that reverses each word in a string?
  2. Function that counts the number of empty lines in a string?
  3. Function that applies a some operation to every word in a string?
  4. Function that sorts a list using user specified sorting order?
Upload answer

(Firefox temporarily unsupported. Use chrome)

Exercise -- Deduce types I

  1. What is the type of f = unwords . map reverse . words
  2. What is the type of f str = maximum (map length (words str))
  3. 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)

Exercise -- Deduce types II

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)

Exercise -- Constraints

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)

Footnotes


  1. 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:

[TOPIC]



Clarity of presentation

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

Interestingness of the topic


Detailed comments/Criticisms




Comments on this section