← Back to context

Comment by perihelions

1 year ago

I was just thinking about something adjacent to this the other day. I had this half-baked idea that you could classify all the "types" built out of, say (R, ×, →) by algebraically replacing each copy of R with a finite set of cardinality a and then counting the cardinality of the entire type expression. So you'd formally associate, say, R^3 with the algebraic term a^3, and that holds regardless of how you rearrange R^3 = R^2 × R or R × R^2 or whatever. I liked the idea because it seemed (?) to derive non-obvious set theoretic equivalences, for free: such as

    R -> (R -> R)  ~   (a^a)^a = a^(a^2)
    R^2 -> R       ~   a^(a^2)

    (R -> R)^2     ~   (a^a)^2 = a^(2a)
    R -> R^2       ~   a^(2a)

The first equivalence is between a "curried", partial-application, function form of a function of two arguments, and the "uncurried" form which takes a tuple argument. The second equivalence is between a pair of real functions and a path in the plane R^2—the two functions getting identified with the coordinate paths x(t) and y(t). (Remember the cardinality of distinct functions over finite sets S -> T is |T|^|S|).

And I think you can take this further, I'm not sure how far, for example by associating different formal parameters a,b,c... for different abstract types S,T,U... Is this a trick that's already known, in type theory?

(My motivation was to try to classify the "complexity", "size", of higher-ordered functions over the reals. The inspiration's that you're imagining a numerical approximation on a grid of size a for (a finite subinterval in) each copy of R: then that cardinality relates to the memory size of the numerical algorithm, working inside that space. And you could interpret the asymptotic growth of the formal function, as a complexity measure of the space. If you think of R^n -> R as a "larger" function space than R -> R^n, that observation maps to a^(a^n) being an asymptotically faster-growing function (of 'a') than (a^n)^a = a^(na). And similarly the functionals, (R -> R) -> R, and function operators (like differential operators) (R -> R) -> (R -> R), form a hierarchy of increasing "size").

2 comments

perihelions

Reply
cvoss  1 year ago

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