Written by Luka Kerr on August 3, 2019

-- f = function name
-- :: = "Of type"
-- Int = Domain
-- Bool = Codomain
-- x = Input
-- (x > 0) = Output
f :: Int -> Bool
f x = (x > 0)


### Currying & Partial Application

The evaluation of a sequence of functions, each with a single argument.

-- Function that takes an a and returns another
-- function taking an a and returning an a
f :: a -> (a -> a)

-- Practical example, usage: logBase 2 2.754
logBase :: Double -> (Double -> Double)


Function application associates to the left in Haskell, so:

$\text{logBase} \ 2 \ 64 \equiv \text{(logBase 2)} \ 64$

### Tuples

A way to take multiple inputs or produce multiple outputs.

toCartesian :: (Double, Double) -> (Double, Double)
toCartesian (r, theta) = (x, y)
where x = r * cos theta
y = r * sin theta


### Higher Order Functions

Functions that take other functions as arguments.

-- Function that takes a function and returns that function applied twice
twice :: (a -> a) -> (a -> a)
twice f a = f (f a)


### Lists

Lists are singly-linked lists in Haskell. The empty list is written as [] and a list node is written as x : xs. The value x is called the head and the rest of the list xs is called the tail.

[True, False, True] :: [Bool]
[3, 2, 5+1] :: [Int]
[sin, cos] :: [Double -> Double]
[(3, 'a'), (4, 'b')] :: [(Int, Char)]


#### Map

A useful function is map, which, given a function, applies it to each element of a list.

map :: (a -> b) -> [a] -> [b]


### Strings

The type String in Haskell is just a list of characters:

type String = [Char]


### Function Composition

We used function composition to combine our functions together. The mathematical $(f \circ g)(x)$ is written (f . g) x in Haskell.

## Data Types

### Type Synonyms

New names for existing types.

type Point = (Float, Float)
type Vector = (Float, Float)
type Color = (Int, Int, Int, Int)


Type synonyms can be prone to errors, since for example Point and Vector are interchangeable.

### Product Types

Compound types can be defined using the data keyword.

data Point = Point Float Float
deriving (Show, Eq)

data Vector = Vector Float Float
deriving (Show, Eq)


In the Point example there are three areas of interest:

• data Point, where Point is the type name
• = Point, where Point is the constructor name
• Float Float, where both types are the constructor argument types

The Haskell type system can differentiate between these types, and a type error will be thrown if Point is used instead of Vector.

### Records

Identical to data types, but gives projection functions and record syntax.

data Color = Color { r :: Int
, g :: Int
, b :: Int
, a :: Int
} deriving (Show, Eq)


To access a field in a record, use the field name as a function. g (Color 255 18 120 0) gives 18.

### Enumeration Types

Enumeration types are known as sum types since they have more than one constructor.

data LineStyle = Solid | Dashed | Dotted


### Algebraic Data Types

Constructors for sum types can take parameters.

data Picture
= Path [Point] Color LineStyle
| Circle Point Float Color LineStyle
| Polygon [Point] Color LineStyle
-- ...and so on


### Recursive & Parametric Types

Data types can also be defined with parameters and recursively.

-- Maybe type
data Maybe a = Just a | Nothing

-- Lists
data List a = Nil | Cons a (List a)

-- Natural numbers
data Nat = Zero | Succ Nat


## Type Classes

Type classes are constraints that work on multiple types. They can be thought of as a set of types for which certain operations are implemented.

Some examples of type classes are Ord, Eq and Show.

### Show

-- Defining a type class
class Show a where
show :: a -> String

-- Defining an instance of Show for the type Bool
instance Show Bool where
show True = "True"
show False = "False"


### Read

class Read a where


### Ord

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


Ord instances should satisfy the properties of a partial order:

• Reflexivity: x <= x
• Transitivity: If x <= y and y <= z then x <= z
• Antisymmetry: If x <= y and y <= x then x == y
• Totality: Either x <= y or y <= z

### Eq

class Eq a where
(==) :: a -> a -> Bool


Eq instances should satisfy the properties of an equivalence relation:

• Reflexivity: x == x
• Transitivity: If x == y and y == z then x == z
• Symmetry: If x == y then y == x

### Semigroup

A semigroup is a pair of a set $S$ and an operation $\bullet : S \to S \to S$ where the operation $\bullet$ is associative.

There exists a type class in Haskell for Semigroup, where the associativity property must be enforced.

class Semigroup a where
(<>) :: a -> a -> a


Some examples of Semigroup instances are $(\mathbb{N}, +)$ and $(\mathbb{B}, \land)$.

### Monoid

A monoid is a semigroup $(S, \bullet)$ equiped with a special identity element $z \in S$ such that $x \bullet z = x$ and $z \bullet y = y$ for all $x, y \in S$.

In Haskell, the identity element is a function named mempty.

class (Semigroup a) => Monoid a where
mempty :: a


Some examples of Monoid instances are $(\mathbb{B}, \land), z = \top$ and $(\mathbb{N}, +), z = 0$.

### Newtypes

A newtype declaration is similar to a data declaration except that there can be only one constructor and it must take exactly one argument.

newtype Score = S Integer

instance Semigroup Score where
S x <> S y = S (x + y)

instance Monoid Score where
mempty = S 0


Newtypes are represented identically to their type argument, but are treated differently in the type checker, allowing for a zero cost abstraction at runtime.

## Property Based Testing

Key idea: generate random input values, and test properties by running them.

### QuickCheck

Haskell’s QuickCheck is the first library ever invented for property-based testing.

### PBT vs Unit Testing

• Properties are more compact and describe more cases than unit tests
• PBT relies on randomly generated test data which may not cover edge cases
• By increasing the number of random inputs, code coverage is improved in PBT

### Test Data Generation

Data which can be generated randomly is represented by the following type class:

class Arbitrary a where
arbitrary :: Gen a
shrink :: a -> [a]


The shrink function is for when test cases fail. If a given input x fails, QuickCheck will try all inputs in shrink x, repeating the process until the smallest possible input is found.

### Coverage

Types of code coverage include:

• Branch/Decision Coverage: are all conditional branches executed?
• Function Coverage: are all functions executed?
• Entry/Exit Coverage: are all function calls executed?
• Path Coverage: are all behaviours executed?
• Statement/Expression Coverage: are all expressions executed?

## Lazy Evaluation

Haskell is lazily evaluated, also called call-by-need. This means that expressions are only evaluated when they are needed to compute a result for the user.

We can force the previous program to evaluate its accumulator by using a bang pattern, or the primitive operation seq:

sumTo :: Integer -> Integer -> Integer
sumTo !a 0 = a
sumTo !a n = sumTo (a + n) (n - 1)


### Infinite Data Structures

Laziness lets us define data structures that extend infinitely.

-- infinite list of 1's
ones = 1 : ones

-- infinite list of natural numbers
naturals = 0 : map (1+) naturals


## Data Invariants

Data invariants are properties that pertain to a particular data type.

Whenever we use operations on that data type, we want to know that our data invariants are maintained.

For a given data type X we define a wellformedness predicate wf :: X -> Bool. For a given value x :: X, wf x returns true iff our data invariants hold for the value x.

### Modules

A Haskell program will usually be made up of many modules, each of which exports one or more data types.

Modules usually provide a set of functions for a data type X:

• Construction: c :: ... -> X
• Querying: q :: X -> ...
• Updating: u :: ... X -> X

## Abstract Data Types

An ADT is a data type where the implementation details of the type and its associated operations are hidden.

-- Only the Dict type and dict related functions are exported
module Dictionary
( Dict
, empty
, insert
, get
) where

type Word = String
type Definition = String

newtype Dict = [(Word, Definition)]

empty  :: Dict
get    :: Word -> Dict -> Maybe Definition
insert :: Word -> Definition -> Dict -> Dict


## Data Refinement

### Refinement Relations

To connect a model with a type we can define a refinement relation, that tells us whether the model and concrete type represent the same structure conceptually.

-- Model is some hashmap from word to definition
-- Concrete type is Dict
rel :: Dict -> Map -> Bool


### Abstraction Functions

An abstraction function takes a concrete type and produces an abstract model.

toAbstract :: Dict -> Map


### Refinement & Specifications

In general, all functional correctness specifications can be expressed as:

1. All data invariants are maintained
2. The implementation is a refinement of an abstract correctness model

## Higher Kinds

Haskell is comprised of two languages:

• The value-level language, consisting of expressions such as if, let, where etc
• The type-level language, consisting of types Int, Bool, (->), Maybe etc

This type-level language itself has a type system, in which types are given their own types called kinds.

The most basic kind is written as *.

• Types such as Int and Bool have kind *
• Types such as Maybe have kind * -> *
• Types such as Either have kind * -> * -> *

Using ghci we can find the kind of a type by writing :k SomeType.

## Functors

Functor is over types of kind * -> *.

class Functor f where
fmap :: (a -> b) -> f a -> f b


### Functor Laws

-- Identity
fmap id == id

-- Composition
fmap f . fmap g == fmap (f . g)


## Applicatives

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


### Applicative Laws

-- Identity
pure id <*> v = v

-- Homomorphism
pure f <*> pure x = pure (f x)

-- Interchange