3 ms·
I agree. From the article: > The | operator indicates that this is a sum type [..] This doesn't explain what's going on; it references terminology used only b
by runeks 10y ago
I agree. From the article:
> The | operator indicates that this is a sum type [..]
This doesn't explain what's going on; it references terminology used only by people who already know what's going on.
A pedagogical explanation would say: the | operator means "or", in that you can use multiple different constructors (separated by |) to construct the type in question (whose name is to the left of the '=' operator). For example:
data Bool = True | False
means that you can construct a value of type Bool using one of the constructors True or False.
- danieldk 10y agoBut 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 10y 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?
- moomin 10y agoI think you're missing the point between a teaching article and an article about teaching. This is in the latter category.