α

`list`= 1 + α + α

^{2}+ ...

right? So morally

α

`list`= 1 / (1 - α)

by "solving the geometric series". However, unless I did my algebra wrong, it seems that setting f(x) = 1 / (1 - x) has the property that

f(f(f(x))) = x

which, at one in the morning, seems mysterious and significant to me. This function does a three-card monte among the intervals (1, ∞), (-&infin,0), and (0,1).

So is there any interesting connection at all between the types α and α

`list list list`? It seems to me there cannot be a natural (either in the informal or categorical sense) isomorphism, but who knows.

A cute trick that actually works involves solving for an immediate fixed point of the function f. You get

x = 1 / (1 - x)

(1 - x) x = 1

x = 1 + x

^{2}

the characteristic type equation of binary trees,

*et voila*, indeed the type of binary trees is elegantly isomorphic to the type of lists of binary trees. Witness LISP's representation of trees with cons cells! I'm nearly certain I've seen this before, but it's fun to work through it again and find it for myself.

Oh! I just had a realization. The paper revealed that e

^{X}was multisets (aka "bags") over the type X, and I just realized that cosh X and sinh X ought to be multisets over X with, respectively, an even and odd number of elements.