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
Contents
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-function 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.
Collapsing down an 3-argument-function into a 1-argument-function taking an 3-tuple
- : a -> a -> a -> b ~ ((b^a)^a)^a) = b^a^a^a … by convention
- (a,a,a) -> b ~ b^(3*a)
What about inverse functions:
subtracion, division, logarithms??
They are sure to be a portal to some odd realm ...
Why function types correspond to ResultType^ArgumentType (and are called exponentials)
A function with an argument of type Bool can only receive two different values and thus yields a pair of result values.
To gain all possible situations all possible combinations of result values need to be taken.
- Bool → Int ~ (Int,Int) ~ #Int * #Int ~ #Int ^ 2 ~ #Int ^ #Bool
Consequences and applications
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.
When storing changes incrementally this might remove the necessity to decide whether to store them as raw-diffs or edit-actions.
Instead from the chosen data representation naturally there falls out an elegant representation of changes and
user edits can then perhaps be represented in terms of that. That would be superb, wouldn't it?
There is probably room for messy ad-hoc (invented rather than discovered)
practical optimizations atop a formalized (discovered rather than invented) derived core diffing calculus
like e.g. adding "key-frames" at important snapshot states for faster restore and more resilience against data damage like holes in the sequence of update edits.
This space seems pretty much unexplored, so how this could look like in the details is largely unclear.
External Links
- Wikipedia: Curry–Howard correspondence
Videos:
- https://youtu.be/REqRzMI26Nw?t=1999 — 33:19 — Category Theory 8.1: Function objects, exponentials – by Bartosz Milewski
- https://youtu.be/iXZR1v3YN-8 — Category Theory 8.2: Type algebra, Curry-Howard-Lambek isomorphism – by Bartosz Milewski
