A pair colleagues of mine and I have been staring at an interesting riddle, which I’m guessing exists in the literature somewhere. He pointed out that we have sum types where a+b is the type containing all the values in a, and all the values in b, we have product types where a*b is the type containing all the values which contain an a, and a b. What we don’t have though is exponentiation types. The riddle then – what is the type ab?
Bart realised that this type is b -> a. The type contains all functions that map bs onto as. This has some rather nice mathematical properties. We know from our early maths a couple of rules about exponents:
ab * ac = ab+c
This gives us a rather nice isomorphism: (b -> a, c -> a) is equivalent to (b + c) -> a. That is, if we have one function that produces an a from bs, another that gives us an a from cs, we can write a function that gives us as, given either a b or a c, and vice versa.
Secondly, and perhaps even nicer
(ab)c = ab*c
This gives us a different isomorphism: c -> b -> a is equivalent to (b,c) -> a. Woohoo, we have currying!
This seems very close to the curry-howard isomorphism, but not quite there. Does anyone know who’s discovered this already?
No Ordering 
Functions are a well known example of exponentials in category theory. You can view the types categorically and this derivation drops right out.
An example of a paper using that terminology:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.7380
But the notion goes back a lot farther than that.
See:
http://en.wikipedia.org/wiki/Exponential_object
Thanks a lot, some very useful references, I think it’s time I bought a book on category theory too 🙂
This is really beautiful, but how do you get to the conclusion that a^b is actually the b -> a type?
Intuitively, I would think of a^b as the type of a b-sized tuple containing only values of type a.
We came up with a few different suggestions along the way. The problem with b-sized tuples is that they don’t actually include any values from b, the type has the right number of elements, but doesn’t have the values you’d expect to see.
b -> a on the other hand involves the right number of elements — you can map each of the bs to any a, and *also* involves all the expected combinations of b and a.
I don’t follow. A b-sized tuple of values of type a works for me just fine. Taking Bool = 2, Bool -> Int is isomorphic to (Int,Int).
Nat -> Bool is an infinite tuple of Bools. A typical value might be (True, True, False, False, …)
Integer -> Bool is an infinite tuple of Bools, indexed by integers of course. A typical value of such might be (…, False, True, False, True, … ), with an arrow pointing to one of those marking it as zero.
(Integer -> Bool) -> Bool is where it gets scary… it’s an uncountable infinite tuple, indexed by infinite tuples, which gets kinda hard to think about as a tuple anymore.
But I digress.
Anyway, I don’t know what you mean by combinations of b and a.
I guess I find it strange that if we have:
data A = A1 | A2
data B = B1 | B2 | B3
then A^B would not contain any reference to B’s constructors ever, that doesn’t sound much like exponentiation to me, especially when multiplication does give rise to values with B’s constructors in. The function type on the other hand creates values which cover both sets totally.
Oh, I see, this is actually a choice, more or less. I was being confused by the “Bart realised that this type is b -> a”, as if there was a mathematical reasoning that would lead to this interpretation.
Thanks for the explanations!
There’s a reasonable mathematical intuition into the identification.
Basically you look at n-tuples (for n an integer) and realize that there’s a trivial isomorphism between n-tuples of type a and functions f:{1,…,n}->a, in that: any f:{1,…,n}->a defines an n-tuple (f(1),…,f(n)), and any n-tuple (a1,…,an) defines an f by f(i) = a_i; this establishes that n-tuples of type a and functions from {1,…n}->a are isomorphic.
So then the identification of a^b with functions b->a is much more intuitive.
If you need a little more intuition look at it this way: there’s an obvious “pun” whereby positive integers n are isomorphic to sets of n elements; eg, n -> {1,…,n} and {1,…,n}->n.
So an n-tuple is an object with members that are uniquely identified by the members of the set {1,…,n} (this is just restating the trivial isomorphism with certain functions); likewise a b-tuple is an object with members that are uniquely identified by the members of the type b.
The right intuition for why exponentials are “morally speaking” best thought of as function spaces goes like this:
By analogy, an element of a^b is a b-tuple of a-elements. What does it mean for something to be a b-tuple (for b an arbitrary type)?
Let’s look at n-tuples. A 2-tuple is a pair — element #1 and element #2 — and a 3-tuple is a triple (elements 1 2 and 3, etc.).
For integers this leaves you thinking the rule ought to be: an n tuple is a tuple with n elements, but that is slightly unhelpful with generalizing.
Rather: an n-tuple is a tuple whose elements can be indexed by the set {1,…,n}; in a 2-tuple there’s a 1-element and a 2-element, in a 3-tuple there’s a 1-element and a 2-element and a 3-element, etc.
Or just the simple identity: an n tuple (a1,…,an) f:{1,…,N} -> a where f(i) = a_i.
From this we can more easily generalize to b-tuples for arbitrary types: a b-tuple (A,…) is isomorphic to f:b->a where f(B) = A_b.
Making this “pun” (conflating the #s N with N-element sets) is a whole area in its own right (look it up under the term categorization, Baez has written some approachable summaries).
Isn’t that it? A function b->a is defined with |b| values of type a, so it is a b-sized tuple containing only values of type a.
Indeed, but the values are tied to a specific b, I think Eric hit the nail on the head with “B-indexed”.
A tuple of elements of A indexed by B is /defined/ to be a function from B to A. So when you say that you “think of A^B as the type of all B-indexed tuples containing only values of type A”, you are saying that you think of A^B as the type of functions from B to A.
(I’ve taken the liberty of replacing “B-sized” with “B-indexed”.)
Cheers, B-indexed makes the connection much clearer.
As Edward Kmett pointed out, this is fairly well known in the math community. I saw this isomorphism in Combinatorics class: if A and B are finite, then |A^B| == |A|^|B|.
> as if there was a mathematical reasoning that would lead to this interpretation
But there is one if you agree that there is a mathematical reasoning that leads to associate the type of
List a = Empty | Cons a (List a)
with 1 + a x ( 1 + a x ( 1 + a x … ) ) = 1 + a + a² + a^3 + … which means that a list is either a list of no element or a list with one element or a list …
Here, a fonction b -> a is a list (think of a collection of (b,a)) whose number of elements is given by type b since there is only one a for each b. So, we can only associate a^b. I don’t think it’s a choice.
Furthermore,
List(a) = 1 + a + a² + a^3 + … = 1 / (1 – a)
so
(1 – a) * List(a) = 1
List(a) – a*List(a) = 1
List(a) = 1 + a*List(a)
which is the recursive definition of lists.
Ohhh, that’s rather nice, cheers for that 🙂
These insights underlie tries. See http://conal.net/blog/tag/trie/ for descriptions & references.
Cheers for that, I’ll check into it :).
Also:
(a*b)^c = a^c * b^c (a function c -> a*b is the same as two functions c -> a and c -> b)
1^a = 1
a^0 = 1
a^1 = 1
A good article on types: http://homepage.mac.com/sigfpe/Computing/diff.html
Oh yay, can’t believe we missed those though >.<
All of Tarski’s High School Algebra axioms can be interpreted as types. Each identity there corresponds to an isomorphism between types. It’s a nice exercise to implement this isomorphism for each case.
Win, cheers for the link 🙂
“This seems very close to the curry-howard isomorphism, but not quite there. Does anyone know who’s discovered this already?”
This is exactly how exponentiation is defined in cardinal arithmetic: http://en.wikipedia.org/wiki/Cardinal_arithmetic#Cardinal_exponentiation
Essentially they made the same observation as you did: With sets A and B of size |A| and |B| then |functions B -> A| = |A|^|B|.
Cheers muchly 🙂
Yep you’ve nailed it.
And you’ve also figured out that this is the Curry-Howard Isomorhpism at work. Why do you say “but not quite there” ?
To the commenter who was wondering whether A^B should instead be a tuple of A’s of length B. This is isomorphic to the concept of a function from B to A (at least, provided you label the positions in the tuple with the elements of B; so in effect, a bit more like a Map data structure which lists a value of A for each value of B).
It’s just a difference between an intentional and an extensional view. The Intentional view of it is as a Function which describes how to calculate one thing from another, The Extensional view is more as a data structure which lists the output for each possible input.
But from a Category Theory point of view, the difference doesn’t matter, they’re both exponentials.
The reason I say not-quite there is that it’s about operations that work on numeric values, and their relation to types, wheras I was under the impression that curry-howard gave a relationship between boolean algebra and types? (Not that those two aren’t related also)
Yep, well the question of “what is the analog in terms of types, for integer operations?” is closely related to curry-howard.
Essentially there are these constructions called sum, product, exponential, which work in a very abstract setting, that of Cartesian Closed Categories. So I reckon category theory in general, and these in particular, are a good starting point if you’re interested in the connections.
http://en.wikipedia.org/wiki/Cartesian_closed_category
What they mean in practise depends what category you’re working in, and we’ve touched on 3 or 4 important examples here:
* The category of types of a programming language, with functions between those types as morphisms
* The category of propositions, with proofs as morphisms
* The category of finite sets, with functions between those sets as morhpisms
* The category of natural numbers (if you think of this as the category of set cardinalities, it’s what you get by taking the category of finite sets, and taking it modulo isomorphism ie modulo set bijections)
The Curry-Howard isomorphism can be seen as an isomorphism of categories, between the first two of these. (in practise you need to name a particular type system and a particular logic)
I’ve left out some details here, perhaps some due to my flaky memory, but hopefully enough to give you a taste!
In fact mathematicians will often use the words ‘Function’ and ‘Map’ interchangeably. Whereas computer scientists will tend to use the different terms to differentiate between Function-as-code and Map-as-data.
For most purposes mathematicians won’t care whether a function is defined extensionally (as data) or intentionally (as code). It might matter if you’re storing or evaluating the things on a computer, but not if you’re just proving stuff about them in the abstract.
You can also look up info on Heyting algebras. These can be used as an interpretation of types. See the following, from Bob Harper’s course on constructive logic:
Click to access alg.pdf
Excellent, thanks, so many references from this post :).
To make a^b * a^c = a^(b+c) and some other identities work, you may want b+c to be the symmetric difference of the two sets, i.e. the union minus the intersection.
I’m not sure I get you – that isomorphism already does work. But I guess I’m assuming that no two types ever have the same value in them, so effectively our statements are equal. Do you have a reference to a type system that doesn’t have this property?
[…] Exponentiation Types A pair colleagues of mine and I have been staring at an interesting riddle, which I’m guessing exists in the […] […]