General Functional Programming

Imperative vs Functional

Imperative	Functional
Mutation of state	Reduction of expressions
Tell the computer how you want to do something	Tell the computer what you want to compute and let it work out how to do it
Statements executed in order specified	Sub-expressions can often be evaluated in an arbitrary order
Loops	Recursion

The Compiler

Haskell is a statically typed functional programming language. This means that types are known at compile-time instead of run-time.

This allows the GHC compiler to help us write better programs. When our code is compiling

It first goes through a parser that converts ASCII source code into data in memory.
Then the GHC checks types and infers missing ones.
Types are then erased after the type checking phase, and the compiler will generate binaries for the CPU to be able to run the program. (Types are not available at runtime – this is type erasure)

Expressions and definitions

Haskell evaluates programs by “reducing” expressions to a “normal” (simplest) form in a lazy manner. This is when a complicated statement has the rules defined by the language and the rest of the program applied to it to reduce its complexity, as it is a declarative language, for example 2+2 would be reduced to 4 by applying the definition of the + function.

Definitions are when expressions are assigned to named variables, so they can be referenced elsewhere without having to be defined again inline

Anonymous functions

The \ is used to resemble the Lambda character from Lambda calculus, and it denotes a function without a name, which is just a transformation on an argument. For example, a function to multiply a parameter by two can be written as:

\x -> x * 2

All functions in Haskell are actually just anonymous functions, which are assigned to variables, as functions are treated as first class objects, but for simplicity and neatness, we needn’t define them this way in code, we can instead use syntactic sugar

Syntactic sugar for functions

Haskell syntax can be verbose if they are written using only anonymous nomenclature, so there is “syntactic sugar”, which can be used to simplify how things are written, for example, the following statements are equivalent

Function definitions can be expressed in various ways. Internally, they are allocating anonymous functions names, but syntactic sugar can be used to make this prettier. For example, the following two functions are equivalent:

x = \a -> a + 1
x a = a + 1

Currying

The process of converting a function which takes multiple arguments into a sequence of functions, each of which take one argument

In Haskell, we fundamentally only create functions which apply an operation to a single input value, and generate a single output value.

We can make functions which look like they take multiple arguments by having a function which takes a parameter, and returns another function, which is specialised based on that parameter. Then, the second (or nth) parameter can be applied to this returned function, yielding the final value.

For example, to write a function to add two numbers, we can say:

add :: Int -> Int -> Int
add = \x -> \y -> x + y

When this is evaluated, the first parameter would “specialise” the function, giving:

(add 5) :: Int -> Int
add 5 = \x -> x + 5

So we can see when the first parameter is evaluated, another function is returned, which can then be evaluated with the next parameter. Then, with the second parameter, it just resolves to a single value:

(add 5 6) :: Int
add 5 6 = 6 + 5

This process is called “partial application”, as each parameter is “partially applied” to the function

Uncurry

Contrastingly, there is a function uncurry that converts a curried function and converts it into a function on pairs.

uncurry :: (a -> b -> c) -> (a,b) -> c

What this does it to make it more like function in mathematics, where arguments are taken together.

f (a,b) = a + b 
	-- vs -- 
f = \a -> \b -> a + b

Conditionals

In function definitions, we often want to be able to write conditional statements. For example, if we want to implement the “not” boolean operator, we might say “if the argument is True, then False, otherwise, True”. This can be written in Haskell in a number of ways:

If..then..else statements
```
not' = \x -> if True
                then False
                else True
```
This can then be re-written using syntactic sugar to an in-line expression
```
not' x = if True then False else True
```
It is worth noting that if an if..then..else statement returns a boolean value, we should always try to replace it with just a simple expression, for example, if x==5 then True else False should be written as x==5.
Guards, which similarly act like syntactic sugar for conditional expressions
```
min x y | x < y		= x
        | otherwise	= y
```

Case statements

not' = \x -> case x of
                True -> False
                False -> True

Lists

In Haskell, the list data type is implemented as a linked list. This effects how they should be used efficiently, for example, indexing inefficient, but looking at the first item is very efficient

Lists are homogenous, meaning all elements must have the same data type. As a result of this, the type of a list is the polymorphic type signature [] :: [a], since they can store any type, but each element must have the same type

Lists are almost always written with their syntactic sugar, but they are in fact constructed by prepending elements to an empty list

x = [1,2,3]
x = 3 : (2 : (1 : []))

The : or “cons” is used as an infix operator to prepend elements to the list, building it up from an empty list

This relates to how list data type is implemented as a linked list, as it encodes the fact that items are added as the head of the linked list sequentially
The type of the “cons” operator is (:) :: a -> [a] -> [a], as it takes an element to prepend, and a list containing the same type, and returns a list of that type

Ranges

Ranges are a way of generating lists, rather than having to explicitly enumerate them. Haskell can handle ranges for many data types, and will infer patterns from them. For example

> [1..4]
[1,2,3,4]
> ['a'..'c']
['a','b','c']
> [1,3..10]
[1,3,5,7,9]

The last example shows the way the compiler can infer patterns - it is effective, but can only handle fairly simple patterns.

Since Haskell is lazily evaluated, it can store ranges of infinite length, and the data will only be used as it is needed

> [0..]
[0,1,2,3,4,5,...]		-- takes infinite time to print all numbers out
> take 3 [0..]
[0,1,2]					-- takes finite time to pull numbers off the front of an infinite array

List comprehensions

List comprehensions are a further way to generate lists, and offer a greater ability to select and filter the data. They have the general form:

[expression | generator(s) (predicate)]

They have a large number of variations, including:

Expressions can be applied to the values being iterated over

[even n | n <- [0..5]]
=> [True,False,True,False,True,False]

Multiple generators can be used
```
[n * m | n <- [0..2], m <- [0..2]]
=> [0,0,0, 0,1,2, 0,2,3]
```
where every m is iterated over for each n
Variables to the left are in scope of those to the right, so the following is also valid
```
[n * m | n <- [0..2], m <- [0..n]]
=> [0,0,1,0,2,4]
```
The left hand side of a generator can be pattern matched on
```
[x | (x:xs) <- [[1,2,3], [4,5,6,7]]]
=> [1,4]
```
Finally, predicates can be used along with generators to select whether a value being iterated over should be included in the list
```
[x | x <- [0..5], even x]=> [0,2,4]
```

Type Classes

Type class constraints are used to restrict type variables to only types which support the functions or operators specified by the type class.

Num is a type class in the Standard Library

Like names of types, type class names must start with an upper-case character.

Type Class Definitions

In a type class definition, we define the method typings that an arbitrary type a must implement to be an instance of that type class.

Example.

class Num a where
  (+) :: a -> a -> a
  (-) :: a -> a -> a
  abs :: a -> a
  ...

Num is the name of the type class we are defining.
a is a type variable.
The definitions are the typing of the methods that a Num must adhere to.

Type Instance

When we define an instance of a type class, we have to adhere to the typing of the method(s) in the type class definition.

class Show a where
  show :: a -> String
  
instance Show Bool where
  show True  = "True"
  show False = "False"

In a Haskell module, there are a bunch of definitions of expressions. If we have a definition for something – we can refer to it by its name in the program. The Haskell compiler works out the typing for each definition is – when we use it it checks if the type is compatible with the expression.

Hence, we say that a type class brings function typings into scope.

(+) :: Num a => a -> a -> a
(-) :: Num a => a -> a -> a
abs :: Num a => a -> a

Num a => is a type class constraint.

Constraints on instances

You can also place constraints on instances.

Example. Let’s say we want to define an instance of Show for pairs.

instance Show (a,b) where
  show (x,y) = ???

Because we are using polymorphic types a and b, we obviously can’t pattern match on all possible values. Hence, the best way to do this is to place constraints that say both a and b must be instances of Show themselves.

instance (Show a, Show b) => Show (a,b) where
  show (x,y) = "(" ++ show x ++ "," ++ show y ++ ")"

Superclass Constraints

Sometimes, certain type classes have a superclass constraint stating that a type must also be an instance of a superclass to be an instance of the current class.

class Eq a => Ord a where
  (<)  :: a -> a -> Bool
  (<=) :: a -> a -> Bool
  ...

In order for a to be an instance of Ord, it must also be an instance of Eq.

As a result, an Ord constraint on a function implies an Eq constraint

greaterOrEqual :: Ord a => a -> a -> Bool
greaterOrEqual x y = x > y || x == y

Polymorphism

Parametric polymorphism

Allows us to reuse the same data structure for different types of elements. (Generics in Java)

Example of Parametric Polymorphism in Haskell

-- The identity function works on elements of any type
id :: a -> a
id x = x
-- Same as head function, works on lists that contain any type
head :: [a] -> a
head (x:xs) = x

Ad-hoc polymorphism

A kind of polymorphism that is open to future extension.

In Haskell, type class constraints is called ad-hoc polymorphism as you can define a function that works with a certain type class K, but does not necessarily work with any type just yet. In the future, as long as you define an instance of K for an arbitrary type, this function will accept/work with this arbitrary type.

Subtype polymorphism

A synonym of this is dynamic polymorphism in Java.

Associativity

Function associativity binds the strongest.

Haskell	Maths
`f x * g y`	$f(x) \times g(y)$

Function expressions associates to the right.

xor = \a -> \b -> (a || b) && not (a && b)
-- is the same as 
xor = \a -> (\b -> (a || b) && not (a && b))

Function application associates to the left.

xor True True
-- is the same as
(xor True) True

Function types associates to the right.

xor :: Bool -> Bool -> Bool
-- is the same as 
xor :: Bool -> (Bool -> Bool)

Lazy Evaluation & Recursion

Evaluation Strategies

Evaluation strategies determine the order in which we reduce expressions. An expression that can be reduced is called a redex.

Strictness

A programming language is strict if only strict functions (functions whose parameters must be evaluated completely before they may be called) may be defined by the user.

Call-by-value

A strict evaluation strategy where all function arguments are reduced to normal forms (values) before being passed as such to the function.

Example.

fac' :: Int -> Int -> Int
fac' 0 m = m
fac' n m = fac' (n-1) (n*m)

   fac 2
=> fac' 2 1
=> fac' (2-1) (2*1)
=> fac' (1) (2*1)
=> fac' 1 2
=> fac' (1-1) (1*2)
   ...

Call-by-name

A non-strict evaluation strategy where expressions are given to functions as arguments are not reduced before the function call is made.

Expressions are only reduced when their value is needed.

When is a value needed?

A case expression is the only thing that enforces the evaluation of a particular expression (we’re only evaluating something if its in a case expression). We need the value of an expression when we cannot proceed with the case expression until we reduce the expression.

fac' :: Int -> Int -> Int
fac' 0 m = m
fac' n m = fac' (n-1) (n*m)

   fac 2
=> fac' 2 1
=> case 2 of
     0 -> 1
     _ -> fac' (2-1) (2*1)
=> fac' (2-1) (2*1)
=> case 2-1 of
     0 -> 2*1
     _ -> fac' ((2-1)-1) ((2-1)*(2*1))
=> case 1 of
     0 -> 2*1
     _ -> fac' ((2-1)-1) ((2-1)*(2*1))

When 2-1 (from the 2nd last step) is reduced to 1, it is the first time in the example that an expression is reduced. This only happens because the value of the redex 2-1 is needed for the case expression to continue.

CBN vs CBV

call by name vs call by value

In a language which uses call-by-name evaluation, such as Haskell, expressions are only evaluated when it becomes clear that their value is needed. In call-by-value, function arguments are always evaluated before the function is called.

Call-by-value	Call-by-name
Reduce function arguments to normal forms before calling the function	Only reduce expressions when their value is needed
We may evaluate arguments even if they are never needed.	We may end up reducing the same expression over and over.

Lazy evaluation

From above, we see that call-by-name and call-by-value each have its flaws.

This is essentially call-by-name + sharing, where we avoid duplicate evaluation but also only ever evaluate expressions that are needed.

Lazy evaluation is the default evaluation strategy in Haskell. Since Haskell is a non-strict programming language, it can be strict if the compiler (the compiler does everything for us 🥳) thinks its better or if we force it to be strict with the $! operator.

This is the technique that helps us avoid duplicate evaluation.

Sharing turns arguments to function into local definitions.

TLDR. Normally for call-by-name, expressions are represented by closures (memory locations on the heap) and pointers to them are then passed to functions as arguments. If an argument is used more than once within a function, then it will be evaluated multiple times. Sharing is an optimisation which allows these closures to be updated with their result once they have been evaluated, meaning they only have to evaluated once.

                              fac' n m = case n of
fac' n m = case n of            0 -> m
  0 -> m                 ==>    _ -> let x = n - 1
  _ -> fac' (n-1) (n*m)                  y = n * m
                                     in fac' x y

This ensures that functions are always applied to either values or a variable defined in a let (or where) bound. This means that if a variable (e.g. x0 = 2-1) has to be evaluated, its RHS is evaluated (so 2-1=1) and x0 is updated with the value of the expression, so x0 = 1. Also see dynamic closures.

   fac 2
=> fac' 2 1
=> case 2 of
     0 -> 1
     _ -> let x0 = 2-1
              y0 = 2*1
          in fac' x0 y0
=> let x0 = 2-1
       y0 = 2*1
   in fac' x0 y0
=> let x0 = 2-1
       y0 = 2*1
   in case x0 of             -- x0 has to be evaluated as its value is
        0 -> y0              -- needed for the case expression to continue
        _ -> let x1 = x0-1
                 y1 = x0*y0
             in fac' x1 y1
=> let x0 = 1                -- x0 has been updated with the result of 
       y0 = 2*1              -- evaluating RHS
   in case x0 of
        0 -> y0
        _ -> let x1 = x0-1
                 y1 = x0*y0
             in fac' x1 y1
=> let x0 = 1                
       y0 = 2*1               
   in case 1 of             -- x0 can now be replaced by 1
        0 -> y0
        _ -> let x1 = x0-1
                 y1 = x0*y0
             in fac' x1 y1

When we refer to x0 again, we have access to its evaluated value (because we evaluated it before) and there will be no need to evaluate it again and again, all while using call-by-name.

Lazy evaluation Walk-through

Given the following expression, show how it is evaluated with lazy evaluation (do not skip steps).

length (take 2 (map even [1,2,3,4]))

When tackling this kind of question it is helpful to refer to the definitions of the functions that are used. These are usually specified/given to you/made by you in an earlier question, otherwise its difficult to evaluate it properly without knowing the exact definition.

Here the definitions we use are.

length :: [a] -> Int
length []     = 0
length (x:xs) = 1 + length xs

take :: Int -> [a] -> [a]
take 0 _     = []
take n []    = []
take n (x:xs) = x : take (n-1) xs

map :: (a -> b) -> [a] -> [b]
map f []     = []
map f (x:xs) = f x : map f xs

Answer.

   length (take 2 (map even [1,2,3,4]))
=> length (take 2 (even 1 : map even [2,3,4]))
=> length (even 1 : take (2-1) (map even [2,3,4]))
=> 1 + length (take (2-1) (map even [2,3,4]))
=> 1 + length (take 1 (map even [2,3,4]))
=> 1 + length (take 1 (even 2 : map even [3,4]))
=> 1 + length (even 2 : take (1-1) (map even [3,4]))
=> 1 + (1 + length (take (1-1) (map even [3,4])))
=> 1 + (1 + length (take 0 (map even [3,4]))) 
=> 1 + (1 + length [])
=> 1 + (1 + 0)
=> 1 + 1
=> 2

Questions may ask about call-by-value and call-by-name too, so know this topic well.

Closures

A structure in memory at runtime that represents a function and its environments (i.e scope).

We can think of it as an array of pointers

1st pointer points to some code
other pointers point to other closures.

Example.

not :: Bool -> Bool
not True = False
not False = True

In memory, you have a particular memory location/address that stores a pointer to the code (we don’t have to worry about where the code is.)

Every usage of not in the code is a pointer to this memory location.

Functions in Haskell (and other functional programming languages) are first class values, which means they can be returned by other functions or given to functions as arguments (higher-order-functions).

Example.

f :: Int -> a -> Int
f x = let g y = x + 5
      in g

In memory, we have a static closure of f as mentioned above for not

Initially when the program is started, there is no closure for g. Only have closures for top-level definitions like f here when program starts.
When we start evaluating f, every call to f will dynamically allocate a closure to g on the heap (this is only for that particular invocation of f)
- This closure is comprised of a pointer to code for g and a pointer to x
- The reason for this is because the body of g refers to x, which is a parameter of f.
- Because g is defined within the scope of f, it has access to whatever is in scope of f, which x is.
It doesn’t matter if the stack frame for f is removed because g still has a reference to what x was.

Dynamic Closures

length (take 2 (map even [1,2,3,4])) 
-- is translated into
let zs4 = 4 : []
    zs3 = 3 : zs4
    zs2 = 2 : zs3
    zs  = 1 : zs2
    ys  = map even zs
    xs  = take 2 ys
in length xs
-- by the compiler

When this expression gets evaluated at runtime, a closure is dynamically allocated for each of these “variables” (so zs4, zs3, … , xs).

length is just a pointer to the static closure for the length function.
xs is a pointer to the closure that is dynamically allocated for xs shown above.

Recursive Functions

In C, Java, and most imperative languages, function calls push frames onto the stack which is where local variables are stored. Each recursive function call is evaluated before the final value is calculated. To illustrate take the factorial function as an example:

int fac (int n) {
  if (n == 0) return 1;
  int r = fac(n - 1);
  return n * r;
}

In C, each value of n-1 for each call to fac is evaluated before the multiplication of n and r, so we get something like this in the stack:

-- The Stack
fac(0)  : int r = 1
...
fac(497): int r = 0
fac(498): int r = 0
fac(499): int r = 0
fac(500): int r = 0

Only when we get to the base case n==0, we get a value for r which is 1. Then the stack is popped and the next call to fac at the top will be evaluated until the initial call to fac(500). If we defined this in Haskell, this would probably look like:

fac :: Int -> Int 
fac 0 = 1
fac n = n * fac (n-1)

   fac 500
=> 500 * fac (500-1)
=> 500 * fac 499
=> 500 * (499 * fac (499-1))
=> 500 * (499 * fac 498)
=> 500 * (499 * (498 * fac (498-1)))
	 ...
=> 500 * 499 * ... * fac 0
=> 500 * 499 * ... * 1 -- multiplication can finally be evaluated
=> multiplication is evaluated

This naive way of evaluating recursion builds up large expressions (with lots of closures) because nothing forces the expressions to get evaluated at intermediate steps.

The multiplication can never be reduced until the end because at no point do we have the second argument until we reach the base case.
Hence, deep recursion in imperative languages could cause your program to run out of memory, which is called a stack overflow.

FYI. There is a “trick” called tail-call optimisation that programming languages can use to prevent a stack overflow for certain kinds of recursive functions.

In functional programming languages, tail call optimisation is often guaranteed by the language standard, as it allows tail recursion to use a similar amount of memory as a loop in an imperative language. If you are interested, read more here.

Optimised Recursive Functions in Haskell

The Haskell compiler optimises this for us by recreating the function we call (i.e fac) with another function that has an accumulating parameter.

-- Here m is the accumulating parameter
fac' :: Int -> Int -> Int
fac' 0 m = m
fac' n m = fac' (n-1) (n*m)
-- fac is then rewritten with fac'
fac :: Int -> Int
fac n = fac' n 1

What this does is that the result of earlier calls to fac is evaluated and “accumulates” in the second argument m

   fac 500
=> fac' 500 1
=> fac' (500-1) (500*1) -- 500-1 needs to be evaluated to continue
=> case x0 of           -- Since x0 = 500 - 1 and needs to be evaluated
     0 -> y0
     _ -> fac' x1 y1
   where x0 = 500 - 1
         y0 = 500*1
         x1 = x0 - 1
         y1 = x0 * y0
=> case x0 of           
     0 -> y0
     _ -> fac' x1 y1
   where x0 = 499       -- We evaluate 500 - 1 = 499, and x0 is updated with 
         y0 = 500*1     -- this new value, and now the case expression can
         x1 = x0 - 1    -- proceed
         y1 = x0 * y0
=> fac' (499-1) (499*500*1) -- This continues for (499-1), (498-1) ...
=> fac' (498-1) (498*(499*(500*1)))
   ...

As you can see, fac' forces the evaluation of the first argument at every step by pattern-matching on it. While the second argument will build up into a long list of closures if is evaluated lazily, the difference with naive recursion is that it can be forced to be evaluated because all arguments are present for multiplication.

Useful recursive functions

There are a number of recursive functions which are useful to be able to lookup to see the schema, or just to be able to reproduce in some contexts

Quick sort

    quicksort :: (Ord a) => [a] -> [a]  
    quicksort [] = []  
    quicksort (x:xs) =   
        let smallerSorted = quicksort [a | a <- xs, a <= x]  
            biggerSorted = quicksort [a | a <- xs, a > x]  
        in  smallerSorted ++ [x] ++ biggerSorted  

Implementation taken from Learn You a Haskell for Great Good! A Beginner’s Guide, Lipovaca, Miran

This can be expressed more neatly than merge sort, as due to the implementation of lists as linked lists, it is less efficient to split arrays in two in Haskell as is required for merge sort

Higher order functions

Higher order functions are functions which operate on other functions, either taking another function as a parameter, or returning one as a result

The process of currying, discussed earlier, is a higher order function, as a function takes a parameter, and returns another functioned, specialised by that parameter

Sections

Sections are partial applications of infix operators. If you give only one argument to an infix operator, it returns a function of the “missing” side of the operation, for example, if the left side of the infix exponent is given, a function taking the exponent as the parameter is returned, but if the right side is given, the function takes the base as parameter. This is written as:

> (^2)
\x -> x ^ 2

> (2^)
\x -> 2 ^ x

Examples of higher order functions

Map

A function that takes a list and a function, and returns a new list, with every element in the old one having had the function applied to it

map :: (a -> b) -> [a] -> [b]  
map _ [] = []  
map f (x:xs) = f x : map f xs  

Filter

A function that takes a list and a predicate (a function which indicates the truth value of its parameter), and returns the list containing only the true values in the original list

filter :: (a -> Bool) -> [a] -> [a]  
filter _ [] = []  
filter p (x:xs)   
    | p x       = x : filter p xs  
    | otherwise = filter p xs  

Quicksort using filter

We can neatly write sorting algorithms using this, such as quicksort (with the pivot being picked as the middle in this case)

quicksort :: (Ord a) => [a] -> [a]    
quicksort [] = []    
quicksort (x:xs) =     
    let smallerSorted = quicksort (filter (<=x) xs)  
        biggerSorted = quicksort (filter (>x) xs)   
    in  smallerSorted ++ [x] ++ biggerSorted  

Folds

Folds are a class of function which repeatedly reduce a list, having an accumulator value, and a function which takes values from the list elementwise, and combines them into the accumulator. It is described in a stack overflow answer as:

In:
    initial value
    way to combine stuff with initial value
    collection
Out:
    combined stuff

We actually write this in code using the following syntax

initialAccumulator :: a
combinationFunction :: a -> a -> a

foo :: [a] -> a
foo xs = foldr (\accumulator x -> combinationFunction accumulator x) initialAccumulator xs

There are two common implementations, foldl, and foldr, which start by applying the function to the first and last elements respectively. These two folds have different properties, and there is an additional type foldl', which strengthens the properties of foldl. Additional source #1 Additional source #2

Foldr

foldr generates the entire expression before evaluation, with foldr f z [1,2,3] evaluating to f 1 (f 2 (f 3 z))

For example foldr (+) [1..1000] evaluates as 1 + (2 + (3 + (...))). As the chain of operations doesn’t contain a redex (reducible expression) until the entire chain is built, the entire expression must be generated before it can be evaluated. This means it will cause stack overflows on large lists.

If the combination function is able to produce part of the result independent of the recursive case, so the rest of the result is never demanded, the recursion will stop, allowing use on infinite lists

foldr (\acc x -> acc + x) 0 [3,5,2,1]
=> foldr (\acc x -> acc + x) (0+1) [3,5,2]
=> foldr (\acc x -> acc + x) (2+(0+1)) [3,5]
=> foldr (\acc x -> acc + x) (5+(2+(0+1))) [3]
=> foldr (\acc x -> acc + x) (3+(5+(2+(0+1)))) []
=> (3+(5+(2+(0+1))))

Foldl

foldl applies the function as it goes along, with foldl f z [1,2,3] evaluating to f (f (f z 1) 2) 3

For example foldl (+) [1..1000] evaluates as (((0 + 1) + 2) + 3) + .... This seems like it would reduce as is goes along, as each bracket is its own redex, but due to Haskell’s lazy evaluation, it doesn’t, so it still causes stack overflows on large lists. It can never handle infinite lists, and will always recurse forever if they are given

An example case of execution is:

foldl (\acc x -> acc + x) 0 [3,5,2,1]
=> foldl (\acc x -> acc + x) (0+3) [5,2,1]
=> foldl (\acc x -> acc + x) ((0+3)+5) [2,1]
=> foldl (\acc x -> acc + x) (((0+3)+5)+2) [1]
=> foldl (\acc x -> acc + x) ((((0+3)+5)+2)+1) []
=> ((((0+3)+5)+2)+1)

Foldl’

foldl' is a modification of foldl which forces Haskell to evaluate each redex as it goes, despite lazy evaluation, allowing avoiding stack overflows for large lists, but inherently sacrificing the other benefits of lazy evaluation

An example case of execution is:

foldl (\acc x -> acc + x) 0 [3,5,2,1]
=> foldl (\acc x -> acc + x) (0+3) [5,2,1]
=> foldl (\acc x -> acc + x) 3 [5,2,1]
=> foldl (\acc x -> acc + x) (3+5) [2,1]
=> foldl (\acc x -> acc + x) 8 [2,1]
=> foldl (\acc x -> acc + x) (8+2) [1]
=> foldl (\acc x -> acc + x) 10 [1]
=> foldl (\acc x -> acc + x) (10+1) []
=> 11

We can see this differs from the standard foldl, as at each step it reduces the accumulated expression

Function composition

A function which chains the output of one function into the input of the other

(.) :: (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)

We can then use this to write code more neatly with fewer brackets, for example, the following statments are equivalent:

f (g (h x))
f . g . h x

Data Types

Data Type Definition

data Bool = False | True
data Module = CS141 | CS256 | CS118 | CS132 ...
data Unit = Unit
not :: Bool -> Bool
not True  = False -- Pattern matching on constructors
not False = True  -- Constructors as values

This is the definition of the data type for Bool. “Bool” is the name of the type, and “False” and “True” are data constructors.

We can pattern-match on data constructors
We can use data constructors as values
We can have as many number of data constructors as we want
Name of the type is not the same as the data constructor (although we can name them the same)
Data constructors can have parameters.

Parametrised Data Constructors

We can add parameters to a data constructor by adding their types after the constructor’s name.

data Shape = Rect Double Double
           | Circle Double

We can treat data constructors like a function.

Rect   :: Double -> Double -> Shape
Circle :: Double -> Shape

Recursive Data Types

data Nat = Zero | Succ Nat

data BinTree a = Leaf a | Node (BinTree a) (BinTree a)

Type Aliases

We can define aliases for a certain type.

type String = [Char]
type Memory = [(String, Int)] -- Recall coursework 2
type Predicate a = a -> Bool

Derivable Type Classes

Type Classes	Extension needed
`Eq`, `Ord`, `Enum`, `Bounded`, `Show`, `Read`
`Typeable`, `Data`	`XDeriveDataTypeable`
`Generic`	`XDeriveGeneric`
`Functor`	`XDeriveFunctor`
`Foldable`	`XDeriveFoldable`
`Traversable`	`XDeriveTraversable`

Equational Reasoning in Haskell

Intro

Functions in Haskell are pure – they have no side-effects and their results only depend on their arguments. Because of that we are able to easily prove formal properties about our functions.

We can’t use equational reasoning on impure functions, because their results may depend on values other than the arguments, thereby rendering any properties we prove invalid.

Techniques

Direct proof

The steps for performing a direct proof are:

Write down the types of all of the variables
Write down the definitions of all of the relevant functions
Repeatedly apply internal steps to get from the LHS to the RHS
- It is often worth working from both sides in towards the middle

The are only a small number of internal steps that can be made in a direct proof:

Function application or unapplication
Applying a known assumption
Eta-conversion
Variable renaming (alpha equivalence)
- Mostly don’t use this, as there are strict rules around it

Function application and unapplication

Consider the function definition:

double :: Int -> Int
double x = x + x

This can also be viewed as a property when reasoning about functions, allowing us to exchange the statement double x freely with x + x. This can be written as:

	double x
= {function application}
	x + x
= {function unapplication}
	double x

Non-overlapping pattern matching

The following function definition is fairly common-place:

isZero :: Int -> Bool
isZero 0 = True
isZero n = False

However, we cannot take the second statement isZero n = False in isolation when using function application/unapplication, as it is dependent on not hitting the pattern match above it, checking that it isn’t zero

Hence, it is often convenient to re-write function without implicit precedence from pattern matching, as such:

isZero :: Int -> Bool
isZero n
	| n == 0	= True
	| n /= 0	= False

Case analysis

This leads us onto case analysis, were we can apply values to a function based on the case it will take. For example, consider the function:

not :: Bool -> Bool
not False	= True
not True	= False

We can then apply cases to simplify expressions, as follows:

	not (not False)
= {application to the inner `not`}
	not True
= {application to the `not`}
	False

Applying an assumption

If an assumption, e.g. a function definition or inductive hypothesis fits the pattern of a part of the proof, it can be re-written with it - this is fairly self-explanatory

Eta-conversion

Eta conversion is the “adding or dropping of abstraction over a function” source.

This means that we can say the following are equivalent:

```
\x -> abs x
```
```
abs
```

Induction

The steps for performing a proof by induction are:

Select the variable to perform induction on. This may be the most used one, or the one which is used equally on both sides
Write out the proposition in terms of the variable to perform induction on, and with any other variables being arbitrary fixed constants of a given type
Prove the base case
1. This is normally a direct proof. However, there is sometimes an additional nested inductive proof
Prove the inductive step
1. Write out the inductive hypothesis
2. Use the inductive hypothesis in the proof of the inductive step. Commonly, the operations are in the following order:
  1. Function application
  2. Apply inductive hypothesis
  3. Function unapplication
  However, there is sometimes an additional nested inductive proof
State the conclusion that the proposition is true by induction

Examples

Direct proof

Reversing a singleton list

Consider the function to reverse a list:

reverse :: [a] -> [a]
reverse [] 	   = []
reverse (x:xs) = reverse xs ++ [x]

We can then directly prove that the reverse of a singleton list is itself

	reverse [x]
= {Using list notation}
	reverse (x : [])
= {function application of `reverse`}
	reverse [] ++ [x]
= {function application of `reverse`}
	[] ++ [x]
= {function application of `++`}
	[x]

Proof by induction

Addition on recursively defined numbers

Consider the definition of the natural numbers, and the function to add them:

-- Data type for natural numbers
data Nat = Zero
		 | Succ Nat
		 
-- Addition function
add :: Nat -> Nat -> Nath
add Zero m	   = m
add (Succ n) m = Succ (add n m)

Adding zero results in no change

Proving the statement that:

For all
	n :: Nat
	
add n Zero = n

Let P(n) be the proposition that n + Zero = n

First, consider the base case P(Zero), which is add Zero Zero = Zero

	add Zero Zero						(LHS)
= {function application of `add`}
	Zero								(RHS)

Next, consider the inductive step, showing P(n) $\implies$P(Succ n). This means that the inductive hypothesis is add n Zero = n. Hence, we want to prove add (Succ n) Zero = Succ n, which is done as follows:

	add (Succ n) Zero					(LHS)
= {function application on `add`}
	Succ (add n Zero)
= {inductive hypothesis}
	Succ n								(RHS)

By the principle of induction, since the base case P(Zero) and the inductive step P(n) $\implies$ P(Succ n) are proven, the proposition is proven for all values of n

Associativity of natural numbers

Proving the statement that:

For all
	x :: Nat,
	y :: Nat,
	z :: Nat
	
add x (add y z) =  add (add x y) z

There are three variables, and we want to show it is true for all values of all of them, but we can’t easily do induction on all of them. Since x is the first parameter in one of the two add functions on both sides, it is likely a good item to pick for induction.

Let P(x) be the proposition that add x (add y z) = add (add x y) z for some fixed y and z

First, consider the base case P(Zero), which is add Zero (add y z) = add (add Zero y) z

	add Zero (add y z)						(LHS)
= {function application on `add`}
	add y z
= {function unapplication on `add`}
	add (add Zero y) z						(RHS)

Next, consider the inductive step, showing P(n) $\implies$P(Succ n). This means that the inductive hypothesis is add x (add y z) = add (add x y) z. Hence, we want to prove add (Succ x) (add y z) = add (add (Succ x) y) z, which is done as follows:

	add (Succ x) (add y z)					(LHS)
= {function application on outer `add`}
	Succ (add x (add y z))
= {inductive hypothesis}
	Succ (add (add x y)) z
= {function unapplication on outer `add`}
	add (Succ (add x y)) z
= {function unapplication on inner `add`}
	add (add (Succ x) y) z					(RHS)

By the principle of induction, since the base case P(Zero) and the inductive step P(x) $\implies$ P(Succ x) are proven, the statement is proven for all x, and fixed arbitrary values of y and z.

This is sufficient to prove the whole statement, as y and z are fixed on both the RHS and the LHS.

Induction on lists

Consider the definition on lists, and the cons operation:

-- Data type for the list
data List a = Empty
			| Cons a (List a)

-- Cons operation on the list
data [] a = []
		  | (:) a [a]

Proving map fusion

Proving the statement that:

For all
	f :: b -> c
	g :: a -> b
	xs :: [a]
	
map f (map g xs) == map (f . g) xs

We take the following function definitions as assumptions:

map :: (a -> b) -> [a] -> [b]
map f []	 = []
map f (x:xs) = f x : map f xs

(.) :: (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)

We need to know what xs is to evaluate this statement, so we use induction on xs

Let P(xs) be the proposition that map f (map g xs) = map (f . g) xs for all xs, and some fixed f and g

First, consider the base case P([]), which ismap f (map g []) = map (f . g) []

	map f (map g [])						(LHS)
= {function application on `map`}
	map f []
= {function application on `map`}
	[]
= {function unapplication on `map`}
	map (f . g) []							(RHS)

Next, consider the inductive step, showing P(xs) $\implies$P(x : xs). This means that the inductive hypothesis is map f (map g xs) = map (f . g) xs. Hence, we want to prove map f (map g (x:xs)) = map (f . g) (x:xs), which is done as follows:

	map f (map g (x:xs))
= {function application on `map`}
	map f (g x : map g xs)
= {function application on `map`}
	f (g x) : map f (map g xs)
= {inductive hypothesis}
	f (g x) : map (f . g) xs
= {function unapplication on `(.)`}
	(f . g) x : map (f . g) xs
= {function unapplication on `map`}
	map (f . g) (x:xs)

Functors, Applicatives, Monads

Functor Factory

A type is a functor if it can represent a “context” for values of some arbitrary type that we can apply functions to.

class Functor f where
  fmap :: (a -> b) -> f a -> f b
data Maybe a = Nothing | Just a
instance Functor Maybe where

Pro Tip. When writing down the instance of a type class like functor here, always write down the specialised type signatures of the function we’re defining first

-- fmap :: (a -> b) -> Maybe a -> Maybe b
fmap f Nothing = Nothing
fmap f (Just x)  = Just $ f x

data Tree a = Leaf a | Node (Tree a) (Tree a)
instance Functor Tree where 
  -- fmap :: (a -> b) -> Tree a -> Tree b
  fmap f (Leaf x)   = Leaf (f x)
  fmap f (Node l r) = Node (fmap f l) (fmap f r)

Functor Laws

A type f is a functor if there is a function

fmap :: (a -> b) -> f a -> f b

and the following laws apply for it:

fmap id = id
fmap (f . g) = fmap f. fmap g

These laws imply that a data structure’s “shape” does not change when we use fmap - we are just operating/changing the elements inside the data structure.

Applicative Academy

A type is an applicative functor if its values represent some form of context that we can lift function application into.

class Functor f => Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b
  
data Maybe a = Nothing | Just a
instance Applicative Maybe where
  -- pure :: a -> Maybe a
  pure x = Just x
  -- (<*>) :: Maybe (a -> b) -> Maybe a -> Maybe b
  (Just f) <*> (Just x) = Just (f x)
  _        <*> _        = Nothing

Suppose that f is a function with two parameters e.g.

f :: a -> b -> c
f <$> x <*> y
= fmap f x <*> y
= pure f <*> x <*> y

Applicative Laws

In Haskell, a type f is an applicative functor if there are functions pure and <*>

class Functor f => Applicative f where
	pure  :: a -> f a
	(<*>) :: f (a -> b) -> f a -> f b

and the following laws apply for them:

             pure id <*> x = x
         pure f <*> pure x = pure (f x)
              m <*> pure y = pure ($ y) <*> m
pure (.) <*> x <*> y <*> z = x <*> (y <*> z)

Left and Right Apply

(<*) :: Applicative f => f a -> f b -> f a
x <* y = const <$> x <*> y
(*>) :: Applicative f => f a -> f b -> f a
x *> y = flip const <$> x <*> y

Limitations of Applicatives

Applicative effects cannot depend on the result of the previous computation, which is why we have monads.

Consider the example of looking up the grandmother of a person from a dictionary which maps people to their mothers. This dictionary can be represented as a value of type [(String, String)] and we can then use the lookup :: Eq a => a -> [(a,b)] -> Maybe b function from the standard library to retrieve the name of the mother of a given person:

grandmother :: String -> [(String, String)] -> Maybe String
grandmother x dict = do
  mother <- lookup x dict
  lookup mother dict

If there is no mapping for a person’s name to their mother, then Nothing is returned. Therefore, to look up a person’s grandmother, we first need to look up their mother’s name and then the name of their mother’s mother.

Writer Type

data Writer w a = MkWriter (a,w)

The writer type is a good example of a functor that is not an applicative functor.

instance Functor (Writer w) where
  fmap f (MkWriter (x,o)) = MkWriter (f x, o)

It cannot be an applicative functor because we need to be able to write an instance for pure. Looking at the typing for pure, we can see that we need to use the MkWriter constructor, which expects a pair of type (a,w) as argument. While we have a value of type a that can be given to pure as argument, we do not have a value for w.

pure :: a -> Writer w a

Hence, since it is not possible to write a suitable definition, the Writer type is not an applicative functor. Even if we find some way to write a definition, it will not obey the relevant applicative laws.

State Type

State has two parameters and therefore is a of kind * -> * -> *. From type signature of St, we can see that we are storing functions that produces pairs.

data State s a = St (s -> (a,s))
St :: (s -> (a,s)) -> State s a

runState :: State s a -> s -> (a,s)
runState (St m) = m

A value of type State s a represents a computation that accepts and initial state of type s and uses it to produce a result of type a and a resulting state of type s.

The main idea behind this is that by combining values of type State in some way, we could automatically propagate state throughout a program in a way that appears as if the state was mutable.

Monad Merry-Go-Round

A type is a monad if its value represent some form of context that permits us to apply a function to all the elements in one context, producing one new context each which can then all be joined together into one final context.

class Applicative m => Monad m where
(>>=) :: m a -> (a -> m b) -> m b

data Maybe a = Nothing | Just a
instance Monad Maybe where 
  -- (>>=) :: Maybe a -> (a -> m b) -> m b
  (Just x) >>= f = f x
  Nothing  >>= f = Nothing

You can also characterise a monad with the join function.

join :: Monad m => m (m a) -> m a
join mm = mm >>= id

(>>=) :: Monad m => m a -> (a -> m b) -> m b
m >>= f = join (fmap f m)

In theory, either function characterises a monad and can be used to define the other function. Haskell’s Monad type class requires us to define >>=, while join is defined in terms of >>=

Monad Laws

In Haskell, a type m is a monad if there are functions return and >>=

class Monad m where
  (>>=)  :: m a -> (a -> m b) -> m b
  return ::   a -> m a

and the following laws apply for them:

-- Left Identity
return x >>= f = f x
-- Right Identity
m >>= return = m
-- Associativity
(m >>= f) >>= g = m >>= (\x -> f x >>= g)

Additional resources

The following chapters in Learn You a Haskell for Great Good! A Beginner’s Guide, Lipovaca, Miran cover functors, applicative functors and monads in gratuitous detail:

However, a simpler more intuitive description of them (which does skim over some points), is available here:

Functors, applicatives and monads in pictures

Type Level Programming

Kinds

Just like how expressions have types, types have kinds.

expression :: type -- type signature
type  :: kind      -- kind signature
Bool  :: *
Maybe :: * -> *

For example, the type Bool has kind * (star) because Bool has no parameters. On the other hand, Maybe is of kind * -> * (star to star), as we know that Maybe is a type constructor and has 1 parameter.

* -> * basically says that if you give this kind a type as an argument, then it gives back a type.

[] :: * -> * is another example – given a type a to the list type constructor and it will give [a] (a list of a).

Kinds = Better Code

Kinds help us code instances better, as long as we understand it.

Monad :: (* -> *) -> Constraint
instance Monad Either where ... 
-- Error: Expected kind * -> * but Either has kind * -> * -> *

In this example, it is easy to see why we get an error, because Monad is a type class that takes a type of kind * -> * (basically a type constructor) and gives a Constraint. So giving it a type of kind * -> * -> * violates this constraint.

You can think of type classes as a constraint constructor, although this isn’t a standard term so don’t use it!

Finding the kind

In the Haskell repl, we have seen we can use :t <VALUE> to find the type of a given value or variable. Similarly, we can find the kind of a type using :k <TYPE>, and additionally reduce the type to a normal form with :kind! <TYPE>.

Type promotion

Using Haskell language extensions, we are able to create our own kinds of types. This feature is not in Haskell by default, so we need to add a language extension to use it. We can use the Haskell extension XDataKinds in three ways:

Writing the following at the top of our source file, as language pragma:
```
{-# LANGUAGE XDataKinds #-}
   
module Program where
```

Modifying the .cabal file for the entire target

library
        ...
    default-extensions: DataKinds

With flags on the command line (requires specification every time)
```
$ ghc Program.hs -XDataKinds
```

Usually we use Language Pragmas.

DataKinds is the language extension that allows us to create our own kinds.

With DataKinds enabled, each data type we define not only introduces a type with some constructor but also introduces

a new kind which has the same name as the data type
additional data types – have the same name as the data constructors but preceded with a '.
- These additional data types are of the new kind that is introduced.

Example. Here we are getting a type-level boolean of kind Bool.

data Bool = True | False
  True  :: Bool -- type signature
  False :: Bool
-- With DataKinds enabled, the 'True and 'False data types are introduced
  'True  :: Bool -- kind signature (do not confuse with typings)
  'False :: Bool

To visualise this you can look at the table below. The right-most column is what the DataKinds language extension adds in addition to what happens normally when you define a type with data.

	Normally	DataKinds Additions
Kind-Level	`*`	`Bool`
Type-Level	`Bool`	`'True` and `'False`
Value-level	`True` and `False`

GADTs

Generalised Algebraic Data Types (GADTs) allow us to define more expressive data type definitions. The language extension is GADTs.

-- ADT syntax
data Vector a = Nil | Cons a (Vector a)
  {- 
     Behind the scenes we get 
       Nil :: Vector a
       Cons :: a -> Vector a -> Vector a 
  -}
-- with GADT syntax
data Vector a where
  Nil  :: Vector a
  Cons :: a -> Vector a -> Vector a

Currently, the head function on lists will break if given an empty list. So we can fix that by returning a Maybe or Either type and then deal with the result in another function.

But GADTs together with another extension, XKindSignatures, will allow us to define a head function for Vector that will reject an empty list at compile-time – removing the need for us to handle the results of Maybe or Either.

data Vector (n :: Nat) a where
  Nil  :: Vector 'Zero
  Cons :: a -> Vector n a -> Vector ('Succ n) a
  
vhead :: Vector ('Succ n) a -> a
vhead (Cons x xs) = x

data Nat where         -- Behind the scenes we get 
  Zero :: Nat          --   'Zero :: Nat
  Succ :: Nat -> Nat   --   'Succ :: Nat -> Nat

In the new definition of Vector we have placed a specification on the 1st parameter n. (n :: Nat) essentially says that the type n has to be of kind Nat. And in the new definition of Nil and Cons, we are able to specify that Nil will only accept an element of type Vector 'Zero and Cons will always give a Vector 1 element larger.

In this example, GADTs allow us to specify more constrained return types for data constructors.

Singleton Types

Types where there is a 1:1 correspondence between types and values. Essentially a particular singleton type will only ever have one value that is associated with it.

From above we have seen that with DataKinds and GADTs we are able to encode information about the value of a certain element through its type. In specific cases, we may want to make use of this to define singleton types.

data SNat (n :: Nat) where
  SZero :: SNat 'Zero
  SSucc :: SNat n -> SNat ('Succ n)

In this example, we are defining a singleton type for natural numbers. If we try to define sone or stwo, their types will be unique.

sone :: SNat ('Succ 'Zero)
sone = SSucc SZero

stwo :: SNat ('Succ ('Succ 'Zero))
stwo :: SSucc sone

Reification

Reification is the process of converting types to values, typically using type classes.

There are a few ways to implement the instances for the type classes and one way (which is used in the lectures) is to use proxy types.

Proxy Types

We don’t have types at runtime due to type erasure, so we can’t write a function that takes types as arguments in Haskell, even though we sometimes want to.

Functions only accept arguments whose types are of kind *. Proxy types are used to establish a link between types of other kinds and types of kind *, thus “carrying” types of other kinds into the scope of a function’s type.

For example, we might want to define a function

fromNat :: forall (n :: Nat) => n -> Int

which takes a type-level natural number n of kind Nat as input and returns the corresponding Int value. However, only types of kind * have values at run-time in Haskell. Since there are no values of types of kind Nat, we cannot define a fromNat function of the given type.

Proxy types provide a partial work around Haskell’s limitations for cases where knowing what type is given to a function as its “argument” at compile-time is sufficient.

TLDR. A proxy type is a type of kind k -> * (where k can be specialised to the kind of whatever types you want to give to a function as argument). Only types of kind * have values, so we apply our proxy type constructor to some argument of kind k to get a type of kind * which then makes a suitable parameter for a function.

In the following example, we will show how this allows us to convert a type into a corresponding value. In other words, we show how to take information from the type level and convert it to information at the value level (reification).

data NatProxy (n :: Nat) = MkProxy

Here, the NatProxy type constructor is of kind Nat -> *, meaning it takes some type n of kind Nat and gives back a type of kind * which has a value at run-time. MkProxy is the data constructor for NatProxy and is of type NatProxy n.

Now with our proxy type, we can define a fromNat function with a slightly modified type. Since NatProxy :: Nat -> *, NatProxy n is a valid parameter type for a function since it is of kind *. We use a type class to overload this fromNat function so that we can provide different implementations for it, depending on which type n is. For example, if n is 'Zero we just define fromNat to return 0 as shown:

class FromNat (n :: Nat) where
  fromNat :: NatProxy n -> Int

instance FromNat 'Zero where -- 'Zero is a type defined by Nat in GADT section
  -- fromNat :: NatProxy 'Zero -> Int
  fromNat _ = 0

Next, the instance for any other n requires us to constrain the n in the instance head to be an instance of FromNat so that we can define the instance for 'Succ n recursively. The recursive call to fromNat is given MkProxy as argument, with an explicit type annotation instructing the compiler to choose the fromNat implementation for n. (Read the comments in the code snippet.)

{-# LANGUAGE ScopedTypeVariables #-}
instance FromNat n => FromNat ('Succ n) where
  -- fromNat :: FromNat n => NatProxy ('Succ n) -> Int
  fromNat _ = 1 + fromNat (MkProxy :: NatProxy n)
  -- (MkProxy :: NatProxy n) essentially means the n in "NatProxy n" 
  -- is the same n as that in the instance head. 
  -- ScopedTypeVariables extension has to be enabled for this to work.
  
  vlength :: forall n a . FromNat n => Vector n a -> Int 
  vlength _ = fromNat (MkProxy :: NatProxy n)
  -- Here "forall n a" is required for ScopedTypeVariables to work correctly

Although we use proxy types to implement the reification process here, they are independent techniques. That is, proxy types have uses outside of reification and reification can be accomplished without proxy types, which is not covered in the module.

Additional Example (Type Application)

FYI. This section is additional material and is not tested in the exams. I have included an example that Michael showed me, to illustrate how we may reify types without using proxy types.

Quoting Michael,

“I just typed straight into Slack, so it may not compile as is, but conceptually this [is how we would do it]”

This example makes use of a few language extensions which are shown.

{-# LANGUAGE TypeApplication, AllowAmbiguousTypes, ScopedTypeVariables #-}
class FromNat (n :: Nat) where
   fromNat :: Int
   
instance FromNat Zero where
   fromNat = 0
   
instance FromNat n => FromNat (Succ n) where
   fromNat = 1 + fromNat @n
   
type Test = Succ (Succ Zero)

test :: Int
test = fromNat @Test

Here, @ is type application which is used to explicitly supply an argument for a universal quantifier. Universal quantifiers are usually implicit in Haskell, but in some cases it is useful to make them explicit when writing down typings. In the case of fromNat, its type is as follows with the universal quantifiers made explicit:

fromNat :: forall (n :: Nat) . FromNat n => Int

When we write fromNat @Test (last line), the n gets instantiated with Test and we get FromNat Test => Int as the type. Because Test expands to something that has an instance of FromNat, the constraint is satisfied and the compiler can pick the right implementation of fromNat to use, which is how the reification “works”.

Type application can be used with other variables, for example something. As long as these have an instance of FromNat defined for them. So if we write fromNat @something then n will be instantiated with something.

Concluding Reification

Here, we have provided two examples of how we can reify types. You have seen how useful type classes are as they allow us overload the fromNat function for different types of n. This resolves to the correct instances at compile-time so the right implementation of the function is evaluated at runtime.

Type Families

Language extension: TypeFamilies

Type families are type-level functions and allow us to perform computation at the type-level. There are two main types of type families, closed type families and associated (open) type families.

Associated (open) type families are “attached” to type classes and is open to further extension when defining instances.

Closed type families are very much like “normal” functions in the sense that you “know” what kind of types the type family will deal with and the effect to be achieved, and you just define it as such.

Closed Type Families

I think the best way to explain this is through an example. As you can see, the syntax for type families is different from anything we’ve seen before. The example below should be pretty self explanatory and you can see that the head of definition sort of resembles the type signature of a normal function, and the definition of the actual Add function is just pattern matching on the type of Nat.

{-# LANGUAGE TypeFamilies #-}
type family Add (n :: Nat) (m :: Nat) :: Nat where
  -- Add :: Nat -> Nat -> Nat
  Add 'Zero m = m
  Add ('Succ n) m = 'Succ (Add n m)

If we enable the TypeOperators language extension, we can use operators in our type family definition, which in turn allow us to use it very nicely in the vappend example below.

{-# LANGUAGE TypeOperators #-}
type family (+) (n :: Nat) (m :: Nat) :: Nat where
-- or
type family (n :: Nat) + (m :: Nat) :: Nat where

vappend :: Vector n a -> Vector m a -> Vector (n + m) a
vappend Nil         ys = ys
vappend (Cons x xs) ys = Cons x (vappend xs ys)

How to test in REPL

We can get REPL to evaluate types for us by using the :kind! syntax. This evaluates the type to its normal form.

Lecture> :kind! (+) 'Zero 'Zero
(+) 'Zero 'Zero :: Nat
= 'Zero

Associated (Open) Type Families

Motivation for Associated Type Families. Sometimes, when we define a certain type class, we want it to be as general as possible but because of certain constraint requirements for different instances of the type class, it is difficult without type families.

Example. Let’s say we want to define a type class Collection for various data structures like lists or trees etc.

class Collection c where
  -- c :: * -> *
  empty  :: c a 
  insert :: a -> c a -> c a
  member :: a -> c a -> Bool -- Checks if `a` is part of a collection

Now when we try to define an instance of Collection for lists, we could try to implement it this way. However, we get a type error due to our usage of elem, which requires elements in the list to have the Eq constraint.

instance Collection [] where
  empty       = []
  insert x xs = x : xs
  member x xs = x `elem` xs 
  -- however we get a type error:
  -- No instance for Eq a arising from use of elem

We could add an Eq a constraint onto the type class definition for member. However, this makes the Collection type class too restrictive for other data structures. Furthermore, we can’t predict what kind of data structures that other people will create, and Collection should be as general as possible.

Associated type families to the rescue

Associated type families allow us to associate a type family with our type class. This allows to do “something” based on the instance of the type class which depends on the problem we are trying to solve.

Regarding the example above, our goal is to have some way of placing constraints on the type of the elements contained inside c, so that our instances for the type class type checks.

So for any instance of collection, the Elem type family, given c, will return the type of elements in c. This establishes a relation between c and some type of kind *.

class Collection c where
  type family Elem c :: *
  
  empty  :: c
  insert :: Elem c -> c -> c
  member :: Elem c -> c -> Bool

If we write down the specialised type signatures for insert and member for this instance of Collection for lists, we can see that the associated type family Elem tells the compiler that the a contained inside the list, is the same a that is used in the rest of the instance definition. We can now place an Eq constraint on a and everything type checks.

instance Eq a => Collection [a] where 
  type Elem [a] = a -- this isn't a type alias; it's a type family instance.
  
  empty       = []
  -- insert :: Elem [a] -> [a] -> [a] (Specialised type signature)
  insert x xs = x : xs
  -- member :: Elem [a] -> [a] -> Bool
  member x xs = x `elem` xs

Overloaded Lists

Language Extension: OverloadedLists

This is a neat language extension that allows us to use list notation for other data types as long as the data type has an instance of IsList defined for it.

-- Without
poultree :: Tree String
poultree = Node Black
             (Node Black Leaf "Chicken" Leaf)
             "Duck"
             (Node Black Leaf "Goose" Leaf)
-- With
{-# LANGUAGE OverloadedLists #-}
poultree :: Tree String
poultree = ["Duck", "Goose", "Chicken"]

Below we show an example with the Tree data structure from one of the labs.

-- IsList is defined in GHC.Exts
class IsList l where
  type family Item l :: *
  
  fromList  :: [Item l] -> l
  fromListN :: Int -> [Item l] -> l
  fromListN _ xs = fromList xs
  toList    :: l -> [Item l]
  
instance Ord a => IsList (L.Tree a) where
  type Item (L.Tree a) = a
  
  toList = L.toList
  fromList = foldr (flip L.insert) L.empty

Table of Contents

General Functional Programming

Imperative vs Functional

The Compiler

Expressions and definitions

Anonymous functions

Syntactic sugar for functions

Currying

Uncurry

Conditionals

Lists

Ranges

List comprehensions

Type Classes

Type Class Definitions

Type Instance

Constraints on instances

Superclass Constraints

Polymorphism

Parametric polymorphism

Ad-hoc polymorphism

Subtype polymorphism

Associativity

Lazy Evaluation & Recursion

Evaluation Strategies

Strictness

Call-by-value

Call-by-name

CBN vs CBV

Lazy evaluation

Sharing

Lazy evaluation Walk-through

Closures

Dynamic Closures

Recursive Functions

Optimised Recursive Functions in Haskell

Useful recursive functions

Quick sort

Higher order functions

Sections

Examples of higher order functions

Map

Filter

Quicksort using filter

Folds

Foldr

Foldl

Foldl’

Function composition

Data Types

Data Type Definition

Parametrised Data Constructors

Recursive Data Types

Type Aliases

Derivable Type Classes

Equational Reasoning in Haskell

Intro

Techniques

Direct proof

Function application and unapplication

Non-overlapping pattern matching

Case analysis

Applying an assumption

Eta-conversion

Induction

Examples

Direct proof

Reversing a singleton list

Proof by induction

Addition on recursively defined numbers

Adding zero results in no change

Associativity of natural numbers

Induction on lists

Proving map fusion

Functors, Applicatives, Monads

Functor Factory

Functor Laws

Applicative Academy

Applicative Laws

Left and Right Apply