Nice to know! I thought about it in terms of cardinalities of types. If A and B are types with |A| and |B| values correspondingly, there are |B|^|A| possible f

Nice to know! I thought about it in terms of cardinalities of types. If A and B are types with |A| and |B| values correspondingly, there are |B|^|A| possible functions A -> B. Another funny thing is that if you consider forall a. (a -> a) -> (a -> a) the type of natural numbers (weird, I know, but basically we encode numbers in unary with number of times we compose (a -> a) to itself), then exponentiation on such numbers will be a ^ b = b a