Hacker News Reader

Comment by sakras | Hacker News Reader

> Let’s pause for a moment to remember that we’re dealing with types. And the expression 1 / (1 - a) contains both a negative and a fractional type, neither of which have a meaning yet.

This makes me wonder, is there a ring of types? There's addition and multiplication. Division and subtraction aren't necessary to define a ring, so their absence isn't particularly surprising.

View on HN

A ring forms an Abelian group with just its additive operation, so you basically have subtraction there. As far I can tell the structure we have formed by these datatypes is a semiring.

Ah also the multiplication operation isn't commutative, since struct { int A; float B; } is different from struct { float A; int B; }. So maybe it's a "noncommutative semiring".

Ring don’t require multiplication to commute, only addition. (Square) matrices make just fine rings despite noncommutativity. But the semiring of types does have commutative multiplication (only a semiring, or "rig", because the lack of additive inverses).

Those two structs are equivalent (isomorphic) in the algebraic sense – names don’t matter, and order (indices are just a kind of names) doesn’t either. (a, b) = a x b = b x a = (b, a).

Technically yeah but there is a natural isomorphism between struct { int A; float B; } and struct { float B; int A; } so if you're willing to do everything up to isomorphism (which is usually completely fine and standard) then you get a commutative semiring.

You have to work up to isomorphism anyway even to get a noncomutative semiring because technically the multiplication isn't exactly associative only associative up to an isomorphism.

Reply on news.ycombinator.com