Curry-Howard-Lambeck isomorphism
Also called Curry-Howard-Lambeck correspondence
It gives a bijective mapping between the following three fields:
- category theory (& numeric representations) <==>
- type theory
- Intuitionistic/constructive logic
Basic correspondences
- 0 or "Initial Object" ≙ Void ≙ False
- 1 or "Terminal Object" ≙ () or "Unit Type" ≙ True
- 2 ≙ Bool ≙ ?
- a*b ≙ (Tuple a b) or (a, b) ≙ a ∧ b … conjunction aka logic and
- a+b ≙ (Either a b) ≙ a ∨ b … disjunction aka logic or
- a^2 ≙ (Tuple a a) or (a, a)
- 2*a ≙ (Either a a) … wich one tells the typeconstructor (Left a) or (Right a)
- b^a ≙ (a → b) ≙ (a ⇒ b) … implication
Algebra with types
- a^0 = 1 ≙ Void → a ~ () … the absurd-funcion is isomorphic to the unit type
- 1^a = 1 ≙ a → () ~ () … the unit-function is isomorphic to the unit type
- a^1 = a ≙ () → a ~ a … the set of single single-element-picker-functions is isomorphic to the set of picked elements … () → a … this morphism is called "global element"
- (a*b)^c = a^c * b^c ≙ c → (a, b) ~ (c → a, c → b) … a function to a pair can always be split up into a pair of functions
- a^(b+c) = a^b * a^c ≙ Either b c → a ~ (b → a, c → a) … a function having two options for inputs can always be split up into a pair of functions
- (a^b)^c = a^(b*c) ≙ c → (b → a) ~ (c, b) → a … a unction returning a function can always be converted in a function taking a pair (and vice versa) This is "currying" and "uncurrying" respectively.
The correspondence of types to the analytic form implies that
one can do analytic differentiation on algebraic datatype (ADT).
That further implies that Tayloeseries (or rather the simpler Mclaurin series) of ADTs can be created.
Taking just the first derivative element of the series one gets special datastructures with holes called zippers.
Filling these holes gives back an instance of the original ADTs structure.
This corresponds to multiplying a derivative with a delta in normal mathematical calculus.
There is a potential practical application of massive value here:
Higly scalable version management and efficent datacomression of logged version history.
External Links
- Wikipedia: Curry–Howard correspondence
