Latest revision as of 11:47, 11 July 2023

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)

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 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.
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:
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.
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.

Related

• Data compression
• Efficient storage of edit histories (data diffing)

• Annotated lambda diagram
• Annotated lambda diagram mockups

• Typed holes

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

Differentiating datastructures:

• https://stackoverflow.com/questions/5919901/data-structure-differentiation-intuition-building

Zippers:

• https://wiki.haskell.org/Zipper
• https://en.wikibooks.org/wiki/Haskell/Zippers
• https://okmij.org/ftp/continuations/zipper.html
• Functional Pearl paper: https://www.st.cs.uni-saarland.de/edu/seminare/2005/advanced-fp/docs/huet-zipper.pdf
• Functional Pearl code: https://github.com/srijs/haskell-lambda-term-zipper

Generating functions:
These can relate to recursively defined datastructures (and their derivatives) like lists & trees.

• wikipedia: https://en.wikipedia.org/wiki/Generating_function
• generatingfunctionology: https://www2.math.upenn.edu/~wilf/DownldGF.html

Generating functions in physics:
Symmetry <=> conserved quantity – (Noether theorem)

• https://en.wikipedia.org/wiki/Translation_operator_(quantum_mechanics)
• https://en.wikipedia.org/wiki/Time_translation_symmetry
• https://en.wikipedia.org/wiki/Time_evolution

(wiki-TODO: Explain hunches on how this links together. Maybe move on other page.)