4 ms·

This also helps with figuring out isomorphisms, i.e. when two types are equivalent. So for example, if someone tries to represent an "Either Bool Bool" (2+2 cas

by kqr 2y ago

This also helps with figuring out isomorphisms, i.e. when two types are equivalent. So for example, if someone tries to represent an "Either Bool Bool" (2+2 cases) with three cases, we see immediately there's a singularity in there which represents at least two of the possible values of the original, i.e. we won't be able to losslessly round trip.

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 ago
  Yep, 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 ago
    That'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 ago
      Sure, 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.
weitendorf 2y ago
The thing about isomorphisms between algebraic structures is that they require a representational+inversible mapping (what you mentioned) that preserves relations (something you didn't mention). That distinction is actually relatively important in programming because you might be using something like polymorphism to operate on two representationally equivalent types in different ways. If you have a base class CollidableObject that both PoolBall and GlobOfHoney extend, they could be representationally equivalent (both having two vector member fields, one for Position and one for Velocity) but with different implementations of CollidableObject::HandleCollision(CollidableObject& target) to reflect the fact that PoolBall can elastically collide with certain kinds of targets but GlobOfHoney only collides inelastically. So you'd not want to treat them as isomorphic. I'm mostly just being pedantic but one of my pet peeves is when programmers use terms like Isomorphism or Vector in a way that is partly but not entirely true to the mathematical definition. I think "bijection" is a better term for what you're talking about, because it's both necessary and sufficient for information-preserving mapping between types.

by kqr 2y ago

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 ago
Yep, 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 ago
  That'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 ago
    Sure, 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.

weitendorf 2y ago

The thing about isomorphisms between algebraic structures is that they require a representational+inversible mapping (what you mentioned) that preserves relations (something you didn't mention). That distinction is actually relatively important in programming because you might be using something like polymorphism to operate on two representationally equivalent types in different ways. If you have a base class CollidableObject that both PoolBall and GlobOfHoney extend, they could be representationally equivalent (both having two vector member fields, one for Position and one for Velocity) but with different implementations of CollidableObject::HandleCollision(CollidableObject& target) to reflect the fact that PoolBall can elastically collide with certain kinds of targets but GlobOfHoney only collides inelastically. So you'd not want to treat them as isomorphic. I'm mostly just being pedantic but one of my pet peeves is when programmers use terms like Isomorphism or Vector in a way that is partly but not entirely true to the mathematical definition. I think "bijection" is a better term for what you're talking about, because it's both necessary and sufficient for information-preserving mapping between types.