Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

When I think of sum types, I like the categorical definition the best, which is that a sum A+B has two morphisms (i.e. constructors) Inl : A -> A+B and Inr : B -> A+B, with a simple commuting diagram[0]. Or in Rust,

  enum Sum<A, B> {
     Inl(A),
     Inr(B),
  }
Why do I prefer this definition? Well, category theory abstracts away irrelevant details, and sums have a "universal property" associated with them. Roughly speaking that means that it doesn't matter how you define sum types in your language, if they fit the universal property of sums (up to isomorphism) then they truly can be considered sum types. In the Rust PlayerClass example the corresponding sum is (Solarian + (Polarian + Centaurian)), and morphisms

  Sol  = Inl . Inl
  Pol  = Inl . Inr
  Cent = Inr . Inr
[0] https://en.wikipedia.org/wiki/Coproduct


I don't know any category theory whatsoever. What happens in your example if A = B? Would it have two morphisms or just one?


What might be causing confusion is the difference between tagged unions and untagged unions.

A union type "A | B" means "a value of type A or a value of type B". Example:

    function f1(): String | Integer {
        if (rand()) {
            return "hello"
        } else {
            return 12
        }
    }

    function f2(x: String | Integer) {
        switch (typeof x) {
            case String: return "string: " + x
            case Integer: return "integer: " + x
        }
    }
The type "String | String" is exactly equivalent to "String".

A tagged union (aka sum type) "A + B" means "either a left value or a right value; if it's the left, it has type A, if it's the right it has type B".

    function g1(): String + Integer {
        if (rand()) {
            return Inl("hello")
        } else {
            return Inr("bye")
        }
    }

    function g2(x: String + String) {
        switch (x) {
            case Inl(s): return "left value: " + x
            case Inr(s): return "right value: " + x
        }
    }
The type "String + String" has one bit of additional information than just "String".


There'll still be two morphisms, Inl : A -> A + A and Inr : A -> A + A




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: