Jason (jcreed) wrote,

For some reason Conor McBride's paper on type derivatives and one-hole contexts bubbled up to the surface of my consciousness, along with a notion that you can pretend that the differential operator itself is a plain old algebraic thingy that you can multiply and pump into functions and stuff, which I swear I got from John Baez's writings somewhere, but I can't find where right now.

For example, I could think of the notion of an ordered list of linear 'holes' of type α in a datatype T (where T mentions α — perhaps T is the type of binary trees with α at the leaves or something like that). There might be no holes, or one hole, or two holes, or three holes, etc., so the differential operator I want is
1 + Dα + Dα2 + Dα3 + ...
or in other words
(1 / (1 - Dα))
which has the same shape as the algebraic representation of lists as a data structure in the first place.

Of course this guy seems to satisfy mysterious laws like
Dα(1 / (1 - Dα))T + T = (1 / (1 - Dα))T
which makes perfect sense in terms of the algebra of real numbers if you squint and forget that T and Dα are of kind (type -> type) and (type -> type) -> (type -> type) respectively.

I could also do unordered lists of holes by dividing by the number of permutations and get
1 + Dα + Dα2/2! + Dα3/3! + ...
or in other words

I would definitely conjecture that
(exp(Dα))T = [α+1/α]T
(that is to say, a piece of data of type T with some number of holes where the order doesn't matter is equivalent to replacing the argument α to T with the type α + 1) but I have no clue how I would prove it. It also mysteriously works out in terms of power series of real numbers, though:

f + f' + f''/2! + f'''/3! + ... = f(x+1)

by an easy application of the binomial theorem.
Tags: calculus, types

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded