3 ms·
ackfoobar has already given a good reason why function types are called exponential, but there is an even deeper reason: function types interact algebraically t
by xigoi 1y ago
ackfoobar has already given a good reason why function types are called exponential, but there is an even deeper reason: function types interact algebraically the same way as exponents.
The type A → (B → C) is isomorphic to (A × B) → C (via currying). This is analogous to the rule (cᵇ)ᵃ = cᵇ˙ᵃ.
The type (A + B) → C is isomorphic to (A → C) × (B → C) (a function with a case expression can be replaced with a pair of functions). This is analogous to the rule cᵃ⁺ᵇ = cᵃ·cᵇ.
- ackfoobar 1y agoSince the cardinalities match the algebra, it's no surprise that identities translate, but seeing them still brings a smile to my face. The correspondence can be pushed much further - to differentiation! https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types https://codewords.recurse.com/issues/three/algebra-and-calcu...