We saw that every data type is inhabited by a value ⊥ pronounced "bottom". It is very important in a non-strict language such
as Haskell to represent how much knowledge you have about a value. You can either know exactly what the value is, know
only a part of it, or know nothing at all. Bottom represents the latter, but you could as well only know that a list starts
with 1, i.e. _1 : ⊥_.

In fact, all data types in Haskell respect an approximation function _⊑_, where _x ⊑ y_ means "_x_ is an approximation
of _y_". For example with booleans, _x ⊑ y iff ⇔ x ≡ ⊥ or x ≡ y_ in other words either you don't know anything about a
particular boolean, or you know exactly what it is. This approximation ordering is important when reasoning about recursive
algorithms, which is why it is important to understand the notion of "nothingness" in Haskell.

In the next session we'll see talk about cyclic data structures and fixed points, where it plays a big role.

## Exercise for next session

The _fusion law_ of `map` is well known and is commonly used to reduce the runtime complexity of an algorithm:
```hs
map f . map g = map (f . g)
```

Folds and unfolds have similar laws. The `foldr` fusion law states that
```hs
foldr f a . g = foldr h b
```
provided three properties are satisfied.

Can you find out what these properties are? To do that, prove that the equality holds for all lists.

### Example of a derivation

Just wanted to provide an example of how to do it. Given the following definition of `reverse`:
```
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
```
We want to prove the following law holds:
```
reverse (reverse xs) == xs
```

#### Case undefined
```hs
reverse (reverse undefined)
= {- no match in the definition of reverse -}
reverse undefined
= {- again -}
undefined
```

#### Case []
```hs
reverse (reverse [])
= {- definition of reverse -}
reverse []
= {- again -}
[]
```

#### Case (x:xs)
```hs
reverse (reverse (x:xs))
= {- def of reverse -}
reverse (reverse xs ++ [x])
= {- we claim reverse xs ++ [x] = x : reverse xs -}
reverse (x:reverse xs)
= {- definition of reverse -}
reverse (reverse xs) ++ [x]
= {- claim -}
x:reverse (reverse xs)
= {- induction hyposethis -}
x:xs
```

The claim above can be proved similarly.