
© Wim Vanderbauwhede
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 = e2-e4
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 ad-hoc 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