Why is the derivative of a regular type its type of one-hole contexts?
Let us define a function that counts the elements of a type, |()| = 1, |Void| = 0, |Either x y| = |x|+|y|, |(x,y)|=|x|*|y|, |List A| = 0 + |A| + |A|^2 + |A|^3 + ... (because lists can be [], [a], [a,b], and so on)
In general the 'size' of any type can be written as a power series (like an infinite polynomial), now for the type |k|*|x|^3, if we punch a hole in it, we get |k|*|x|^2 but we could have picked one of 3 different places to put it so we need to say which one, this gives 3*|k|*|x|^2, and this should be done to every term of a power series.
Since the derivative of a type = the derivative of its powerseries* this explains why we can 'differentiate' a type and get a zipper. (At least it sort of makes sense).
(* why is this true?)
Subscribe to:
Post Comments (Atom)
1 comment:
As a tiny public service, the link in the post is broken -- it should probably be:
http://www.cs.nott.ac.uk/~ctm/diff.pdf
(Hey, anyway, if you're still around, feel free to drop me a line sometime... your presence is missed.)
Post a Comment