Remix.run Logo
xigoi 4 days 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 3 days ago | parent [-]

Since 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-calcu...