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?