Also I think the name 'sum type' is bad. Nothing gets added or summed up, just combined and selectively chosen. For this reason I find supercharging 'enum', like Swift does, a more logical solution.
Various languages use different keywords to access the same concept:
- Rust: 'enum'
- Swift: 'enum'
- Haskell: 'data'
- F#: 'type'
- Ocaml: 'type'
> Also I think the name 'sum type' is bad. Nothing gets added or summed up, just combined and selectively chosen. For this reason I find supercharging 'enum', like Swift does, a more logical solution.
They're the same solution...
In any case, the name sum comes from viewing types "algebraically" as the article discusses. Doing addition of types with a sum type has a lot of similar properties to doing addition of numbers, and similarly doing multiplication of types with a product type (tuple, struct or class, in Swift) has a lot of similar properties to doing multiplication of numbers.
Playing with that a little, if adding a property to an interface is a product, eg:
interface Foo {
foo: string;
bar: number;
}
type Diff<T extends string, U extends string> = ({ [P in T]: P } & { [P in U]: never } & { [x: string]: never })[T];
type Omit<T, K extends keyof T> = Pick<T, Diff<keyof T, K>>;
interface Foo {
foo: string;
bar: number;
}
interface Bar {
bar: number;
}
type Out = Omit<Foo, keyof Bar>;
interface Out {
foo: string;
}
Out = Foo / Bar = (string * number) / number = string
The closest thing to a division would be a quotient set ( https://en.wikipedia.org/wiki/Quotient_set ), but there you're dividing by an equivalence relation. It is however possible to define an equivalence that undoes set multiplication: (A × B)/~ ≅ A if (a₁, b₁) ~ (a₂, b₂) holds iff a₁ = a₂, ignoring the other component.
Nowadays I consider that a mistake, and all unions have a discriminator property, and there is no need for custom type guards (exceptions would be when writing .d.ts files for JS that uses them untagged, that sort of thing) since it makes the code much more explicit.
Conjunction and disjunction also have other properties, like idempotence: A /\ A = A, which by analogy would suggest that a tuple of two integers is the same as a single integer. Similarly, A \/ A = A, which is exactly the problem mentioned by the featured article that is the difference between union types and proper sum types (aka tagged union types).
So while sum and product may not be great analogies, conjunction and disjunction seem worse.
TLDR: If you interpret sum types as + and product types (tuples/structs/objects) as *, type definitions can be read as polynomials. Recursive type definitions, like for linked lists, can be read as recurrence equations. If you do some calculus over these things and compute the derivative of these type formulas, you get back something meaningful: The formula corresponding to the type's Zipper (https://en.wikipedia.org/wiki/Zipper_(data_structure)), a data structure for efficiently traversing and modifying functional data structures.
I like Chris Taylor's series of posts on this topic, as well as this shorter one: https://codewords.recurse.com/issues/three/algebra-and-calcu...
E.G "boolean" dates back to George Boole, The Mathematical Analysis of Logic (1847)
https://en.wikipedia.org/wiki/Boolean_algebra#History
and "lambda" to Alonzo Church in the 1930s
- C: 'union'
If you've ever dealt with an AST, a sum type is really a wonderful way to represent the nodes. In C you probably want some sort of 'tag' to indicate the actual type of the union. Other languages handle that bookeeping for you.
for java i'm tempted to say 'interface' but that doesn't quite have the flavor of what you're driving at. definitely in the same spirit though.
If you view types as sets of values, then a sum type is the addition (union) of two sets, while a product type is the product (combination) of two sets.
> For this reason I find supercharging 'enum', like Swift does, a more logical solution.
Both are logical, they just come from different trains of thought.
Extending "enum" comes from "developers" viewing sum types as extensions of C-style enums, sum types comes from computer science and set theory.
Either<u8, bool>
Tuple<u8, bool>
Of course, this simple numerical interpretation breaks down as soon as you have something like a linked list which has infinite possible values, but even then, you can fuzz the rules a bit and get useful information out of the math. But that is the core intuition.
There are much more confusing things in type theory, like the ambiguity that the word 'type' has (I still don't grok the terminology, to be honest).
The intuition is that for each types A and B with number of elemnts |A| and |B| the sum type A+B has number of elements |A|+|B|.
(which honors the convention of expressing a dual using "co-" and indeed co-product is the dual of product)