Algebraic Types are not Scary, Actually
65 points by aiono
65 points by aiono
My favorite demonstration for beginners is a type that describes playing cards. It’s more familiar (for those who ever played card games, anyway) than ASTs, and you can show rank comparison, etc.
type suit = Diamonds | Hearts | Spades | Clubs
type card =
Ace of suit
| King of suit
| Queen of suit
| Jack of suit
| Numeral of (suit * int)
I would do it more like:
type rank =
| Ace
| Two
| Three
| Four
| Five
| Six
| Seven
| Eight
| Nine
| Ten
| Jack
| Queen
| King
type suit = Diamonds | Hearts | Spades | Clubs
type card = Standard of rank * suit | Joker1 | Joker2
I may be going a bit overboard though :-)
This definitely makes the minimal set of states representable (i.e. there’s no such thing as a 37 of hearts, which Numeral of (suit * int) allows)
A better way might be to declare a subtype of int with the range 2-10.
Guess it depends on what the language supports, and what operations the data type is trying to support.
What would that look like? What you’re saying sounds like it requires refinement or dependent types.
Honestly I was thinking of Ada when I mentioned it, I don’t know if ML has support for it.
In Ada it could be done a couple of ways:
-- A new type
type card_rank is range 2 .. 10;
-- A subtype of integer
subtype card_rank is Integer range 2 .. 10;
IIRC the first one specifies a new numeric type altogether, while the second one is still an integer, but always restricted to the specified range.
It could be done with a runtime check that validates the number, eg
module CardNumber : sig
type t = private int
val of_int : int -> t
end = struct
type t = int
let of_int i = assert (i > 1 && i < 11); i
end
Yea this is practically a great pattern (usually called “smart constructors”), but worth noting that this shifts the check to runtime and not compile time.
This triggered an old memory: Peter Norvig’s Design of Computer Programs starts with a set of problems about ranking poker hands. He uses Python (and no algebraic data types) but the way he uses lexicographic comparisons of tuples for hand ranking stuck with me as a really elegant way to strength-reduce the problem. I assume this is standard in computer implementations of poker (I wouldn’t know), but it’s very neat.
That is cool, and you can do the same thing with sum types: the default Ord implementation will compare different cases by the order you declare them, then break ties going field-by-field lexicographically.
Handy for things like type UpperBound = Finite Int | Infinite, if you want to treat a missing value as greater than any finite value.
That’s a great example! I seen it before but it didn’t came on my mind while I was writing this article.
So basically it’s addition and multiplication over types.
Spot on. They have a somewhat fancy name, but truly, a language without both operations in its type system is permanently hamstrung. Expressing everything as multiplication (records) just isn’t ergonomic. Addition (unions / enums) is a totally universal data modeling concept.
The way that I like to phrase it is that product types (tuples/records/structs) are for when you have some data AND some other data, and sum types (unions/enums/adts) are for when you have some data OR some other data. I like this phrasing because it makes it obvious how fundamental and basic it is, to be able to easily model when you have one thing OR another.
Yep that’s totally accurate. And –> multiplication, Or –> addition are intimately linked. This relationship shows up all over logic.
That is also exactly what you get from the Curry-Howard isomorphism. The conjunction (AND) of propositions corresponds to the product of types and the disjunction (OR) of propositions corresponds to the sum of types.
Classic real world example:
type SomeState = {
data: A | null,
isError: boolean
isLoading: boolean
}
this data type’s cardinality is 8, when it should be just 3 forcing you to model states that are impossible in your application.
An aside to the content, I know people clamor for dark mode blogs, but I prefer light mode when I am reading long texts. Firefox’s reader mode is nice, but you lose the syntax highlights in code blocks that make code pleasant to look at.
I’ve read several articles like this where it describes type theory concept to non-PLT people, but this description of the types as “having X many different possible values” worked for me to understand the theory. Are there any type systems that “subtract” or “divide” types to remove possibilities from an existing type to create new types? That is, without having to define a whole new type with less members? I’m thinking how useful this could be in creating DTOs, for example.
On the topic of sum types, are there any languages that specialize the variants somehow to maximize layout? IIRC for Rust, every variant is the size of the biggest variant, so if you’re stuffing product types directly in the sum type, it can be quite wasteful.
Are there any type systems that “subtract” or “divide” types to remove possibilities from an existing type to create new types?
Does TypeScript count?
type Foo = Abc | Def | Ghi | Jkl;
type Bar = Exclude<Foo, Ghi>;
// Bar is now Abc | Def | Jkl
Are there any type systems that “subtract” or “divide” types to remove possibilities from an existing type to create new types?
Subtraction and division turn out to be hard. As @refinement-systems wrote, there are “quotient” types which restrict a type wrt a predicate, so unlike sum and product types, quotient types are not purely a type-construction operator on types.
Conor McBride has a paper on dividing data types, “clowns to the left of me, jokers to the right”, which is a follow-up to their famous paper “the derivative of a regular type is its type of one-hole contexts”. But “clowns” is fairly heavy going if you aren’t steeped in dependent types.
The next easiest algebraic type operators after sums and products are function types, which correspond to exponentiation; derivatives correspond to a split in a purely functional data structure that occurs during copy-on-write mutation; and dependent pairs and functions are written with big-sigma and big-pi because they correspond to iterated sums and products. (I wrote about this a few months ago.)
are there any languages that specialize the variants somehow to maximize layout?
That is completely normal for functional languages that do not allow mutation everywhere, i.e. the ML family, Haskell, etc. When (like Rust) you allow the variant of a sum type to be modified in place, you have to reserve space for the largest variant. If you don’t allow that kind of mutation, you can shrink the space so it’s a snug fit for only the variant you are constructing.
I think subtraction isn’t conceptually, it’s types with a value constraint. You could say “All even numbers” is {i in int: x % 2 == 0}, or alternatively Int - OddInt.
The tricky bit is that this is really hard to typecheck.
The tricky bit is that this is really hard to typecheck.
SMT solvers are doing ok with that, and anyone who wants to implement such a language can grab an exisiting solver like Z3. it’s just that they themselves tend to be complicated and some people don’t trust their output.
Back when I was working on https://letlang.dev where types are basically functions to determine if the passed argument belong to the type or not, I was looking at Z3 to implement static typing.
I ended up giving up because:
They’re okay for simple refinements, but you can easily encode undecidable types, like “the type of all solvable diophantine equations”.
PS. if you see the term “dependent product”, be very suspicious: it can mean either “dependent pair” (because a pair is a product) or “dependent function” (because a big-pi is a product), so you need to look carefully at the context to disambiguate.
Great post. I think it’s worth highlighting the deriviative thing: it turns out that it’s completely reasonable to take the partial derivative of a type with respect to one of its type variables, and it results in something very useful.
That is completely normal for functional languages that do not allow mutation everywhere, i.e. the ML family, Haskell, etc.
I didn’t know that but it totally makes sense. In this case, does every object has an indirection? For instance if you have a list of a variant type, then each cell can have different sizes based on the variant. But if it’s just a pointer to the data then the sizes of the cells are the same.
Usually yes every value is represented as a pointer to the heap, tho there are optimizations for word-sized primitive types. For instance, Ocaml has 63 bit ints because one bit is used as an int/ptr type tag. Haskell has unboxed types which are more sophisticated.
It feels to me like the decreasing utility as you go deeper into the numeric rabbit hole starting at reals, going to imaginary numbers, then quaternions, then octonions. Yeah it can be done, but no I don’t want to.
We aren’t dealing with fancy numbers here, nothing as exotic as the reals let alone the rest.
I think part of why subtraction and division are awkward is related to the natural numbers being closed under addition, multiplication, and exponentiation; if you introduce subtraction you have to deal with integers, and if you introduce division you have to deal with rationals. And the simple counting analogy breaks because it isn’t obvious what it means for the cardinality of a data type to be negative or fractional.
This paper (from 2012) proposes meanings for negative and fractional types. If I understood correctly:
There are use cases for subtraction. Imagine that String is an interface defining a set of methods for an abstract string type and MutableString the ones that are added to it to make a mutable string type. If MutableString is a subtype of String, then you can just write String anywhere where you’re happy to accept a mutable or immutable string, or MutableString where you require a mutable string. But how do you accept only immutable strings? If you have subtraction, you can write String & !MutableString.
Unfortunately, it also makes type checking really hard for compilers to reason about.
a common feature request when I worked on python type checking was a way to represent “proper subtypes”, i.e. “any subclass of A, but not A itself”.
Are there any type systems that “subtract” or “divide” types to remove possibilities from an existing type to create new types?
I’ve never heard of “divide” types.
I’ve worked with type subtraction, and I’ve worked with “and-not” types, and they sometimes end up both using the “-” operator.
The and-not one is very interesting, because it’s the desire to be able to say “something might of type T1, but it must not be of type T2”. This can occurs quite easily in a type flow system (e.g. in a compiler that does inference or type flow analysis), such as the inferred type for the expression e inside the curlies: if (e.is(T1) && !e.is(T2)) { ... }
Type subtraction is also quite useful when describing an unnamed type based on named types, or on some combination of named types and pieces/parts of types, e.g. when carving up trait/interface types to reduce their surface area. I actually ran into an example earlier today in a test, where it was subtracting the surface area of the Object interface from the definition of another interface for purposes of delegation. (Remember, this was something that I saw in a test, so don’t reason too hard on what it’s doing.)
class NamedNumber(String name, Int number)
delegates Stringable(name) {}
class NamedNumber2(String name, Int number)
delegates Stringable-Object(name) {}
Are there any type systems that “subtract” or “divide” types to remove possibilities from an existing type to create new types?
You mean something like refinement types? As in:
Or like quotient types, a different kind of type “division”?
I don’t have the vocabulary to talk about the topic, but I appreciate everyone’s links to give me more reading!
Thanks for the styling feedback. The website has both styles according to your system preference. But it doesn’t have a manual toggle to switch between light and dark.
I am glad if you found it helpful!
Are there any type systems that “subtract” or “divide” types to remove possibilities from an existing type to create new types?
I also wondered about the same thing. I am not aware of any but I am just a masters student so I just a beginner in the field. I didn’t think about it deeply but subtraction can be useful if you want to partially match some variants from a sum type and leave the rest as a smaller sum type. For division I am not sure how could be useful.
On the topic of sum types, are there any languages that specialize the variants somehow to maximize layout
Entity component system kind of solves this by having a separate array for each variant. But I didn’t see any language that handles everything for you and presents a sum type.
One more stye feedback: in light mode the code samples are nearly unreadable–contrast is too low. Axe DevTools browser extension will easily pinpoint all these. My guess is the code highlighter is styled for dark mode, hence why it doesn’t work for light mode.
Could you share a screenshot with me? I noticed it before and overrided the background on code block to be dark regardless of the light/dark preference. Is this not happening on you?
I took a screenshot and uploaded it to the first website that showed up for “share picture online”, if you don’t mind the slightly sketchy hosting – https://ibb.co/5xhzfx4K
I realized it works as expected on Firefox but not on Chrome. Thanks for letting me know, I will fix it when I have time.
Well, not quite so simple. I took that screenshot in Firefox. It looks the same to me in Chrome. But if you’re able to reproduce locally, that’s the important thing.
Interesting, because both on my mobile and laptop Firefox behaves as desired but Chrome displays a lighter background on code blocks.
Edit: I was able to reproduce it in Firefox as well. You were right.
Are there any type systems that “subtract” or “divide” types to remove possibilities from an existing type to create new types?
I worked on something similar in the past: https://letlang.dev/spec/symbols/class/
And Elixir now has a gradual type system that can use function guards.
“Algebraic types” is such an unnecessarily fancy term for the concept of tagged unions.
Tagged unions are frequently done wrong so I think “algebraic” usefully implies that the language upholds safety and probably has pattern matching too.
Is “the programming language prevents the user from doing something unsafe” really a concept in algebra or the concept of a sum in math?
If not, maybe these are things that are specific to programming and don’t really have anything to do with math?
I believe a C struct with a tag and a union can be uncontroversially argued to be a mathematical sum of types. It relies on the programmer doing everything correctly of course, like anything else in C, but it is a concrete implementation of the concept. If you want a term which differentiates “good sum types” from “bad sum types”, invent one.
I believe a C struct with a tag and a union can be uncontroversially argued to be a mathematical sum of types.
I disagree, because tagged C union has more possible values than the corresponding sum type. You have the wrong tag with the union value, which shouldn’t exist according to sum type definition.
A tagged C union that’s used according to certain constraints (i.e you don’t put the wrong value in the tag field) is an implementation of a mathematical sum of types. Just like a Rust enum that’s used according to certain constraints (i.e you don’t use mem::transmute and other tricks to mess with the tag) is an implementation of a mathematical sum of types. Or a struct Vector2 { float x; float y; } is an implementation of a 2D vector if used according to certain constraints (i.e you don’t put NaN in x and y, and you never let both x and y be 0 at the same time).
All real-world implementations of a mathematical concept will have ways to be used in ways which aren’t allowed by the mathematical concept. That’s by necessity. It doesn’t invalidate the relationship between the real world implementation and the mathematical concept.
Fair enough. I agree that C tagged union pattern is related with the sum type concept, albeit it’s a very poor version of it as it relies on convention a lot. Just like an integer representation that can represent any integer and not limited to any range represent mathematical integers better, sum type implementation that doesnt let you construct invalid values is closer to the mathematical sum type concept.
I feel like I’ve had this discussion before, whether with you or someone else, but you are conflating the low-level implementation details of one possible way to represent algebraic data types in memory, with the abstract concept of algebraic data types.
The point of algebraic data types is not that the in-memory representation looks in a particular way, it is that the language enforces certain invariants about using them.
It relies on the programmer doing everything correctly of course
That’s like saying Go has algebraic data types because one can write
type result struct {
is_ok bool
result_value int
error_value string
}
and expect the user to only use it in a particular way. That’s false. It’s false, not because the memory layout is different from what you would get with a tagged union, but because the language doesn’t enforce safe usage.
To reiterate: The particular way a language with algebraic data types (such as Haskell, SML, Rust, Elm and many others) choses to represent values of such types in memory is irrelevant. The memory-representation is never exposed to the user.
Your later point about using mem::transmute in Rust is irrelevant, because unsafe allows the developer to explicitly opt out of these language guarantees.
So in your opinion, is std::variant in C++ with compiler options to abort on misuse an example of “good sum types”? That enforces invariants automatically rather than through convention.
I don’t know enough about C++ or std::variant to say. Do you think it is?
I think it’s inarguably an implementation of sum types (tho I think C tagged enums are too). It’s also an implementation of sum types with invariant checking. But I don’t think they’re what functional programmers mean when they say that languages should have sum types. And I certainly wouldn’t say that std::variant is a good implementation of sum types.
I think functional programmers want a specific kind of sum type implementation where pattern matching is the preferred (or only) way to access a particular field.
C++ doesn’t have pattern matching syntax, and the preferred way to access a field is to ask for a pointer to it via std::get_if and check if the pointer is null.
maybe these are things that are specific to programming and don’t really have anything to do with math?
Types obviously are mathematical, because algebraic structures in mathematics are useful for programming when they are turned into types. That’s where things like differentiating types come from, and monads, and Curry-Howard.
It’s much deeper than sum types.
If you want a term which differentiates “good sum types” from “bad sum types”, invent one.
There already is one ¯\_(ツ)_/¯
There already is one ¯\(ツ)/¯
That is it then? Why isn’t that term used instead of “sum types”?
If a language claims to have “sum types” that’s good; if it uses some other synonym that often means the design is broken in the ways Graydon discussed. If it claims to have “algebraic data types” that’s even better as I already explained. If it talks about coproducts then expect lots of abstract nonsense.
Okay. I claim that C has sum types.
I think you two are talking past each other.
fanf is being descriptive, and is describing what you can infer about a language from whether it says (in its documentation?) that it has “sum types” or “algebraic data types” or “coproducts” or “tagged unions”. Though I think the reality of how people use these words is a bit messier than fanf is suggesting: Rust calls its sum types enums and Zig calls its sum types tagged unions and I believe both are well implemented and not broken in the ways Graydon discussed.
mort, on the other hand, is being prescriptive, and discussing what the terminology should be rather than what it is. And correctly points out that “algebraic types” is a bad name.
And here’s your counterexample showing that C doesn’t have sums for every tuple of C types:
extern struct thing th;
union compiler_error { int tag; struct thing t; };
That’s a bad counter example. An incomplete type ‘struct thing’ and a complete type ‘struct thing’ aren’t different types, so your ‘struct thing’ isn’t an example of a type that can’t be part of a sum. Types just can’t be part of a sum before they’re defined.
C allows you to do certain things with types before they’re defined, but that’s really just a convenience thing. You can’t seriously be of the genuine opinion that the fact that C lets you express “pointer to T” before you define T fundamentally change the nature of its type system from an algebraic one to a non-algebraic one.
But it’s more than just tagged unions. That’s like saying “grammar” is an unnecessarily fancy term for the concept of nouns.
I agree ‘algebraic’ comes across as fancy. But if there’s a better word for, “the free combination of addition and multiplication,” I can’t think of it. 🤷♂️
When someone says “algebraic”, I do not think “the free combination of addition and multiplication”. I may think “manipulation of expressions built from a free combination of addition, multiplication, division, subtraction, powers, logarithms and trigonometric functions, involving unknown variables”.
I acknowledge that one particular use of the word “algebra” refers to a system where elements have some multiply operation and some addition operation and where these can be applied freely, and that types can be viewed as the element of one such algebra if you define a sum operation and a multiply operation for them, and that structs are a natural implementation of a product operation while tagged unions are a natural implementation of a sum operation. But that’s one very specific interpretation of the term “algebra”. It would be just as correct to interpret “algebra”, as it applies to types, to mean manipulation type expressions where some types are unknown to simplify complicated type expressions.
Besides, you don’t even mean “any system where there is a product type and a sum type”, because, assuming you agree with fanf’s comment, you want to exclude certain implementations of sum types. When you say “sum types” and “algebraic data types”, you want a programming language with specific safety guarantees preventing the user from accessing the wrong field of a union, typically a pattern matching syntax. We’re so, so far removed from the general idea of “algebra” here.
“Fancy” is overselling it. Algebra is taught in schools; if they were named appropriately from the get-go then the theory would feel a lot more approachable.
Algebra is taught in schools as “you have expressions with addition, subtraction, multiplication and division between numbers, but some numbers are unknown”. Eventually powers and logarithms and roots and trigonometric functions are introduced. At no point in my education was I taught the concept of “an algebra”, as in a set combined with addition and multiplication operations with specific properties. People who don’t study maths don’t typically have any idea what “algebraic” means in “algebraic data types”, even if they’re good at finding X or simplifying expressions.
People who don’t study maths don’t typically have any idea what “algebraic” means
That’s because they’re not taught it. Algebraic types is just “you know sum and product and variables from algebra? now imagine it’s more than just numbers”. It’s not even as complicated as the level it gets to in school. I’m not fighting you, I’m saying if “see how similar this is to elementary algebra?” was part of programming education then it wouldn’t be “fancy” and might even have been seen as a useful element to be put in popular languages decades sooner.
This exchange is a bit frustrating:
Everyone knows what an algebra is, it’s taught in schools
No, it’s not actually taught in schools, so people don’t actually know what it is
That’s just because people aren’t taught what an algebra is
But okay, I will engage with the new argument. I don’t really disagree. It is a bit messed up that people (such as myself) can go through an entire academic computer science education and not once learn about how combination of types can be viewed as an algebra.
I still don’t think that “algebraic data types is really what people want though, people want something with specific properties like safety and pattern matching. See: https://lobste.rs/c/bqkiq5
Everyone knows what an algebra is
Probably frustrating because that’s not what I said, so I’ll rephrase: the relationship between the algebra that everyone knows and tagged unions should be taught early and explicitly.
It’d be interesting to see where algebraic analogies could go. Could an expression with multiple roots be a safety issue due to ambiguity or something? I’ve not thought it through that much.
The correct name is algebraic data types. Algebra has lots of operations (e.g., kernels and cokernels, direct and inverse limits, etc.) that ought to be included in an “algebraic” type system, but are inexpressible with algebraic data types alone.