Composable things

There are two types of programming languages; dynamically typed and statically typed. Haskell (and Purescript) is a statically typed language. In simple terms this means that various errors will be caught at compile time as opposed to runtime as with a dynamically typed language. This basically improves the correctness of programs and eliminates a wide class of incorrect programs before they can run.

Haskell can be thought of as a set of types and a set of functions acting on types. (This of course forms the category $Hask$, which is the category of Haskell types and both partial and total functions). A function $f$ taking a type $A$ and returning a type $B$ can be composed with a function $g$ that takes a type $B$ and returns a type $C$ which gives us a single function $h$ that takes an $A$ and returns a $C$. The key is that the output of one function has to be the same as the input to another function in order for them to be composable.

That means that types themselves are also composable and we will return to this when we cover Algebraic Data Types.

Types can be thought of as sets of values. For example the type Bool is a two-element set of True and False (in Haskell). More specifically, it is a three-element set if you include the bottom which is the thing that is used to describe non-terminating computations. Those functions that return bottom are called partial functions as opposed to total functions which return a valid output for every possible input.

One of the big advantages of a language like Haskell is that it is built using denotational semantics, which essentially means that every single construct in the language has it's mathematical counterpart. That simply means that the entire language can be reasoned about and proofs can be done showing that the language behaves exactly as expected without fail.

Let's cover a few examples of types.

The type corresponding to an empty set is called $Void$ in Haskell. As you can imagine it's a type that has no inhabitants. There exists a function from Void to any type a, but this can never be called as there is no way to construct a value of type Void. This function is polymorphic in the return type and it is called absurd as in logic there is a statement that from falsity follows anything:

There is also the type that corresponds to the single element set. In Haskell this is called unit and is represented by the type $()$. A function that takes unit can be thought of as a function that takes nothing and returns a value. A function from unit to a type $a$ simply selects a single element from the set $a$.

What this means is that you can replace an actual value of type $a$ with a function that returns that value itself. These functions from unit are in a one-to-one correspondence with the elements of the set $a$.

Conversely we have functions that return the unit type. These functions are used for side-effects. Haskell is a pure language which means that these functions simply discard their argument. This function maps every single element in its set to the singleton set (or type unit). This function is also parametrically polymorphic:

And of course this logic extends to types that contain an arbitrary number of elements.