3 ms·
But the constructor approach does not explain what makes a sum type a sum. If the readers already have some background in a programming language, you could als
by danieldk 9y ago
But the constructor approach does not explain what makes a sum type a sum.
If the readers already have some background in a programming language, you could also start with e.g. a struct from an imperative language:
struct Foo {
X x;
Y y;
}
This is a so-called product type, because the number of possible values of Foo is the number of values of type X times the number of values of type Y. So if X = {Red, Green, Blue} and Y = {Light, Dark}, then this product type has 3 x 2 = 6 different values:
Foo {Red, Light}
Foo {Green, Light}
Foo {Blue, Light}
Foo {Red, Dark}
Foo {Green, Dark}
Foo {Blue, Dark}
What if instead, we wanted to have the sum of the possible values of X and Y? In other words, where we'd have to choose between a value from X or from Y?
Foo {Red}
Foo {Green}
Foo {Blue}
Foo {Light}
Foo {Dark}
That's a sum type: it is a type where you can pick a value from X or Y, giving a total of 3 + 2 = 5 possible values.
Then give a motivating example where one would need such a type (e.g. trees nodes) and introduce proper notation.
- hcs 9y agoI agree with your approach, one suggestion: If you're using struct to introduce product, does it make sense to use union to explain sum? Although maybe that's too complicated given the need to tag it?