3 ms·

I think one of the most critical issues with thinking about ADTs in terms of an algebra is that they lack inverse operations which are otherwise an extremely cr

I think one of the most critical issues with thinking about ADTs in terms of an algebra is that they lack inverse operations which are otherwise an extremely critical component of how we conceive mathematics. A disjoint union type is formally equivalent to addition, but disunion is never defined, we are given no formal representation of subtraction. The same is given for cognates of division, of logarithms and roots (what those might look like is an interesting, if oft. neglected manner of research) There's (somewhat) good reasons we don't define these operations, of course. All the same, without being able to represent these inverse operations, the ease of which it maps to familiar notions of the typical algebras we're used to ends up thrown out the window. The algebra metaphor makes a bit more sense when you move beyond ADTs into more advanced levels of type-theory. Dependent types are a fair bit beyond a mere algebra, instead being more like a complete metalanguage akin to higher-order logic.

taeric 2y ago
I think this is underscoring my concern with this as a pedagogical thing. I have seen people try very hard to find analogs with basic algebra. And... by people, I mainly mean younger me. Building algebras is, I think, still a very valuable thing if you can do it. Often times, though, the goal is not to fully mimic the basic algebra of grade school, but to map out what is doable with the abstractions that you have.
Sharlin 2y ago
The algebra of types is a semiring, which is a generalization of a ring that drops the requirement of an additive inverse, just as a ring is a generalization of a field that doesn’t require a multiplicative inverse. Semirings are pretty common in math – hell, natural numbers form (only) a semiring, having neither type of inverse! Can’t get more fundamental than that. And of course the connection between naturals (counting numbers) and types is evident from the fact that we started this whole exercise by counting inhabitants and defining equivalent based on that!

taeric 2y ago

I think this is underscoring my concern with this as a pedagogical thing. I have seen people try very hard to find analogs with basic algebra. And... by people, I mainly mean younger me. Building algebras is, I think, still a very valuable thing if you can do it. Often times, though, the goal is not to fully mimic the basic algebra of grade school, but to map out what is doable with the abstractions that you have.

Sharlin 2y ago

The algebra of types is a semiring, which is a generalization of a ring that drops the requirement of an additive inverse, just as a ring is a generalization of a field that doesn’t require a multiplicative inverse. Semirings are pretty common in math – hell, natural numbers form (only) a semiring, having neither type of inverse! Can’t get more fundamental than that. And of course the connection between naturals (counting numbers) and types is evident from the fact that we started this whole exercise by counting inhabitants and defining equivalent based on that!