Hacker News Reader

Hacker News

Comment by dbaupp | Hacker News Reader

Parent Full thread

dbaupp

Swift enums are sum types.

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.

View on HN

in case it's useful for anyone who has ever dealt with tagged pointers,

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

C++: union or boost::variant or (C++11) std::variant

And Scala (via Dotty) is being re-worked to have sum types with a cleaner "enum" syntax soon too: https://github.com/lampepfl/dotty/issues/1970 (merged)

why would you want to view a programming language algebraically?

It lets you reuse your existing knowledge about algebra to transform programs. For example if you have a data type that has two different cases (= sum) each of which has a bunch of fields (= factors in a product) some of which are shared (= common factors in a sum of products) then you can literally factor them out, just like you can factor A * B * C + A * D * C into A * (B + D) * C.

Conjunction and disjunction are more apt anologies that have the same properties. There is also no division types while subtraction is used very rarely.

I didn't think to call it that at the time, but I think that I came across a division type in react-redux the other day: https://github.com/DefinitelyTyped/DefinitelyTyped/blob/8f8f...

Playing with that a little, if adding a property to an interface is a product, eg:

    interface Foo {
        foo: string;
        bar: number;
    }

where Foo is a product of string and number, then removing a property from an interface is division:

    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>;

the output type Out is equivalent to:

    interface Out {
        foo: string;
    }

or phrasing it another way:

    Out = Foo / Bar = (string * number) / number = string

I can't think what a 1/number type would be used for other than to remove number from a a T*number, in other words I can't think what a rational type would be used for unless it simplified down to a "normal" type. But I wouldn't like to bet that there's no other use :-)

What is the set theory intuition of that? If product is intersection, division is...?

Product is not intersection. The equivalent to product types in set theory is the Cartesian product ( https://en.wikipedia.org/wiki/Cartesian_product ).

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.

That isn’t how product (intersection) types work in typescript. If we are talking about typescript, of course.

Product and intersection are different things in TypeScript, as well. The product of string and number would be a type like { first: string; second: number }, which combines two different values into one; whereas the intersection string & number is the type of all values that are both strings and numbers.

Right, but if we are going to call union types as sum types, why aren’t interesection types called as product types? Anyways, this is why the whole sum type thing breaks down and Union is more apt, since we can describe A|B and A&B using the same terminology family.

A | B and A + B are only "the same" (but not identical) if A and B are disjoint (i.e. there is no value that is in both types). That's why + is also called disjoint union. You can simulate + with | by introducing artificial tags to make A and B disjoint, but in the end they are different operations. TypeScript doesn't really have first-class support for sum types because it needs to remain interoperable with JavaScript, so this simulation is the closest you are going to get.

I agree, so it really isn’t an example of the popularity of sum typing. Typescript does have support for user-supplied tagging, so you can also approximate it to some extent.

Yea, support isn't first class. When I was learning to use union types in TypeScript, initially I wrote custom type guards to distinguish them, using any property that was unique to a particular constituent type to differentiate them.

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 are more apt anologies that have the same properties.

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.

This is what leads to things like monads appearing as programming constructs; they provide neat abstractions which allow you to reason about code at a higher level than you otherwise could.

https://chris-taylor.github.io/blog/2013/02/10/the-algebra-o...

This would be more useful and more upvoteable if you had provided some text for context.

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

A lot of academic programming language research is an outgrowth of mathematics, so it uses the language of mathematics.

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

https://en.wikipedia.org/wiki/Lambda_calculus

Reply on news.ycombinator.com