7 ms·

What is the difference between these 'sum types' and Swifts enum type? Also I think the name 'sum type' is bad. Nothing gets added or summed up, just combined

• silluk 9y ago
  A sum type is the more general name for a Swift/Rust enum.
• matt_kantor 9y ago
  The numbers of values in the types are what get summed up. The sum type `Boolean | Byte` has 2 + 256 unique values while the product type `(Boolean, Byte)` has 2 * 256 unique values
• dbaupp 9y ago
  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.
  • gavinlynch 9y ago
    why would you want to view a programming language algebraically?
    • yorwba 9y ago
      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.
      • seanmcdirmid 9y ago
        Conjunction and disjunction are more apt anologies that have the same properties. There is also no division types while subtraction is used very rarely.
        • DougBTX 9y ago
          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/8f8f6c439296ade0ab205751a72dfd626dd73364/types/react-redux/index.d.ts#L50 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 :-)
          • deleted 9y ago
            [deleted]
          • 9y ago
    • Smaug123 9y ago
      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.
    • wz1000 9y ago
      https://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/ https://chris-taylor.github.io/blog/2013/02/10/the-algebra-o...
      • tom_mellior 9y ago
        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) 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-calculus-of-algebraic-data-types/ https://codewords.recurse.com/issues/three/algebra-and-calcu...
    • SideburnsOfDoom 9y ago
      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 https://en.wikipedia.org/wiki/Boolean_algebra#History and "lambda" to Alonzo Church in the 1930s https://en.wikipedia.org/wiki/Lambda_calculus https://en.wikipedia.org/wiki/Lambda_calculus
  • jfoutz 9y ago
    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.
    • humanrebar 9y ago
      C++: union or boost::variant or (C++11) std::variant
  • sixbrx 9y ago
    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 https://github.com/lampepfl/dotty/issues/1970 (merged)
• reycharles 9y ago
  > Also I think the name 'sum type' is bad. 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|.
• meuk 9y ago
  The name has its origin in type theory (you also have product types). It's not the best name I guess, but not the worst either: If we have type A with n terms and type B with m terms, then the sum type of A and B has n + m terms. 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).
• Smaug123 9y ago
  "Sum" is a word used throughout maths for "coproduct". They could have used "coproduct type", but then people might have started complaining that they were being exposed to category theory ;)
• masklinn 9y ago
  > Also I think the name 'sum type' is bad. Nothing gets added or summed up 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.
• unhammer 9y ago
  https://www.youtube.com/watch?v=ojZbFIQSdl8&feature=youtu.be&t=3m40s https://www.youtube.com/watch?v=ojZbFIQSdl8&feature=youtu.be... is a nice explanation for curly-brace programmers of why it's called a sum type (vs structs, which are product types)
• kazagistar 9y ago
  Sum type comes from the fact that the resulting type has as many possible values as the types it is combining, summed. This is in contrast to product types like tuples and structs. Either<u8, bool> This has exactly 256 + 2 possible values. Tuple<u8, bool> This has exactly 256 * 2 possible values. 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.
• doug1001 9y ago
  the category theory term is co-product (which honors the convention of expressing a dual using "co-" and indeed co-product is the dual of product)