> 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."