porges

Derivatives of Containers claims to look for the ‘container which is its own derivative’; in other words, a type analogue of e^x. They arrive at (approximated in ASCII and the notation used in my previous post):

T[X] = Forall(n : N) Xn / Autn

This is a little much for me, since I don’t understand the symbolism and terminology used in the other 99% of the paper, either! However, as they note that it closely matches the Taylor-series expansion of e^x. I think that using the simple concepts I linked to in the previous post, I can approach a similar definition.

First of all, start with a simple (identity?) type:

F[X] = X

Now, since what we want is a type that when differentiated, gives itself, we should start by integrating:

F[X]  = X2 ÷ 2

As shown in the previous post, we can interpret the division operator as ‘missing information’. In this case, the missing information is a 2-enum stating where the new type element was to be inserted… thus we have a type consisting of two elements, only we don’t know in what order they should appear. If we repeat this process several times, we obtain:

F[X] = X3 ÷ (2×3)
F[X] = X4 ÷ (2×3×4)
F[X] = X5 ÷ (2×3×4×5)

Now we can begin to see a pattern emerging. Each time we integrate the function, we are adding an element to the type, without saying where it should be inserted—in other words, we are creating an unordered set of objects (note that these aren’t true sets, but merely bags: sets which can contain duplicates). Now if we take the literal Taylor expansion of e^x, we can see what it really is as a type:

E[X] = Σ (Xn ÷ n!)

It is either a bag with one element, or a bag with two elements, or a bag with three elements… it is in fact the union of all bag types! That is, the exponential function interpreted as a type, is the type of bags.