Curry-Howard-Lambeck isomorphism - Revision history

Apm: added Category:Programming

2023-07-11T10:47:42Z

← Older revision		Revision as of 12:47, 11 July 2023
Line 110:		Line 110:

	{{wikitodo\|Explain hunches on how this links together. Maybe move on other page.}}		{{wikitodo\|Explain hunches on how this links together. Maybe move on other page.}}

			[[Category:Programming]]

Apm: /* Related / added Typed holes

2022-12-30T02:16:17Z

Related: added * Typed holes

← Older revision		Revision as of 04:16, 30 December 2022
Line 73:		Line 73:
	* [[Annotated lambda diagram]]		* [[Annotated lambda diagram]]
	* [[Annotated lambda diagram mockups]]		* [[Annotated lambda diagram mockups]]
			----
			* [[Typed holes]]

	= External Links =		= External Links =

Apm: /* External Links */ added a lot of links

2022-10-26T20:13:05Z

External Links: added a lot of links

@@ Line 76: / Line 76: @@
 = External Links =
-* Wikipedia: [https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence Curry–Howard correspondence]
+* 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

Apm: added related section & link to yet unwritten page * Efficient storage of edit histories

2022-10-26T15:43:27Z

added related section & link to yet unwritten page * Efficient storage of edit histories

← Older revision		Revision as of 17:43, 26 October 2022
Line 65:		Line 65:
	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>		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.		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 =		= External Links =

Apm: /* Consequences and applications */ added link to page data compression

2022-01-26T09:25:05Z

Consequences and applications: added link to page data compression

← Older revision		Revision as of 11:25, 26 January 2022
Line 53:		Line 53:

	There is a '''potential practical application''' of massive value here: <br>		There is a '''potential practical application''' of massive value here: <br>
	Highly scaleable version management and efficient data-compression of logged version history.		Highly scaleable version management and efficient [[data-compression]] of logged version history.

	----		----

Apm: /* Consequences and applications */ fixed typos & spelling - a lot

2021-10-30T08:35:33Z

Consequences and applications: fixed typos & spelling - a lot

← Older revision		Revision as of 10:35, 30 October 2021
Line 46:		Line 46:
	The correspondence of types to the analytic form implies that <br>		The correspondence of types to the analytic form implies that <br>
	one can do analytic differentiation on [[algebraic datatype]] (ADT). <br>		one can do analytic differentiation on [[algebraic datatype]] (ADT). <br>
	That further implies that ~~Tayloeseries~~ (or rather the simpler Mclaurin series) of ADTs can be created.		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>		Taking just the first derivative element of the series one gets special datastructures with holes called zippers. <br>
Line 53:		Line 53:

	There is a '''potential practical application''' of massive value here: <br>		There is a '''potential practical application''' of massive value here: <br>
	~~Higly scalable~~ version management and ~~efficent datacomression~~ of logged version history.		Highly scaleable version management and efficient data-compression of logged version history.

	----		----

Apm: /* Consequences and applications */ added notes on -- no need for type of diff representation & option to add informal stuff atop

2021-10-30T08:33:44Z

Consequences and applications: added notes on -- no need for type of diff representation & option to add informal stuff atop

@@ Line 54: / Line 54: @@
 There is a '''potential practical application''' of massive value here: <br>
 Higly scalable version management and efficent datacomression of logged version history.
 = External Links =

Apm: /* Why function types correspond to ResultType^ArgumentType (and are called exponentials) */

2021-10-22T14:16:26Z

Why function types correspond to ResultType^ArgumentType (and are called exponentials)

← Older revision		Revision as of 16:16, 22 October 2021
Line 37:		Line 37:
	== Why function types correspond to ResultType^ArgumentType (and are called exponentials) ==		== 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 ~~<br>~~		A function with an argument of type Bool can only receive two different values and thus yields a pair of result values. <br>
	and thus yields a pair of result values. To gain all possible situations all possible combinations of result values need to be taken.		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		* Bool → Int ~ (Int,Int) ~ #Int * #Int ~ #Int ^ 2 ~ #Int ^ #Bool

Apm: /* External Links */ added links to relevant videos

2021-10-21T12:19:47Z

External Links: added links to relevant videos

← Older revision		Revision as of 14:19, 21 October 2021
Line 58:		Line 58:

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

Apm: /* Algebra with types */ added note on inverse functions.

2021-10-21T12:17:03Z

Algebra with types: added note on inverse functions.

← Older revision		Revision as of 14:17, 21 October 2021
Line 30:		Line 30:
	* : a -> a -> a -> b ~ ((b^a)^a)^a) = b^a^a^a … by convention		* : a -> a -> a -> b ~ ((b^a)^a)^a) = b^a^a^a … by convention
	* (a,a,a) -> b ~ b^(3*a)		* (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) ==		== Why function types correspond to ResultType^ArgumentType (and are called exponentials) ==