We use cookies to give you a better experience. Carry on browsing if you're happy with this, or read our cookies policy for more information.

Skip main navigation

Types, lambda functions and type classes

Types, lambda functions and type classes
Detail of temple doors receding into the distance
© University of Glasgow

Function types

  • Ordinary data types are for primitive data (like \(Int\) and \(Char\)) and basic data structures (like \([Int]\) and \([Char]\)).
  • 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. \(Int \rightarrow String\).
  • We now look at function types in more detail.

Lambda expressions

  • Lambda expressions (named after the greek letter \(\lambda\)) play a very important role in functional programming in general and Haskell in particular.

Named and anonymous expressions

  • You can give a name \(sum\) to an expression \(2+2\):
 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 = e2-e4
e6 = sqrt e5
e7 = e1+e6

Some background

  • Sometimes in a mathematics or physics book, there are statements
    like “the function \(x^2\) is continuous\(\ldots\)”
  • This is ok when the context makes it clear what \(x\) is.
  • But it can lead to problems. What does \(x*y\) mean?
    • Is it a constant, because both \(x\) and \(y\) have fixed values?
    • Is it a function of \(x\), with a fixed value of \(y\)?
    • Is it a function of \(y\), with a fixed value of \(x\)?
    • Is it a function of both \(x\) and \(y\)?
  • In mathematical logic (and computer programming) we need to be
    precise about this!
  • A lambda expression \(\backslash x \rightarrow e\) contains
    • An explicit statement that the formal parameter is \(x\), and
    • the expression \(e\) 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 :: Char->String
f x = x:" There is a kind of character in thy life"

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 \(a \rightarrow b\), and gives the
    type of a function with argument type \(a\) and result type \(b\)
  • An application \(e_1\; e_2\) applies a function \(e_1\) to an argument
    \(e_2\)
  • 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 ad-hoc polymorphism

The type of \((+)\)

Note that \(fst\) has the following type, and there is no restriction on
what types \(a\) and \(b\) could be.
 fst :: (a,b) -> a
What is the type of \((+)\)? Could it be\(\ldots\)
 (+) :: 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 \(a \rightarrow a \rightarrow a\) for any type \(a\)
that is a member of the type class \(Num\).
 (+) :: Num a => a -> a -> a
  • The class \(Num\) is a set of types for which \((+)\) is defined
  • It includes \(Int\), \(Integer\), \(Double\), and many more.
  • But \(Num\) does not contain types like \(Bool\), \([Char]\), \(Int\rightarrow Double\), 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 \(a\), \(b\), \(c\), \(\ldots\)
    • Example: \(length :: [a] \rightarrow Int\) 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 \(\Rightarrow\) notation.
    • Example: \((+) :: Num\, a \Rightarrow a \rightarrow a \rightarrow a\) says that \((+)\) can add values of any type \(a\), provided that \(a\) is an element of the type class \(Num\).

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
\[\frac {\hbox{assumption — what you’re given}} {\hbox{consequence — what you can infer}}\]

Context

  • Statements about types are written in the form similar to \(\Gamma \vdash e :: \alpha\)
  • This means "if you are given a set \(\Gamma\) of types, then it is proven that \(e\) has type \(\alpha\).

Type of constant

\[\frac {\hbox{$c$ is a constant with a fixed type $T$}} {\Gamma \vdash c :: T}\]
If we know the type \(T\) of a constant \(c\) (for example, we know that \(‘a’ :: Char\)), then this is expressed by saying that there is a given theorem that \(c :: T\). Furthermore, this holds given any context \(\Gamma\).

Type of application

\[\frac {\Gamma \vdash e_1 :: (\alpha \rightarrow \beta) \qquad \Gamma \vdash e_2 :: \alpha } {\Gamma \vdash (e_1 \ e_2) :: \beta}\]
If \(e_1\) is a function with type \(\alpha \rightarrow \beta\), then the application of \(e_1\) to an argument of type \(\alpha\) gives a result of type \(\beta\).

Type of lambda expression

\[\frac {\Gamma, x :: \alpha \quad \vdash \quad e :: \beta} {\Gamma \vdash (\lambda x \rightarrow e) :: (\alpha \rightarrow \beta)}\]
We have a context \(\Gamma\). Suppose that if we’re also given that \(x :: \alpha\), then it can be proven that an expression \(e :: \beta\). Then we can infer that the function \(\lambda x \rightarrow e\) has type \(\alpha \rightarrow \beta\).
© University of Glasgow
This article is from the free online

Functional Programming in Haskell: Supercharge Your Coding

Created by
FutureLearn - Learning For Life

Our purpose is to transform access to education.

We offer a diverse selection of courses from leading universities and cultural institutions from around the world. These are delivered one step at a time, and are accessible on mobile, tablet and desktop, so you can fit learning around your life.

We believe learning should be an enjoyable, social experience, so our courses offer the opportunity to discuss what you’re learning with others as you go, helping you make fresh discoveries and form new ideas.
You can unlock new opportunities with unlimited access to hundreds of online short courses for a year by subscribing to our Unlimited package. Build your knowledge with top universities and organisations.

Learn more about how FutureLearn is transforming access to education