| ▲ | taeric 3 days ago |
| The name for them feels a bit unfortunate, to me. The vast majority of programmers know of algebra from grade school, at best. And there you think of algebra as being able to do symbolic operations on equations. Not so much as "algebra over a field." I think it is fair to say that that is the more unfortunate naming, maybe? I still contend that that is what people think of when they hear the term, though. |
|
| ▲ | dfabulich 3 days ago | parent | next [-] |
| I strongly agree. Algebraic types aren't "scary," but "algebraic types" is a bad term for what they are. In all popular languages that support "sum types" we just call them "unions." Your favorite programming language probably already supports unions, including Python, TypeScript, Kotlin, Swift, PHP, Rust, C, and C++. C# is getting unions next year. The article never mentions the word "union," which is overwhelmingly more likely to be the term the reader is acquainted with. It mentions "sets" only at the start, preferring the more obscure terms "sum types" and "product types." A union of type sets kinda like a sum, but calling it a "sum" obscures what you're doing with it, rather than revealing. The "sum" is the sum of possible values in the union, but all of the most important types (numbers, arrays, strings) already have an absurdly large number of possible values, so computing the actual number of possible values is a pointless exercise, and a distraction from the union set. Stop trying to make "algebraic" happen. It's not going to happen. |
| |
| ▲ | chrisnight 3 days ago | parent | next [-] | | > In all popular languages that support "sum types" we just call them "unions." When I was doing research on type theory in PL, there was an important distinction made between sum types and unions, so it’s important not to conflate them.
Union types have the property that Union(A, A) = A, but the same doesn’t hold for sum types. Sum types differentiate between each member, even if they encapsulate the same type inside of it.
A more appropriate comparison is tagged unions. | | |
| ▲ | adastra22 3 days ago | parent | next [-] | | What you are calling Union type is not what GP is talking about. | |
| ▲ | wasabi991011 3 days ago | parent | prev [-] | | So, disjoint union in set theory terms? If I understand correctly . |
| |
| ▲ | dkarl 3 days ago | parent | prev [-] | | > Stop trying to make "algebraic" happen. It's not going to happen It's been used for decades, there's no competitor, and ultimately it expresses a truth that is helpful to understand. I agree that the random mixture of terminology is unhelpful for beginners, and it would be better to teach the concepts as set theory, sticking to set theoretic terminology. In the end, though, they'll have to be comfortable understanding the operations as algebra as well. | | |
| ▲ | dfabulich 3 days ago | parent [-] | | No, seriously, you literally never need to understand the operations as algebra. You just need to know how to use your language's type system. None of the popular languages call them sum types, product types, or quotient types in their documentation. In TypeScript, it's called a "union type," and it uses a | operator. In Python, `from typing import Union`. In Kotlin, use sealed interfaces. In Rust, Swift, and PHP, they're enums. There are subtle differences between each language. If you switch between languages frequently, you'll need to get used to the idiosyncrasies of each one. All of them can implement the pattern described in the OP article. Knowing the language of algebraic types doesn't make it easier to switch between one popular language to another; in fact, it makes it harder, because instead of translating between Python and TypeScript or Python and Rust, you'll be translating from Python to the language of ADTs (sum types, tagged unions, untagged unions) and then from the language of ADTs to TypeScript. People screw up translating from TypeScript to ADTs constantly, and then PL nerds argue about whether the translation was accurate or not. ("Um, actually, that's technically a tagged union, not a sum type.") The "competitor" is to simply not use the language of algebraic data types when discussing working code. The competitor has won conclusively in the marketplace of ideas. ADT lingo has had decades to get popular. It never will. ADT lingo expresses no deeper truth. It's just another language, one with no working compiler, no automated tests, and no running code. Use it if you enjoy it for its own sake, but you've gotta accept that this is a weird hobby (just like designing programming languages) and it's never going to get popular. | | |
| ▲ | dkarl 3 days ago | parent | next [-] | | If you're so confident that algebraic data types will never become popular, I don't understand why you feel it's so important to convince a few nerds not to talk about them. I don't think anyone here is advocating making the topic compulsory. There will always be some people who are interested in theory and others who aren't. | |
| ▲ | WorldMaker 2 days ago | parent | prev [-] | | > None of the popular languages call them sum types, product types, or quotient types in their documentation. It seems like you may want to spend a bit more time with the ML family of languages. Sure, you can argue the degree of what constitutes "popular" but OCaml and F# routinely make statistics on GitHub and Stack Overflow. The ML family will represent tuples as products directly (`A * B`), and sometimes use plus for sum types, too (though yes `|` is more popular even among the ML family), which they do call sum types. > Knowing the language of algebraic types doesn't make it easier to switch between one popular language to another The point of ADTs is not to build a universal type system but to generalize types into Set thinking. That does add some universals that a sum type should act like a sum type and a product type should act like a product type, but not all types in any type system are just sum types or just product types. ADT doesn't say anything about the types in a type system only that there are standard ways to combine them. It says there are a couple of reusable operators to "math" types together. > ADT lingo expresses no deeper truth. Haskell has been exploring the "deeper truths" of higher level type math for a long while now. Things like GADTs explore what happens when you apply things like Category Theory back on top of Algebraic Data Types, that because you have a + monoid and * monoid, what sorts of Monads do those in turn describe. Admittedly yes, a lot of those explorations still feel more academic than practical (though I've seen some very practical uses of GADTs), but just because the insights for now are mostly benefiting "the Ivory Tower" and "Arch Haskell Wizards" doesn't mean that they don't exist. The general trend of this sort of thing is that first academia explores it, then compilers start to use it under the hood of how they compile, then the compiler writers find practical versions of it to include inside their own languages. That seems to be the trend in motion already. Also, just because it's a relatively small audience building compilers doesn't mean we don't all benefit from the things they explore/learn/abstract/generalize. We might not care to know the full "math" of it, but we still get practical benefits from using that math. If a compiler author does it right, you don't need to know mathematical details and jargon like "what is a product type", you indeed just use the fruits of that math like "Tuples". The math improves the tools, and if the language is good to you, the math provides you with more tools and more freedom to generalize your own algorithms beyond simple types and type constructs, whether or not you care to learn the math. (That said, it does seem like a good idea to learn the type math here. ADTs are less confusing than they sound.) |
|
|
|
|
| ▲ | bananaflag 3 days ago | parent | prev | next [-] |
| I always thought "algebraic" sounds unscary because in high school / undergraduate, algebra feels easier than analysis. Now, "analytic data types", that would be something. |
| |
| ▲ | taeric 2 days ago | parent | next [-] | | Apologies, I missed this yesterday. It isn't that it is scary. It is that it connotes something about equations and such. It is literally the name of the class people learn how to symbolically solve quadratic equations and such. I was saying in another thread that I think this would be a lot more obvious if people actually did algebra on the types. But we don't. At least, I can't recall ever seeing it done. Closest I've seen is in places where people have to do so to justify the naming here. And I want to be clear, I specifically mean using + and * with types. And not that it can be done. Is it done? | |
| ▲ | thechao 3 days ago | parent | prev | next [-] | | Right. So, there's a unit type: the type that the sum of returns the other type, i.e., a + () = a
So that means there's an identity type for the product type operator: a * 1 = a
I.e., the type that you can "multiply" by that doesn't give you a two-field tuple, but just returns the single-field tuple. If "1" is a type, then we can build a sum-type with it: a + 1 = (a, 1)
Ok. Cool. But! If we can "add 1", then we should be able to remove "1", right? That kinda implies that "-1" exists: (a, 1) -1 = (a,) # don't shoot the messenger, I'm just riffing
But, that also implies that we can allow a product type whose result is the "-1" type? (i, i) = -1
OH NOES! | |
| ▲ | adastra22 3 days ago | parent | prev [-] | | Why not just “struct” or “record” and “enum” or “variant”? |
|
|
| ▲ | dkarl 3 days ago | parent | prev [-] |
| I think the term "algebra" is nice and neutral, common ground from grade school through college mathematics and higher, and I think it's a good clue for someone who doesn't have much math background. "You know how you learned to do math operations on numbers, and then in algebra class you learned to do them on other things like variables and equations? You can do operations on types as well." It's inevitable that someone starting from zero like this needs some time to get used to the ideas. Nobody learns this stuff instantly. Even if they can read an explanation in ten minutes and understand every word of it, it still takes time for the ideas to sink in and become natural. That's why an undergraduate math course might only cover a couple hundred pages in a semester. For someone not used to the process of absorbing ideas like these, the time it takes can be confusing and disappointing, but it's normal. I think one point of confusion that could be avoided is that areas of math that are initially taught as separate topics often get freely mixed in introductory explanations of type theory. For example, someone who is exposed to a little bit of set theory in one class, and a little bit of logic in another, probably thinks of these things as separate from each other and both separate from algebra. But then an explanation like this confuses them by freely interchanging "union" and "sum" and the operator "|" which programmers learn as logical "or." Ideally, I think an introduction should stick to a single set of terminology from one area (I would pick set theory) at first, and after the student is comfortable with the concepts and operations, only then show how the other terminology maps to the ideas the student has learned. |
| |
| ▲ | taeric 3 days ago | parent [-] | | Oddly, that is precisely my problem with it as a name. I can't do any "basic algebra" operations on these things. I say this as someone that is having to help my grade schoolers learn algebra this week, actually. :D I can squint to see where things are going and how they intersect. But it takes a lot of squinting. | | |
| ▲ | dkarl 3 days ago | parent | next [-] | | You can add and multiply. You have to learn what add and multiply mean with types. There was a time when you only knew how to add and multiply with numbers, and you had to learn how to deal with things like "x". It's confusing for most kids at first, and they spend weeks getting used to it. I'd say that virtually anybody who has learned grade school algebra will learn to add and multiply types faster than they learned to add and multiply polynomials. "Squaring" and "cubing" is an easy way to build intuition with type multiplication, because the name helps you visualize the result. If you have a type C with three values {red, green, blue} then C^2 = C x C is a "square" of values: (red, red) (red, green) (red, blue)
(green, red) (green, green) (green, blue)
(blue, red) (blue, green) (blue, blue)
and C^3 = C x C x C can be visualized as a "cube" of values.You can imagine arranging other products of finite types in the same way: class Foo(color: C, enabled: Boolean)
// the values of Foo can be arranged in a 3x2 array
Foo(red, true) Foo(red, false)
Foo(green, true) Foo(green, false)
Foo(blue, true) Foo(blue, false)
This is analogous to how kids are taught to multiply 3 x 2. | | |
| ▲ | taeric 3 days ago | parent [-] | | Like I said, I can squint to see what you mean. But people tend to treat types more as what grade schools call units. And those act more as constraints on what you can do with the values. With you doing add/multiply on the values. Note that I'm not necessarily arguing that things should change. At this point, I'd consider the name fairly well established. But, it should be noted much more heavily that you are doing algebra on the types and that this does not imply anything that you can do with the values they may represent at any time. | | |
| ▲ | dkarl 3 days ago | parent | next [-] | | > But people tend to treat types more as what grade schools call units. And those act more as constraints on what you can do with the values. With you doing add/multiply on the values. Ah, I see. Yes, it doesn't make sense unless you see types as sets of values. I haven't been super deep into type theory, so I don't know how far that definition takes you, but it's the intuitive/naive starting place for understanding the idea of algebraic data types. The addition and multiplication operations are on sets of values and don't have anything to do with adding or multiplying the values themselves. | | |
| ▲ | taeric 3 days ago | parent [-] | | Thinking a little more about it, I would wager it would be a lot easier if people used the + and * when combining types. As things are, we say that that is what defines them being algebraic, but then never use + and *. Would be a lot easier if Maybe[String] was defined as [String + None] and similar. (I... don't actually know if that was classically done?) | | |
| ▲ | dkarl 3 days ago | parent [-] | | I think they both have advantages. "Union" directly references the set operation, which helps keep you concretely grounded when learning the concept. + references a different level of abstraction, which is fine after you've internalized the operations, but probably a bit confusing to start with. | | |
| ▲ | taeric 3 days ago | parent [-] | | Certainly. Names are important, as much as it annoys us. My question was more on if you could move the algebra into more focus in the types defined. Specifically, I don't think I've seen people use +/* in describing the type that often. Or ever, really. As an example, I could see defining an Either<A, B> as (A + B) as a fairly easy to understand example that would make it very easy to see the algebra being described. Though, at that point, I confess I don't know of any common product types by name. Tuple, but that is not really satisfying to me, for some reason. (Fully ack that is a me problem.) Could easily explain this using cards. You start with the types of Suite and Rank. With a Card being (Suite * Rank). This nicely could show that asking about a Suite is effectively asking about only part of the type for any Card. I'll probably be slightly thinking on this longer than makes sense. :D | | |
| ▲ | dkarl 3 days ago | parent [-] | | When you start thinking about real programming languages, most of them don't assign any meaning to A + B or A * B, so it's up to you to construct types that act like those types. Product types are easiest. Tuples or case classes / record types act like product types. In the case of the Foo type I defined above, it's easy to see that for each pair (c, b) in C x Boolean, there is one value of Foo, Foo(c, b), and vice-versa. Sum types are weird, because in practice you often don't have a guarantee that two types are disjoint. Because of this, you typically don't see sum types in use without wrapper types that distinguishes the two cases. For example, the instances of Either<A, B> are typically Left(a) for some a in A or Right(b) for some b in B. To see why this is important, consider a sum type combining Option<A> + Option<B>. The value None belongs to both types, and you can't tell if None arose as a value of Option<A> or Option<B>. In practice, this distinction matters more often than not. For a more extreme value of non-disjoint union, consider a library function fetch<A>(extract: Response -> A): Either<A, Int>
that calls an HTTP API, extracts a value of type A from the response, and returns either the extracted value or, if extract fails, the HTTP status code of the response. If you extract a value of type Int from the response, the return value is Either<Int, Int>. A simple sum type Int+Int is useless here, because you won't be able to tell if 404 was the value extracted from the response or the HTTP response code.For these reasons, Either<A, B> isn't a sum of A and B, but rather a sum of Left<Int> + Right<Int>. One place sum types are useful is combining enumerations, because different enumerations have distinct values. For example: enum ClientErrors { BadRequest, NotFound }
enum ServerErrors { InternalServerError, BadGateway }
APIErrors = ClientErrors + ServerErrors
| | |
| ▲ | taeric 3 days ago | parent [-] | | Right. Apologies, but I know the basics. My argument is that "algebraic types" would be less confusing if you actually did algebra using the types. That is it. That is my full argument. As it is, you have to go through hoops to show what the algebra of the types is. And how that maps to whatever subtyping rules that the popular language you are using is. Now, my argument is not that there is not some usefulness to understanding the algebra you can do with types. Quite the contrary. I think that is very useful and people should try to understand it. But my argument remains that without using the common operations that define algebras, namely + and *, that calling them algebraic types does not provide any help in understanding the types for people. It remains an unfortunate naming based on how people are commonly introduced to the term "algebra." |
|
|
|
|
| |
| ▲ | mrkeen 3 days ago | parent | prev [-] | | Units also receive the add/multiply treatment. | | |
| ▲ | taeric 3 days ago | parent [-] | | Sort of? If you multiply two values, then the units also multiply. But if you add, they do not. They just have to be equal. No? Even there, there is a very different thing from "adding units" and "adding values that have units." |
|
|
| |
| ▲ | adastra22 3 days ago | parent | prev [-] | | Where are grade schoolers learning algebra? | | |
| ▲ | taeric 3 days ago | parent [-] | | Just google "algebra 1." Largely, it is where they learn to do symbolic math. Lots of time spent on quadratics. | | |
| ▲ | adastra22 3 days ago | parent [-] | | Yes, where I live (Silicon Valley) the earliest you can take algebra 1 is in middle school, and that is the accelerated pathway for the smart kids. | | |
| ▲ | taeric 3 days ago | parent [-] | | Ah, I see that "grade school" is sometimes defined as just to 6th grade or so. I have always used it to include all schooling up to college. So, apologies on that. I am referring to the same stuff you are mentioning. I don't think that changes my point, at all? | | |
| ▲ | adastra22 3 days ago | parent [-] | | No it doesn’t, I was just curious. And yeah in the US grade school is just through 5th grade, and 6th grade in most of the rest of the world. Synonymous with elementary school AFAIK. I think the US is far too slow in introducing algebra, with it standardly being taught in 9th grade. So that made me curious. | | |
| ▲ | taeric 3 days ago | parent | next [-] | | I don't remember my school days, oddly. For my kids, they don't have an "algebra" class until later. But they do basic symbolic math far sooner. I know they have done what we would call linear systems of equations as early as 6th grade. Different number systems even earlier. My 9th grader is in an algebra class. I don't remember if it is 1 or 2. I'm still not entirely clear I see the obvious path from the things they are doing to algebraic types. | |
| ▲ | jghn 3 days ago | parent | prev [-] | | > in the US grade school is just through 5th grade, and 6th grade in most of the rest of the world Be careful with this. Where I grew up in the US, "Grade school" was usually through 6th grade with a grade 7-8 middle school or just 1-8. |
|
|
|
|
|
|
|