Home

Derivatives and dissections of data types

The Derivative of a Regular Type is its Type of One-Hole Contexts by Conor McBride was mentioned on LtU several times.

If you enjoyed it, try a new paper by the same author:
Clowns to the left of me, jokers to the right (Dissecting Data Structures).

More generic programming, more parallels between data types and calculus, more fun.

As usual for Conor's paper, it's short and full of (sometimes obscure) humor. Beware of typos, though.

By Andris Birkmanis at 2007-01-03 21:35 | Functional | Type Theory | other blogs | 19578 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

stuck in the middle of simplicial cats

The key to Stokes' theorem (and hence the Fundamental Theorem of Calculus) appears to me to be that both manifolds and the functions we integrate over them have a simplicial structure, and as the integration respects that structure, we can choose to take our derivative/boundary on either side without affecting the final result. (cf http://lambda-the-ultimate.org/node/1919#comment-23627)

As McBride is dealing in polynomial types, he should have a simplicial object hiding out somewhere and therefore it may not be too surprising that there are many parallels with the calculus.

For those who are far more comfortable with triangle soups than tensors, it might be interesting to take his results for data types and try to interpret them with faces, edges, vertices, etc., thereby substituting the tools of geometry for those of analysis.

By Dave at Thu, 2007-01-04 08:42 | login or register to post comments

I think a good place to look...

...to try to make sense of this stuff mathematically is to consider species, discussed here among other places. These types aren't exactly the same thing as species, but species do also support the notion of the derivative operator making something like a hole in a structure.

I've already thought a little about trying to derive some kind of (co)homology theory from simplices on these things but I haven't got too far yet...

By sigfpe at Thu, 2007-01-04 18:01 | login or register to post comments

heartily agreed

I have posted about species on LtU several times, as has Frank Atanassow.

In fact, I have a PhD student (Gordon Uzskay) working on this topic. More precisely, he's trying to figure out "what happens / what's new / what can you do" when you replace inductive types by species in a functional language. We should have some concrete results (i.e. a paper) by the start of summer.

By Jacques Carette at Thu, 2007-01-04 21:58 | login or register to post comments

Pushing things a bit further...

...it's amazing that the notion of a hole in a semiconductor is related. I'm not stretching the truth too much when I say that. With types, the operator d makes a hole, and the operator X adds a new object to a type eg. X.X^2 is a pair with an extra element, ie. a triple. We have the relation dX=1+Xd (ie. d(X.F[X])=F[X}+X.F'[X]). Similarly in semiconductors we have creation and annihilation operators a' and a with the properties aa'=1+a'a where a makes a hole and a' makes a particle (or maybe a and a' should be swapped). As Baez has pointed out, there is a deep connection between species and quantum field theory.

Anyway, I look forward to seeing some publications on species and types.

By sigfpe at Thu, 2007-01-04 23:16 | login or register to post comments

Weyl and Ore Algebras

Another very very close connection is to Weyl Algebras and thence to Ore algebras. You'll note that the fundamental identity for d above is exactly the fundamental identity defining a Weyl Algebra.

Now, in the Weyl Algebra, this identity is non-commutative, but still linear. That is also what happens with most of the interesting Ore Algebras, but these cover not just differentials, but also shift, delta (ie recurrences), q-shift and q-differential, Mahler operator, etc. Interestingly, Groebner bases can be computed for these, which leads quite directly to providing short proofs for many combinatorial identities (Non-commutative Elimination in Ore Algebras Proves Multivariate Identities).

And of course Baez's work here is fascinating, as is the work of his student Andrew Morton on Stuff Types. Even more interesting (though I do not claim I understand much of it) is Marcelo Fiore's work in this area - a talk and a preprint are available that are cryptic, daunting and tentalizing.

By Jacques Carette at Fri, 2007-01-05 01:03 | login or register to post comments

Finally here

Gordon and I, a year overdue, have finally produced the (submitted preprint) Species: making analytic functors practical for functional programming. All feedback very welcome.

Note that this is essentially a "technology transfer" paper - we are heavily leveraging powerful theory. But there is a long tradition of doing that in programming languages, with Monads being the most prominent example. Of course type theory (as a field) predates programming, and so does the lambda calculus. We're just fishing in combinatorics waters this time 'round.

By Jacques Carette at Wed, 2008-04-23 00:45 | login or register to post comments

Delta -> whatever

After a little persual of Mac Lane it looks as though all of these things are related because given any monoid (and hence any monad), one can get there from Δ.

Aside: If one's nonsense is abstract enough, one should not be surprised that it becomes general enough to map to almost any given problem -- which implies that species, if more specific, should be a better way of treating these issues. Does anyone know of, or would anyone be willing to write, a more accessible (say, on the order of Lawvere and Schnauel) introduction to species? (end of aside)

Weyl algebras take YX − XY − 1 to the identity, which is just a rewriting of the ladder operators: aa†=1+a†a. Both of those are another way of saying that (per Baez) there's one more way to put a ball in a box and then take one out, than to take one out and then put one in. Taking it back to Mac Lane, one finds that the same thing is true of the monotone functions that are the arrows of Δ. Moving that to the concrete setting of triangle meshes, there's one more way to add a point to an edge to form a triangle and then pick an edge (XY * Z → XYZ; XYZ → XY+ZX+YZ (= XY-XZ+YZ)) than to pick a vertex from an edge and then add a point to form a new edge ( XY → X+Y; (X+Y) * Z → XZ+YZ ).

Compare the process of taking the boundary of a triangle by deleting vertices:

    XYZ -> XY. - X.Z + .YZ

to the process of taking a derivative:

 
   XXX -> XX. + X.X + .XX (ie, X^3 -> 3X^2)

to that of forming the different states of a zipper:

    XYZ -> Zip [XY] Z [] | Zip [X] Y [Z] | Zip [] X [YZ]

Note the resemblance here to the dual stacks in Forth or the dual lists of otuto or the stack/input list of a parser, and perhaps it won't then be too much handwaving to say that it seems to work dually, for code as well as data, where:

    S / injective monotone / degeneracy
    K / surjective monotone / face operator
    (leaving I for the isos)

or, in a monad, with:

    return / a -> Ma / 0->1 / degeneracy
    join / MMa -> Ma / 2->1 / face operator

By Dave at Fri, 2007-01-05 16:24 | login or register to post comments

Derivative Of List Type

I think it's reasonable to say that List X is a sum type, 1 + X + X2 + X3 + .... This is alluded to in McBride's paper. However, I can't figure out how to show either one of:
  1. it's derivative is (List X)2 for all X (McBride 'puns' on the |x| < 1 case)
  2. List X is not really the sum type 1 + X + X2 + X3 + ...
The proof in McBride's paper is a little opaque, involving the funny µ operator; I was hoping to find something a little more intuitive.
By Jason Dusek at Wed, 2008-01-23 20:37 | login or register to post comments

You can't really get around

You can't really get around µ - without it the type's not recursive.

By Philippa Cowderoy at Wed, 2008-01-23 21:53 | login or register to post comments

Agree with Philippa

You really do need to understand μ. You're way better off thinking of list x as μy.1 + xy rather than the infinite series, in general (and for lots of reasons). Then you can simply follow the rules on page 6, and the only non-obvious cases reduce to a straightforward application of the old-fashioned chain rule (as he notes on pages 6 and 7).

Actually, though, from an intuition perspective, this is no worse than in regular calculus. In the comment beginning "Amusingly" on page 7 of the paper, he notes a connection with a power series in calculus. If the derivative of that power series is intuitive to you, it may be the most intuitive approach to list x as well. If not (and it is certainly not intuitive to me), it perhaps highlights the strength of his approach using explicit fixpoints.

The other way to get an intuition about it is to approach it from the one-hole context perspective. It's fairly easy to see why (list x)2 is the correct type for one-hole contexts in list x.

Anyway I would not expect it to be too intuitive. The very interesting thing about this line of work is that the result is surprising.

By Matt Hellige at Thu, 2008-01-24 00:08 | login or register to post comments

Take a list and make a hole in it

Before the hole is a list. After the hole is a list. So a list with a hole gives you a pair of lists. Conversely, given a pair of lists you can join them together with a hole between them. So the derivative of List X really is (List X)^2.

By sigfpe at Thu, 2008-01-24 01:02 | login or register to post comments

1 + X + X^2 + X^3 + ... ==

1 + X + X^2 + X^3 + ... == (1 - X)^-1

The derivative of which is (1 - X)^-2.

Perhaps this sort of infinite series juggling is more familiar to someone versed in combinatorial or physics nonsense? More specifically, one needs to realise that the derivative of a formal power series has nothing to do with analysis, and is purely a statement of combinatorics -- issues like convergence need not apply. Alternatively, one takes the physicist approach and just ignore anything to do with convergence. *wink* (I'm a physicist, so I'm allowed to say that.)

By genneth at Thu, 2008-01-24 09:00 | login or register to post comments

There's no problem with limits...

...as despite appearances, no limits are being formed. For example, List X = 1+X+X^2+X^3+... is shorthand for List X = 1+X+X^2+...+X^(n-1)+X^n.List X.

By sigfpe at Thu, 2008-01-24 15:23 | login or register to post comments

Nonsense with equations

To apply genneth's well known manipulation of power series in this context, you need the equation (1-x)^{-1}=1+x+x^2+..., but the left hand sign of that equation uses operators that I haven't seen McBride use.

Joyal's theory of species does try to get to grips with more complex operations, but IIRC the theory is neither commutative nor associative in the general case: good luck with equational reasoning in that case!

Some people might be interested in a snippet from the history of logic: Boole's original logic is not the theory we know today as Boolean logic, but was a modified algebraic system containing "uninterpretable terms" that he and his contemporaries did not know how to make sense of. Boolean logic is actually due to Schroeder & Pierce, and the original system only received a full interpretation by Hailperin in the 1970s.

By Charles Stewart at Sat, 2008-01-26 07:21 | login or register to post comments

McBride uses mu

If A = mu X.F then we have an isomorphism A = (F|X=A) (more or less by definition of mu). For example, we can define a list of B's by A=mu X.1+BX. So we get A=1+BA=1+B(1+BA)=1+B+B^2A=1+B+B^2+B^3A and so on. Informally you can think of mu X.1+BX as 1/(1-B) and hence as the sum of a Taylor series, but you don't need any kind of limit to talk about this stuff rigorously.

By sigfpe at Wed, 2008-01-30 01:47 | login or register to post comments

Sign Me Up

So, what's a good link that describes this particular nonsense -- the way a derivative of a formal power series is purely a statement of combinatorics.

By Jason Dusek at Fri, 2008-01-25 08:19 | login or register to post comments

Zeilberger

Doron Zeilberger is quite a character, but one who is actually a mathematician -- he's partially known for being controversial and his great disliking of analysis. Unfortunately his website appears at first glance to be that of a real crank.

See http://www.math.rutgers.edu/~zeilberg/Opinion74.html

As an earlier post mentioned, derivatives and integrals are really combinatorial operations over simplical structures. It's just that usually the structures are deeply hidden. Put another way, derivatives are probably just another endofunctor on some suitable category equipped with a "cardinality" functor to the reals (or even complex).

By genneth at Sat, 2008-01-26 08:58 | login or register to post comments

Interesting...

..but this material does not explain the method you employed.

By Jason Dusek at Sun, 2008-01-27 18:24 | login or register to post comments