Revision as of 14:13, 21 October 2021

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-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)

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.

External Links

• Wikipedia: Curry–Howard correspondence