Learning goals

Haskell:

  • To be able to explain and use the central notions of types in Haskell – basic types, list types, function types and tuple types
  • To be able to explain and use curried and uncurried functions and how these notions relate to higher-order functions
  • To be able to explain and use the notion of type classes
  • To be able to explain the notions of polymorphism and overloading (parametric and ad hoc-polymorphism), the difference between them and the relationship to type classes

The theoretical foundations:

  • To be able to explain and use the syntax and reduction semantics of the pure lambda-calculus
  • To be able to explain why renaming of bound variables is a necessary notion

Haskell

Types

A type is name for collection of related values.
E.g. Bool contains False and True.

e :: t means that e has type t.

Haskell is strongly typed as type errors are found at compile-time.

A list is a sequence of values of the same type: [t] is the type of list with elements of type t.

A tuple is a sequence of values of (possibly) different types: (False, 'a', True) :: (Bool, Char, Bool).

A function is a mapping from values of one type to values of another type: even :: Int -> Bool.
You can do function with muliple arguments or results by using lists or tuples.

Haskell has multiple type classes, e.g.

  • Num — numeric types
  • Eq — equality types
  • Ord — ordered totally (linearly) types. Strings, lists, and tuples are lexicographically ordered (same was as words in a dictionary). Comparison occurs like you’d compare strings. One character at a time.
  • Show — types whose values can be converted to strings of characters
  • Read — types whose values can be converted from strings of characters
  • Integral — types that are instances of Num but are integers
  • Fractional — types that are instances of Num but are fractional types

Curried Functions

You can also have functions with multiple arguments by returning functions as results.

add' :: Int -> (Int -> Int)
add' x y = x+y -- takes int x and returns function add' x. That takesan integer y and returns x+y.
-- Haskell says the type of add' is add' :: Num a => a -> a -> a

In JS, this would be const add = x => y => x + y.

Conventions

  • The arrow → associates to the right. Int -> Int -> Int -> Int means Int -> (Int -> (Int -> Int)).
  • Function application associates to the left. mult x y z means ((mult x) y) z.

Polymorphic Functions

A function is polymorphic if its type contains one or more type variables. length :: [a] -> Int is polymorphic. It doesn’t care which type of list you give it. So now a is a type variable.

Overloaded Functions

A polymorphic function is overloaded if its type contains one or more class constraints.

(+) :: Num a => a -> a -> a means for any numeric type a, (+) takes two values of type a and returns a value of type a.

The => defines a class constraint: everything before it is part of the constraint.

Lambda Calculus

An expression can be 3 things: a variable, abstraction, or application.

$\lambda x.e_{1}$ denotes a function with formal parameter $x$ and body $e_{1}$.
Scope of $x$ is all of $e_{1}$, but parentheses can be introduced to delimit scope.

$e_{1}e_{2}$ denotes that function $e_{1}$ is to be applied to argument $e_{2}$.

Scope rules: In $\lambda x.e$, the scope of the Formal parameter $x$ is the body $e$ of that abstraction. We say $x$ is bound in $e$.

But in $\lambda x.xy$, $x$ is bound but $y$ is not—so it’s free.

Beta-reduction
This is the most important rule. There are multiple rules in the reduction relation, but this one is central.
The reduction relation is how an expression can be reduced to some other expression.

(Beta)(λx.e1)e2e1[xe2](\text{Beta}) \qquad (\lambda x.e_{1})e_{2}\Rightarrow e_{1}[x\mapsto e_{2}]

It says that if we have the application $(\lambda x.e_{1})e_{2}$, we can substitute the formal parameter $x$ with $e_{2}$ inside the body $e_{1}$.
This is beta-reduction: if we apply a function to an argument, we substitute the formal parameter by the actual parameter. This is the call-by-name parameter mechanism (SS 13 - Parameter Mechanisms).

An expression of this form is called a redex.
A redex is a subexpression for which reduction is possible. If the reduction is a $\beta$-reduction, it’s a $\beta$-redex. It stands for reducable expression.

We need some more rules now:

(Left)e1e1e1e2e1e2(\text{Left})\qquad \frac{e_{1}\Rightarrow e_{1}'}{e_{1}e_{2}\Rightarrow e_{1}'e_{2}}
(Right)e2e2e1e2e1e2(\text{Right})\qquad \frac{e_{2}\Rightarrow e_{2}'}{e_{1}e_{2}\Rightarrow e_{1}e_{2}'}

The left part of the application is what should become a function (abstraction).
We could also reduce to the right component.

In abstraction $\lambda x.e$, the $x$ is called a binding occurrence of $x$. If the same $x$ occurs inside $e$, it’s called a bound occurrence of $x$. A binding occurrence is like a placeholder—the name isn’t important. Just like parameter names in functions, it doesn’t matter what they’re called: they shouldn’t conflict with outside variable names.

If an expression $e_{2}$ can be obtained from some other expression $e_{1}$ by systematically renaming zero or more binding occurrences and their bound occurrences, $e_{1}$ and $e_{2}$ are $\alpha$-convertible, and write $e_{1}\equiv_{a}e_{2}$.

Examples

  • Increment by 1: $\lambda x.x+1$
  • Sum: $\lambda x.\lambda y.x+y$
  • Square: $\lambda x.x^{2}$
  • Identity function: $\lambda x.x$

Applying a function on another expression:

(λx.x2)7(\lambda x.x^{2})7

The above gives 49.

Lambda Calculus | Brilliant Math & Science Wiki
Lambda Calculus Calculator

ELI5

Abstractions are function definitions, and are denoted by $\lambda$. After the symbol you write the input variables, followed by a dot, and then the output of a function where you describe what you want to get (the body of the function).

Variables are the same as variables in programming languages. They contain values. The scope of a variable is defined by its closest function or parentheses. Variables can be free or bound. Bound variables are those used in its scope after it was delared in the closest function input, otherwise it’s free. In the following lambda, $x$ is bound and $y$ is free: $\lambda x.xy$

A Lambda term is a basic entity. It can be a variable or function. So any variable, application, or abstraction is a valid term. These can be given names for easier reusability, e.g. $I := \lambda x.x$, for the identity term.

Alpha conversion (alpha renaming) says that names of bound variables in abstraction can be changed. Variables not bound in abstractions don’t work.

Function is a process of associating input to output. But here, functions are anonymous (can’t be given names), can take only one variable, and are treated as first-class values, so they can be both inputs and outputs of functions.

Application is applying a lambda term to another. To write it, just write the terms with whitespace between them: $x\ y$.

More than 1 argument through currying:
$\lambda xy.x$ becomes $\lambda x.\lambda y.x$.

To make a function that takes multiple arguments, make a function that takes the first argument, and returns a function which takes the second argument and returns an output.

Substitution
Replacing all free occurrences of a variable in the expression with another expression.

Beta-reduction
The process of applying a variable to a function.
Like calling a function with an argument.
E.g. multiplyByFive(2) would look like:

(λx.x5) 25210(\lambda x.x*5)\ 2\rightarrow 5*2\rightarrow 10

When you apply a function to a term, take the function’s body and run it with the applied argument as an input.

Recursion
A function using itself.
To do this in a language where every function is anonymous, describe a function and then describe it again in its argument:

Y:=λz.(λx.z (x x)) (λx.z (x x))Y:=\lambda z.(\lambda x.z\ (x\ x))\ (\lambda x.z\ (x\ x))

This is the Y combinator (fix-point combinator).

Exercises

1. Write down Haskell definitions of quango and tango that have the following types; it is not important what the definitions do as long as they are type correct

quango :: a -> [a]
tango :: Num p1 => (a, b) -> p2 -> p1

Are quango and tango polymorphic? If so, tell us if for each of them if this involves parametric Polymorphism or overloading (ad hoc Polymorphism) or maybe both — and how. If not, tell us why.

Answer

quango :: a -> [a]
quango a = [a]

tango :: Num p1 => (a, b) -> p2 -> p1
tango (a, b) p2 = 1

Yes, they are. Both involve typed variables.
quango is parametric polymorphism, as it doesn’t matter which value is given as argument, it simply returns a list of that type.

And tango is overloaded as it contains class constraints in its type.

2. Find a terminating reduction sequence of the lambda-expression

(λx.xy)(λz.(λu.uu))(\lambda x.xy)(\lambda z.(\lambda u.uu))

To do this, use the reduction rules of the note.

Answer

It reduces to $xy$ and I have no idea why.

1. What is the type of this function

twice f x = f(f(x))

-- Initial guess
twice :: f -> x -> f(f x)

-- Actual answer
twice :: (t -> t) -> t -> t

It is parametric polymorphic, as it contains a type variable.

How would you go about figuring this out? First, observe that the function takes two arguments. Since functions in Haskell take exactly one argument, we know that it returns a function which takes the second argument.

So we can infer the following:

twice::tftxtrtwice :: t_{f} \rightarrow t_{x}\rightarrow t_{r}

So the question is, what is $t_{f}$, $t_{x}$, and $t_{r}$?
Well, in the result, you see a function application, which is an argument of another function application.
We know that $f$ is a function, just from the syntax. So $f:t_{a}\rightarrow t_{b}$

From page 23 in the book. we know that if a function is of type $f::A\rightarrow B$, and its argument has type $x :: A$, then $f\ x :: B$.

So in this case, $x :: t_{a}$ and $f(x) :: t_{b}$.
And $f(f(x))::t_{b}$ and $f(x)::t_{a}$.
Otherwise we couldn’t apply $f$ to $f(x)$.
And from this we observe that $f(x)::t_{b}=t_{a}$. They must be the same type.
So now we know that $t_{r} = t_{a}$, and $t_{x}$ is also $t_{a}$.
And then it must be the case that $t_{f}=(t_{a}\rightarrow t_{a})$.

2. What is the type of the funtion

dingo (x,y) = [x,y]

--- Initial guess ✅
dingo :: (t, t) = [t]

Because even if tuples can take different types, lists cannot. This is parametric polymorphic, as it a type variable.

3. A famous influencer…

defined a Haskell function bighead that can tell us how many elements in a list xs are greater than the head of xs. As an example of the behavior of the function, the result of bighead [7,4,5,8,9] is 2. They claim the type os [Num] -> Num. Why is this incorrect?

Answer

Ehh, the list can be empty?
It isn’t just any number, but an integer it spits out?
I’d say that the type is

[Num] -> Int

But that’s actually wrong. It’s more like

bighead :: (Num a, Ord a) => [a] -> Int
bighead xs = count
    where   h = head xs
            count = length [e | e <- tail xs, e > h]

4. Why are function types not allowed to be members of the type class Eq?

The Eq type class checks equality.
How can you ever know if two functions are equal?
That is impossible.
Can encounter halting problen when checking equality of functions.

a. What is the type of mango 14

mango x y z = x * y + z - 42

What is the type of mango 14?

--- Initial guess
mango 14 :: y -> z -> Num

--- Answer
mango 14 :: Num a => a -> a -> a

I got it wrong in that it should have just been a class constraint for a single type variable, because we’d expect all the inputs to be numeric for this function to work.

b. Write a definition of a function bingo

that has the following type. Definition doesn’t matter as long as it’s type correct:

bingo :: a -> a

Answer

bingo a = a

It’s parametric polymorphism, as it has a type variable.

c. Suppose you want to define a function thesame

that takes a list of pairs xs and gives us the list of pairs whose first and second component are the same

for example, we want thesame [(1,2),(4,4),(6,7),(17,17)] to return [(4,4),(17,17)]

What should the type of thesame be?

Answer

thesame [(a, b)] -> [(a,a)]

d. Here is a Haskell expression

[(+),(*),(+),(-)]

What does it contain and what is the type of the expression?

What can you say about the type of [(+), (*), (+), (-), (++)]

Answer 1

It’s a list of functions.
Not wrong…
[(+),(*),(+),(-)] :: Num a => [a -> a -> a]

But the real answer:
Check page 34 in the book.
There the types of these functions are given.
The type of the list is

[(+), (*), (+), (-)] :: Num a => [a->a->a]

Answer 2

Also a list of functions?
Not wrong…
[(+),(*),(+),(-), (++)] :: Num [a] => [[a] -> [a] -> [a]]

e. Here is a term in the lambda-calculus

(λx.xx)(λx.xx)(\lambda x.x x)(\lambda x.x x)

Are the bound variables in the term distinct? If not, rename so they are. Then find a reduction step that the term can take.

Answer

They are distinct. Recall the scope rules for the bound variables.

Reduction step reduces to $x x$ by beta-reduction.
Left fn takes right fn as input.

f. Suppose you want to define a function map that takes a function f and a list xs and returns the list where f has been applied to every element in xs

mapp :: (i -> o) -> [i] -> [o]
mapp f xs = [f x | x <- xs]