Sum Types in Julia and Rust

Post by millstone » Mon, Aug 31, 2020, 5:31 AM UTC

siraben wrote: post #8

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 { 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 mean…

Post by siraben » Mon, Aug 31, 2020, 5:49 AM UTC

millstone wrote: post #11

siraben wrote: post #8

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 { 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 mean…

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

Post by cakoose » Mon, Aug 31, 2020, 6:25 AM UTC

millstone wrote: post #11

siraben wrote: post #8

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 { 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 mean…

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

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

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

Post by bocckoka » Mon, Aug 31, 2020, 7:12 AM UTC

chalst wrote: post #16

Two thoughts: For this problem, I would use union types in Julia. Union types are a sort of sum, but they are amalgamated sums whilst sums types in PL semantics usually means disjoint sums. The difference is that disjoint sums 'mark' whether a value is of the left or right type, while with amalgamated sums the value may belong unmarked to the intersection. The distinction does not matter in the example the post gives…

Post by curryhoward » Mon, Aug 31, 2020, 7:36 AM UTC

enricozb wrote: post #6

amitport wrote: post #3

I may be wrong, but I don't think this is what people mean by 'sum types'. I was expecting union types (e.g., https://www.typescriptlang.org/docs/handbook/unions-and-inte... or https://dotty.epfl.ch/docs/reference/new-types/union-types.h... ) I guess enums are a type of sum type, but seems this is more specifically about enums

I believe another word for enums (in the Rust sense, not in the C++ or Java sense) are tagged unions.