View source for 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-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 … <small>''() → a … this morphism is called "global element"''</small> 
----
* (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: <br>
subtracion, division, logarithms?? <br>
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. <br>
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 <br>
one can do analytic differentiation on [[algebraic datatype]] (ADT). <br>
That further implies that Taylorseries (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. <br>
Filling these holes gives back an instance of the original ADTs structure. <br>
This corresponds to multiplying a derivative with a delta in normal mathematical calculus. <br>

There is a '''potential practical application''' of massive value here: <br>
Highly scaleable version management and efficient [[data-compression]] 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. <br>
Instead from the chosen data representation naturally there falls out an elegant representation of changes and <br>
user edits can then perhaps be represented in terms of that. That would be superb, wouldn't it? <br>

There is probably room for messy ad-hoc ([[invented rather than discovered]]) <br>
practical optimizations atop a formalized ([[discovered rather than invented]]) derived core diffing calculus <br>
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. <br>
This space seems pretty much unexplored, so how this could look like in the details is largely unclear.

= Related =

* [[Data compression]]  
* [[Efficient storage of edit histories]] (data diffing)
----
* [[Annotated lambda diagram]]
* [[Annotated lambda diagram mockups]]

= External Links =

* Wikipedia: [https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence 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