3 ms·
This works with function types too. You can get a hint that objects with signature A -> (A -> A) have an isomorphism with objects of signature (A × A) -> A, by
by perihelions 2y ago
This works with function types too. You can get a hint that objects with signature A -> (A -> A) have an isomorphism with objects of signature (A × A) -> A, by observing that the cardinalities are equal as algebraic expressions, ( |A|^|A| )^|A| = |A|^( |A|*|A| ). That one's just "currying" [0].
[0] https://en.wikipedia.org/wiki/Currying https://en.wikipedia.org/wiki/Currying
- Sharlin 2y agoYep, that’s one of the more mind-blowing "tricks" as it were. Maybe less moreso, but still nifty, is that |T -> bool| = |bool|^|T| = 2^|T| …which also happens to be the number of subsets of a set of size |T|. And indeed that’s what a predicate function is, a subset-generator; for every subset there is exactly one predicate that picks the members of that subset from the larger set.
- gpderetta 2y agoThat's true for any type, not just bool right? And is equivalent of to the observation that any pure function can be replaced by a lookup table.
- Sharlin 2y agoSure, any function T -> U partitions T into |U| subsets. But the case where |U|=2 is special because 2^N is special in being the number of subsets of a set of size N.