porges

After reading Differention of Datastructures, I think I finally understand what is meant by “types as functions”, and immediately I can see one direction in which to go from what is presented there.

If we take integration to be the logical inverse of differentiation (which is defined in the article as ‘removal of an element from a type’, then we have integration as the addition of an element to a type.

For example, take the type of an array of 3 elements of the same type:

F[T] = T3

If we are to add an element to this array, we want to integrate it. This gives us:

F[T] = T4 ÷ 4

Clearly this is not what we expected. If we want to add an element to a 3-element array, we are expecting a 4-element array. However, if we look again at the above result, we can reinterpret it as telling us something: the mere integration of the type is not supplying the expected result; and if we interpret division as ‘without’ (just as addition is ‘or’ and multiplication is ‘and’, then we can understand the result obtained.

What this is in fact telling us is that we need to provide another parameter (an enum in this case), which will give us the required result. In other words (if we do it backwards…:

F[T] = T4 -- wanted
F'[T] = 4.T3 -- needed

In order to obtain a 4-element array, we need a 3-element array and a 4-enum. This makes sense, because if we have a 3-element array:

x y z

…and we wish to add an element ‘w’ to it, we need to know where to insert it. The number of insertion points is:

(1) x (2) y (3) z (4)

…and thus we need to supply a 4-enum to specify exactly where we want the insertion to take place. Once we have done this, we obtain our 4-element array with no ‘missing’ parameters.