SDG is all about working with values, d, such that d²=0. When this is true, we find that for suitable functions f,
f(x+d)=f(x)+d f'(x) (Eq. 1)
where f' is the derivative of f.
Now consider derivatives of types. I've written a really sloppy description here but for a proper treatment there are papers like this one. The curious idea is that if you 'differentiate' the type of a container you find the type of the container with a hole in it. Here's a really quick example: let F[X] be the container that is a triples of X's. In other words F[X]=X×X×X=XXX=X3. Here × is the usual product in the category of types. By a container with a 'hole' we mean a container with one of its elements missing, but with a 'hole' left behind so we know where the element has gone missing from. Consider the triple. Either the first element is missing. In this case there are two elements left, so we have something of type X2. On the other hand the middle element could be missing, and the remaining elements also give something of type X2. Or the last element could be missing. Put these three cases together and we get X2+X2+X2=3X2. (The '3' in 3X² indicates that we know which of the three elements has been replaced with a hole.) If we use the prime symbol to mean differentiation we see that a triple with a hole in it is just dX3/dX=F'[X]. This generalises to other types, you can read the papers for more details. I think that's the most amazing bit of computer science I've seen in years. And it's even more fun with recursive types because you then get zippers.
Anyway, those are my ingredients and the following assumes that the above makes some kind of sense to you. So the mad thought I had was this: if you can do calculus by introducing infinitesimals such that d2=0, can we investigate containers with holes by introducing some kind of infinitesimal type with the bizarre property that
D is a type here, not a value. I'm hoping you can just play along here. Clearly we're talking about a weird kind of product when the product of a non-trivial object with itself is the zero object. Presumably to make sense of this we're not really talking about the usual categorical product, just as in the algebra R[d]/(d2) we're not talking about the usual real number multiplication. And note, of course, that I'm not saying that D is the type of infinitesimal numbers - I'm saying that the type itself is in some sense infinitesimal.
So what could D2=0 possibly mean? Well 0 is the type defined by the property that there are no values of type 0. So D2=0 simply means that you can't have a pair of objects of type D. So D isn't so weird at all, it corresponds to a type representing the singleton pattern. (Don't confuse this with the 'singleton' type 1. There is only one object of type 1 but we can have as many of them as we like. On the other hand, there may be many values an object of type D could take, but only one of those possible values can be realised.)
So now consider the type F[X+D]. This is a container, each of whose elements are of type X or of type D. Consider the case that they're all of type X. Then we have something of type F[X]. Now suppose that one of the elements is of type D. Then what we have is an F-container of X's with a hole, with a D in the hole. In other words, D×F'[X]. And now's the fun bit - this is all of the possible cases because the container can only contain one D. After all only one D can exist. Writing this out formally we get:
In other words, we have interpreted Equation 1 in the context of types. As d can be thought of an infinitesimal value it makes sense to call D an infinitesimal type. I'm not sure how far you can run with this idea, but given that the argument above seems to make some kind of sense I expect a smarter person than me could give it rigorous form.
A final thought: D2=0 isn't really all that weird. We're already familiar with linear types and linear logic where we have things that can't be duplicated. This is just a different language to say something similar. Anyway, </mad thought>
Linear logic also bans contraction. This corresponds to not being able to avoid using the hole. Or perhaps that corresponds to weakening. I forget whether I'm going forwards or backwards.
ReplyDeleteIn any case, is it so that d^0 = 0 rather than 1?
d^0 = 0 corresponds to "get rid of the constants". Ideas are now forming in my brain but I don't know if they'll go anywhere.
ReplyDeleteI don't suppose there's anything even resembling singleton types in Haskell…is there?
ReplyDeleteHmm. Reminds me of monads in Haskell.
ReplyDeleteSnorri,
ReplyDeleteI did eventually come up with an interpretation of D^2=0 for types. See here.
The d^2 = 0 is also the case of the exterior derivative for differential forms:
ReplyDeletehttp://en.wikipedia.org/wiki/Differential_form#Exterior_differential_complex
I also see a connection to the boundary operator on chains in algebraic topology:
ReplyDeletehttp://en.wikipedia.org/wiki/Chain_%28algebraic_topology%29
Building on this: Consider a particular space x (which may have positive measure). Then a differential with respect to x should be a finite set of points. The sum x + dx is simply the union of the spaces, which preserves the measure of x. To carry out x/dx, you form an equivalence relation R so that the members of x/R have the same measure and |x/dx| = |dx|, and then identify each of the members with an element of dx.
ReplyDelete