Following a remark of Lawvere, we explicitly exhibit a particularly elementary bijection between the set T of finite binary trees and the set T^7 of seven-tuples of such trees. "Particularly elementary" means that the application of the bijection to a seven-tuple of trees involves case distinctions only down to a fixed depth (namely four) in the given seven-tuple. We clarify how this and similar bijections are related to the free commutative semiring on one generator X subject to X=1+X^2. Finally, our main theorem is that the existence of particularly elementary bijections can be deduced from the provable existence, in intuitionistic type theory, of any bijections at all.
Metadata: arXiv. Abstracts retain their original authors’ rights.
In the conversation
Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels
The connection between type isomorphisms and algebraic equalities is known and explored in a variety of interesting ways.
I don't know the precise history of the development of the notation and vocabulary, but there's a reason types like A+B are notated with a plus symbol and called "sums". Similarly for products. And it may surprise you (or not) to learn that people sometimes call A -> B an exponential type, and even notate it with superscript notation.
One of my favorites is the result that the binary tree type is isomorphic to septuples of binary trees, which you can arrive at by using the definition of binary trees as the fixed point solution of T = 1 + T*T and deriving T = T^7 with some algebra. [0]
[0] https://arxiv.org/abs/math/9405205
Some related links (specifically that they perform "high school" algebra on types):
- Seven trees in one [0], a paper showing a bijection between binary trees and seven-tuples of binary trees.
- The algebra of algebraic data types [1] discusses Taylor expansions of data types.
- Differentiation of higher-order types [2] is commenting on OP's paper.
I used to be really interested in type theory, but haven't had as much time to explore it, but over the years I've saved these links (and the one posted).
[0]: https://arxiv.org/pdf/math/9405205.pdf
[1]: https://codewords.recurse.com/issues/three/algebra-and-calcu...
[2]: http://conal.net/blog/posts/differentiation-of-higher-order-...
A very nice fact that I coincidentally learned just yesterday, which is not in the linked answer but is touched on in one of the comments and in an edit on the accepted answer: there is an explicit bijection that maps a binary tree to seven binary trees (and vice-versa, by the inverse function).
Consider the definition of a binary tree: "a binary tree is either empty, or is a root with a left tree and a right tree". This we can write as
T = 1 + T²
Solving the analogous equation z = 1 + z² in the complex numbers gives z to be a primitive sixth-root of unity (https://www.wolframalpha.com/input?i2d=true&i=z+%3D+1+%2B+Po...), i.e. z⁶ = 1, and so z⁷ = z. It turns out that…
Read the full comment
we can similarly show T⁷ = T with some algebra (without subtractions) by repeatedly applying the transformations T→1+T² or 1+T²→T (a "game" version is at http://lebarde.alwaysdata.net/seventrees/):
T⁷
= T⁶ + T⁸
= T⁵ + T⁷ + T⁸
= T⁴ + T⁶ + T⁷ + T⁸
= T⁴ + 2T⁷
= T³ + T⁵ + 2T⁷
= T³ + T⁶ + T⁷
= T² + T⁴ + T⁶ + T⁷
= T² + T⁵ + T⁷
= T² + T⁶
= T + T³ + T⁶
= T + T² + T⁴ + T⁶
= T + T² + T⁵
= 2T + T³ + T⁵
= 2T + T⁴
= 1 + T + T² + T⁴
= 1 + T + T³
= 1 + T²
= T
This can be used to give an explicit bijection: see Andreas Blass's paper "Seven trees in one": https://arxiv.org/pdf/math/9405205 (via https://twitter.com/CihanPostsThms/status/157901771352705024... — see also https://math.ucr.edu/home/baez/week202.html which has more.)
A few remarks on this stuff.
1. Very closely related is the pure-mathematical technique of generating functions, where you take a sequence (let's say the Fibonacci sequence 0,1,1,2,3,5,8,13,...) and use its elements as coefficients in a power series (0+1x+1x^2+2x^3+3x^4+5x^5+8x^6+13x^7+...) and then notice that (e.g.) shifting the sequence by 1 is the same as multiplying by x, so if F is the series for (f(n)) then x.F is the series for (f(n-1)) and x^2.F is the series for (f(n-2)) apart from some corrections for very small n, which gets you F=(x+x^2)F+x or F = x/(1-x-x^2), and now you can factorize that quadratic and write F in the form p/(1-ax)+q/(1-bx) which immediately…
Read the full comment
gets you an explicit formula for the Fibonacci numbers (the one with all the sqrt(5)s in it).
So let's translate this into algebraic data types. We get
F(x) = x + x F(x) + x^2 F(x)
data FibTree a = Leaf a | Pair a (FibTree a) | Triple a a (FibTree a)
and the number of FibTrees with n "a"s in is exactly the nth Fibonacci number.
(There is a theoretically important data structure called a Fibonacci heap, but I don't believe there is any connection between these and these "Fibonacci trees" other than that in both cases there is something you can count with Fibonacci numbers.)
2. Suppose you consider a rather boring binary-tree type like this:
data Tree = Leaf | Pair Tree Tree
whose corresponding identity is T = 1+T^2, or T^2-T+1=0. If you're a mathematician you will quickly see that the solutions (in the complex numbers!) of this are sixth roots of unity; that is, they have T^6=1. This clearly can't hold in terms of types (it would mean an equivalence between 6-tuples of trees and objects of the "unit type", there being only one such object), but it turns out that T^7=T is "true"; you can find an explicit construction for it on page 3 of http://arxiv.org/abs/math/9405205 if you like.
3. It doesn't appear that the author of the OP ever got round to writing about negative and fractional types, but other people have. For instance, this paper http://www.cs.indiana.edu/~sabry/papers/rational.pdf which I have only glanced at (it appears to do this in a more restrictive context where there aren't general ADTs with recursive definitions; negative types seem to involve running computations backwards somehow, and reciprocals are "constraints").
Apologies if I've got my Haskell syntax wrong anywhere.
In response to Jaffe and Quinn [math.HO/9307227], the author discusses forms of progress in mathematics that are not captured by formal proofs of theorems, especially in his own work in the theory of foliations and geometrization of 3-manifolds and dynamical systems.
Artificial intelligence (AI) researchers have been developing and refining large language models (LLMs) that exhibit remarkable capabilities across a variety of domains and tasks, challenging our understanding of learning and cognition.