Haskell Guide: Types, Lambda Functions and Type Classes

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]), (Intrightarrow 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).