3 ms·

I am always torn when I see these discussions. Yes, I fully appreciate a lot of the easy algebra applies to some things. I further appreciate many of the opti

by taeric 2y ago

I am always torn when I see these discussions. Yes, I fully appreciate a lot of the easy algebra applies to some things. I further appreciate many of the optimizations that can be created by taking advantage of many of these. However, I have grown skeptical on its pedagogical use in programming. Specifically, I question if it is really how most people think in terms of programming. I further question if this is how most modelling considers things. An easy example would be chemistry. There are algebraic ideas in chemistry, but I would struggle to say how they look the same as this. Am I looking past an obvious aide to modelling that these approaches can give? I appreciate how this post acknowledges that there are not obvious uses of integration and such, but I feel that sort of proves my point. There are familiar mathematical tools that are good to use when we can. This does not mean you need to force them onto everything you have. It would probably help me a ton, if I ever saw these applied to state machines?

marcosdumay 2y ago
> Specifically, I question if it is really how most people think in terms of programming. No, of course not. Algebra is only useful when you want to manipulate that exact thing, and most programmers never do any complex manipulation of types. Compiler programmers writing powerful type systems do think that way. > There are algebraic ideas in chemistry, but I would struggle to say how they look the same as this. Oh no, they don't. The algebra of Quantum Mechanics is way weirder than that. (At least when you move after simple rotations and step-potential wheels.)
- taeric 2y ago
  Just to make sure I'm not misreading, this is largely an agreement? I think I'm fully in agreement that a compiler class should cover this. I will also hasten to say that I find it a fun topic, such that I don't think it should not be offered elsewhere. I just don't know that I can see a lot of application to general programming.
  - marcosdumay 2y ago
    > I think I'm fully in agreement that a compiler class should cover this. Then yes, I agree with you.
noelwelsh 2y ago
Here's a very simple example: A user can have one of two roles: Normal or Admin. You can model this as: - User = Name x Password x Role - Role = Normal + Admin or you can multiply it out and get - User = Admin or Normal - Admin = Name x Password - Normal = Name x Password Which you should choose depends on the application. The second representation forces you to consider at every step if you have an Admin or Normal user, which is better for security. The first representation is more convenient when you don't care about the role. I do these transformations a lot when modelling things. They are trivial, but if you don't understand the underlying algebra you might not see them (in the same way the developers who aren't used to sum types tend to be blind to them.) Does that help?
- galaxyLogic 2y ago
  What would be User x Role? Is it (Name x Password x Role) x (Normal + Admin) = ? What data-structure would that represent?
  - noelwelsh 2y ago
    If User = Name x Password x Role and Role = Normal + Admin Then (Name x Password x Role) x (Normal + Admin) = (Name x Password x Role) x Role = Name x Password x Role x Role (See the normal rules of algebra apply) In Ocaml you would write type Something = User * Role or type Something = Name * Password * Role * Role In Typescript you would have something like type Something = { user: User, role: Role } or type Something = { name: Name, password: Password, role1: Role, role2: Role } These two types are isomorphic (they have the same structure when you ignore irrelevant details) but you'd program with them slightly differently. Neither type makes a great deal of sense, but it's what you asked for. :-)
- taeric 2y ago
  I'm not clear that I see the benefit of the techniques here? For one, it is not necessarily obvious that the "or (|)" is not a distributive property. It is, instead, a population description? As such, it seems like it leads to a very weird statements compared to what you would get in other uses. For example, if instead of Role, it was IsAdmin, and IsAdmin = True | False, then your application here gets you the odd True = Name x Password. What does that even mean? It also has an odd one of what if Role = Normal + Admin + SuperAdmin, but User is still Admin | Normal? What does that even mean?
johnnyjeans 2y ago
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!

by taeric 2y ago

marcosdumay 2y ago

> Specifically, I question if it is really how most people think in terms of programming. No, of course not. Algebra is only useful when you want to manipulate that exact thing, and most programmers never do any complex manipulation of types. Compiler programmers writing powerful type systems do think that way. > There are algebraic ideas in chemistry, but I would struggle to say how they look the same as this. Oh no, they don't. The algebra of Quantum Mechanics is way weirder than that. (At least when you move after simple rotations and step-potential wheels.)

taeric 2y ago
Just to make sure I'm not misreading, this is largely an agreement? I think I'm fully in agreement that a compiler class should cover this. I will also hasten to say that I find it a fun topic, such that I don't think it should not be offered elsewhere. I just don't know that I can see a lot of application to general programming.
- marcosdumay 2y ago
  > I think I'm fully in agreement that a compiler class should cover this. Then yes, I agree with you.

noelwelsh 2y ago

Here's a very simple example: A user can have one of two roles: Normal or Admin. You can model this as: - User = Name x Password x Role - Role = Normal + Admin or you can multiply it out and get - User = Admin or Normal - Admin = Name x Password - Normal = Name x Password Which you should choose depends on the application. The second representation forces you to consider at every step if you have an Admin or Normal user, which is better for security. The first representation is more convenient when you don't care about the role. I do these transformations a lot when modelling things. They are trivial, but if you don't understand the underlying algebra you might not see them (in the same way the developers who aren't used to sum types tend to be blind to them.) Does that help?

galaxyLogic 2y ago
What would be User x Role? Is it (Name x Password x Role) x (Normal + Admin) = ? What data-structure would that represent?
- noelwelsh 2y ago
  If User = Name x Password x Role and Role = Normal + Admin Then (Name x Password x Role) x (Normal + Admin) = (Name x Password x Role) x Role = Name x Password x Role x Role (See the normal rules of algebra apply) In Ocaml you would write type Something = User * Role or type Something = Name * Password * Role * Role In Typescript you would have something like type Something = { user: User, role: Role } or type Something = { name: Name, password: Password, role1: Role, role2: Role } These two types are isomorphic (they have the same structure when you ignore irrelevant details) but you'd program with them slightly differently. Neither type makes a great deal of sense, but it's what you asked for. :-)
taeric 2y ago
I'm not clear that I see the benefit of the techniques here? For one, it is not necessarily obvious that the "or (|)" is not a distributive property. It is, instead, a population description? As such, it seems like it leads to a very weird statements compared to what you would get in other uses. For example, if instead of Role, it was IsAdmin, and IsAdmin = True | False, then your application here gets you the odd True = Name x Password. What does that even mean? It also has an odd one of what if Role = Normal + Admin + SuperAdmin, but User is still Admin | Normal? What does that even mean?

johnnyjeans 2y ago

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!