Types, lambda functions and type classes
Function types
 Ordinary data types are for primitive data (like and ) and basic data structures (like and ).

Algebraic data types are types that combine other types either as records (‘products’), e.g.
data Pair = Pair Int Double
or as variants (‘sums’), e.g.
data Bool = False  True
 Functions have types containing an arrow, e.g. .
 We now look at function types in more detail.
Lambda expressions
 Lambda expressions (named after the greek letter ) play a very important role in functional programming in general and Haskell in particular.
Named and anonymous expressions
 You can give a name to an expression :
sum = 2+2
 But you can also write anonymous expressions — expressions that just appear, but are not given names.
(b) + sqrt (b^2  4*a*c)
 Without anonymous expressions, writing this would almost be like assembly language:
e1 = (b)
e2 = b^2
e3 = 4*a
e4 = e3*c
e5 = e2e4
e6 = e1+e5
Some background

Sometimes in a mathematics or physics book, there are statements like “the function is continuous”

This is ok when the context makes it clear what is.

But it can lead to problems. What does mean?

Is it a constant, because both and have fixed values?

Is it a function of , with a fixed value of ?

Is it a function of , with a fixed value of ?

Is it a function of both and ?


In mathematical logic (and computer programming) we need to be precise about this!

A lambda expression contains

An explicit statement that the formal parameter is , and

the expression that defines the value of the function.

Anonymous functions
 A function can be defined and given a name using an equation:
f :: Int > Int
f x = x+1

Since functions are “first class”, they are ubiquitous, and it’s often useful to denote a function anonymously.

This is done using lambda expressions.
\x > x+1
Pronounced “lambda x arrow x+1”.
There may be any number of arguments:
\x y z > 2*x + y*z
Using a lambda expression
Functions are first class: you can use a lambda expression wherever a function is needed. Thus
f = \x > x+1
is equivalent to
f x = x+1
But lambda expressions are most useful when they appear inside larger expressions.
map (\x > 2*x + 1) xs
Monomorphic and polymorphic functions
Monomorphic functions
Monomorphic means “having one form”.
f :: Int > Char
f i = "abcdefghijklmnopqrstuvwxyz" !! i
x :: Int
x = 3
f x :: Char
f x  > 'd'
Polymorphic functions
Polymorphic means “having many forms”.
fst :: (a,b) > a
fst (x,y) = x
snd :: (a,b) > b
snd (x,y) = y
fst :: (a,b) > a
fst (a,b) = a
snd :: (a,b) > b
snd (a,b) = b
Currying

Most programming languages allow functions to have any number of arguments.

But this turns out to be unnecessary: we can restrict all functions to have just one argument, without losing any expressiveness.

This process is called Currying, in honor of Haskell Curry.

The technique makes essential use of higher order functions.

It has many advantages, both practical and theoretical.

A function with two arguments
You can write a definition like this, which appears to have two arguments:
f :: Int > Int > Int
f x y = 2*x + y
But it actually means the following:
f :: Int > (Int > Int)
f 5 :: Int > Int
The function takes its arguments one at a time:
f 3 4 = (f 3) 4
g :: Int > Int
g = f 3
g 10  > (f 3) 10  > 2*3 + 10
Grouping: arrow to the right, application left

The arrow operator takes two types , and gives the type of a function with argument type and result type

An application applies a function to an argument

Note that for both types and applications, a function has only one argument

To make the notation work smoothly, arrows group to the right, and application groups to the left.
f :: a > b > c > d
f :: a > (b > (c > d))
f x y z = ((f x) y) z
Type classes and adhoc polymorphism
The type of
Note that has the following type, and there is no restriction on what types and could be.
fst :: (a,b) > a
What is the type of ? Could it be
(+) :: Int > Int > Int
(+) :: Integer > Integer > Integer
(+) :: Ratio Integer > Ratio Integer > Ratio Integer
(+) :: Double > Double > Double
(+) :: a > a > a  Wrong! has to be a number
Type classes
Answer: has type for any type that is a member of the type class .
(+) :: Num a => a > a > a

The class is a set of types for which is defined

It includes , , , and many more.

But does not contain types like , , , and many more.
Two kinds of polymorphism

Parametric polymorphism.

A polymorphic type that can be instantiated to any type.

Represented by a type variable. It is conventional to use , , ,

Example: can take the length of a list whose elements could have any type.


Ad hoc polymorphism.

A polymorphic type that can be instantiated to any type chosen from a set, called a “type class”

Represented by a type variable that is constrained using the notation.

Example: says that can add values of any type , provided that is an element of the type class .

Type inference

Type checking takes a type declaration and some code, and determines whether the code actually has the type declared.

Type inference is the analysis of code in order to infer its type.

Type inference works by

Using a set of type inference rules that generate typings based on the program text

Combining all the information obtained from the rules to produce the types.

Type inference rules
The type system contains a number of type inference rules, with the form
Context

Statements about types are written in the form similar to

This means ``if you are given a set of types, then it is proven that has type .
Type of constant
If we know the type of a constant (for example, we know that ), then this is expressed by saying that there is a given theorem that . Furthermore, this holds given any context .
Type of application
If is a function with type , then the application of to an argument of type gives a result of type .
Type of lambda expression
We have a context . Suppose that if we’re also given that , then it can be proven that an expression . Then we can infer that the function has type .
© University of Glasgow