When I wrote a type as an exponential, a labmate in a different discipline immediately asked what a logarithm would be, so I have been thinking along these same lines recently, playing with the recursive equations for Stream, List, Nat, and whatnot. Is this perhaps useful for flattening a type for parallel computation? What about non-Naperian types that are related to Naperian types? Take lists as finite prefixes of infinite streams; the “McBridean formula” gives the same result for both, even though the latter is non-Naperian.

I’m hoping that you do find something non-trivial, as I want to read about it from someone who knows what they are talking about

Then the operator D defined by D F X = \|/ F X 1 is Fox’s free derivative.

Just responding to your comment here: http://sigfpe.blogspot.com/2006/06/taylor-series-for-types.html I had actually already found and read this dissection document. Interesting. It’s nice to see a rigorous derivation of something like a Taylor expansion for types.

If you don’t mind recklessly throwing all caution to the wind here’s another way to ‘derive’ the Taylor series, different to my previous ‘derivation’:

If F[X] is an F-container of X’s
dF[X] is an F-container with a hole
d^2F[X} is an F-container with an ordered pair of holes
(1+d^2/2)F[X} is an F-container with no holes or an unordered pair of holes, etc.
G[d]F[X] is an F-container with a G-container of holes in it(!!)
A.dF[X] is an F-container with an A-labelled hole
G[A.d]F[X] is an F-container with a G-container of A-labelled holes in it
exp(A.d)F[X] is an F-container with a set of A-labelled holes in it
But that’s just an F[X+A].
Expanding the left hand side gives the Taylor series.

But yes, I’m fully aware this is a long way from rigour. But it’s fun to play with, and a container of holes sounds like a useful thing to me. I think it’d be nice to make it rigorous somehow.

The original motivation for this idea was that I wanted a way to incrementally instantiate without having to parse through the whole of the term. We thought that providing “signposts” in the term would allow avoiding large sections of the term in which the variable did not occur.

Anyway, for the binary tree case I think it should be ….

Term V = μ T. V + 1 + T²

Zipper V = [2×(Term V)]

Skeleton V =
μ S. Zipper ∅ ×
(V + S × S + S × Term V + Term V × S × Term V x Term V)

or more briefly:

Skeleton V = μ S. Zipper ∅ × (V + (S + Term V)² )

(by “(a + b)² = a² + 2ab + b²”)

“Deriving rules for inductive sets in Martin-Löf’s type theory” also from 1989.

The approach (only sketched) is to pick out “good” trees in a W-type. Unfortunately it isn’t possible to tell how this predicate is defined. Conceivably though he used the method given above (but to me it seems more likely he used a `large elimination’).

In any case, the next time someone is in Chalmers, could they please ask for a copy of this report? Or if they bump into Dan somewhere?