7 ms·

Programming with union, intersection, and negation types

35 points by pbowyer 4y ago

galaxyLogic 4y ago
Isn't Union Types just the same as "Sum Types" (as in Haskell etc.)? But does Haskell have Intersection Types and Negation Types?
- dragonwriter 4y ago
  > Isn't Union Types just the same as "Sum Types" (as in Haskell etc.)? No, Union Types are untagged, Sum types are tagged. One consequence is that Sum types can be nested in a way that doesn't work for Union Types. E.g., with a Sum type like Maybe a = Some a | None, you can have a Maybe (Maybe a) which expands to None | Some (None) | Some (Some a) Whereas with a union like Maybe a = None | a; Maybe (Maybe a) would be identical to Maybe a.
  - deleted 4y ago
    [deleted]
- spion 4y ago
  Sums are tagged unions, whereas unions are more general. Given the types T1 and T2, the union type `U = T1 | T2` includes all values of type T1 and values of type T2. A tagged union on the other hand is a new type which does not accept values of neither T1 nor T2 without tagging them with their appropriate tag.
  - galaxyLogic 4y ago
    So, as you say unions are more general, and thus might be easier to work with? Would there be any benefit for Tagged Unions over "non-tagged" Unions?
    - Spivak 4y ago
      Maybe<T> is a tagged union between T and None. Nullable<T> is an untagged union between T and None.
    - choeger 4y ago
      There are many benefits of sum types: - Their values can be discriminated at runtime (it's depending on the implementation of union types whether that's possible. In C a union is just a structure large enough to hold all constituents) - You can sum the same type (union(Int, Int) simply is Int) - The tag breaks recursion. You can build recursive sum types because of it, e.g. 'a List = Empty | Cons('a, 'a List)
      - earleybird 4y ago
        > You can sum the same type (union(Int, Int) simply is Int) I'm not sure this is the case. In some cases Union(Int, Int) might be interpreted as a union of Left-Int or Right-Int Then again, my understanding of sum vs union might not be overly precise :-) edit: s/now/not/
    - Sharlin 4y ago
      You need some sort of a tag if you want to pattern match at runtime, which is the usual use case for tagged unions. Now, a tagged union like type Option a = Some a | None # here Some and None are tags, not types themselves could also be written as an untagged union by using types as tags: type Some a # a wrapper type for an a type None # a unit type type Option a = Some a | None but for that to be useful you still need to be able to check at runtime whether you have a Some or a None… which means that the tags are still there, just hidden by the language. But the more typical use case for untagged unions is different: given a type such as type StringOrInt = String | Int you're not even supposed to be able to check whether you in fact have a String or an Int, rather the language only allows you to use the subset of operations defined for both String and Int. In other words, slightly ironically, the type StringOrInt exposes the intersection of String API and Int API.
      - 4y ago
quickthrower2 4y ago
Not sure about negation, but humble Typescript lets you use union and intersection types. I am hooked on intersection types in Typescript. It is like mixin heaven. I have a WithId type I use alot that I can tack on to any Firebase record type. If I had the motivation I could write a generic firebase getter that returns documents as a “T & WithId” (means type T with an additional id:string field) It decreases the number of types you need to define for one. And lets you lego up various interfaces.
- ksbrooksjr 4y ago
  Yeah Typescript is great. It doesn't have a negation type per se, but its pretty easy to derive one using the never type [1]. The author of this essay actually explicitly calls out Typescript several times. Some quotes from the paper's conclusion: > In this essay I tried to survey the multiple advantages and usages of set-theoretic types in programming. > ...the need of set-theoretic types naturally arises when trying to fit type-systems on dynamic languages > The development of languages such as Flow, TypeScript, and Typed Racket is the latest witness of this fact. [1] https://catchts.com/type-negation https://catchts.com/type-negation
- spiralx 4y ago
  I called it HasId, there's a withId RxJS operator to go with it that selects from an IdRecord<T> based on an inner observable that emits an ID string. Due to nominal typing in TS you don't need to explicitly implement HasId anywhere either, meaning you don't end up with it cluttering up every single type with an ID field (plus imports).
  - ttymck 4y ago
    Is "nominal typing" the same as structural or duck typing?
    - jcparkyn 4y ago
      No, they presumably meant to write "structural" because nominal is the opposite.

35 points by pbowyer 4y ago

Isn't Union Types just the same as "Sum Types" (as in Haskell etc.)? But does Haskell have Intersection Types and Negation Types?

dragonwriter 4y ago
> Isn't Union Types just the same as "Sum Types" (as in Haskell etc.)? No, Union Types are untagged, Sum types are tagged. One consequence is that Sum types can be nested in a way that doesn't work for Union Types. E.g., with a Sum type like Maybe a = Some a | None, you can have a Maybe (Maybe a) which expands to None | Some (None) | Some (Some a) Whereas with a union like Maybe a = None | a; Maybe (Maybe a) would be identical to Maybe a.
- deleted 4y ago
  [deleted]
spion 4y ago
Sums are tagged unions, whereas unions are more general. Given the types T1 and T2, the union type `U = T1 | T2` includes all values of type T1 and values of type T2. A tagged union on the other hand is a new type which does not accept values of neither T1 nor T2 without tagging them with their appropriate tag.
- galaxyLogic 4y ago
  So, as you say unions are more general, and thus might be easier to work with? Would there be any benefit for Tagged Unions over "non-tagged" Unions?
  - Spivak 4y ago
    Maybe<T> is a tagged union between T and None. Nullable<T> is an untagged union between T and None.
  - choeger 4y ago
    There are many benefits of sum types: - Their values can be discriminated at runtime (it's depending on the implementation of union types whether that's possible. In C a union is just a structure large enough to hold all constituents) - You can sum the same type (union(Int, Int) simply is Int) - The tag breaks recursion. You can build recursive sum types because of it, e.g. 'a List = Empty | Cons('a, 'a List)
    - earleybird 4y ago
      > You can sum the same type (union(Int, Int) simply is Int) I'm not sure this is the case. In some cases Union(Int, Int) might be interpreted as a union of Left-Int or Right-Int Then again, my understanding of sum vs union might not be overly precise :-) edit: s/now/not/
  - Sharlin 4y ago
    You need some sort of a tag if you want to pattern match at runtime, which is the usual use case for tagged unions. Now, a tagged union like type Option a = Some a | None # here Some and None are tags, not types themselves could also be written as an untagged union by using types as tags: type Some a # a wrapper type for an a type None # a unit type type Option a = Some a | None but for that to be useful you still need to be able to check at runtime whether you have a Some or a None… which means that the tags are still there, just hidden by the language. But the more typical use case for untagged unions is different: given a type such as type StringOrInt = String | Int you're not even supposed to be able to check whether you in fact have a String or an Int, rather the language only allows you to use the subset of operations defined for both String and Int. In other words, slightly ironically, the type StringOrInt exposes the intersection of String API and Int API.
    - 4y ago

quickthrower2 4y ago

Not sure about negation, but humble Typescript lets you use union and intersection types. I am hooked on intersection types in Typescript. It is like mixin heaven. I have a WithId type I use alot that I can tack on to any Firebase record type. If I had the motivation I could write a generic firebase getter that returns documents as a “T & WithId” (means type T with an additional id:string field) It decreases the number of types you need to define for one. And lets you lego up various interfaces.

ksbrooksjr 4y ago
Yeah Typescript is great. It doesn't have a negation type per se, but its pretty easy to derive one using the never type [1]. The author of this essay actually explicitly calls out Typescript several times. Some quotes from the paper's conclusion: > In this essay I tried to survey the multiple advantages and usages of set-theoretic types in programming. > ...the need of set-theoretic types naturally arises when trying to fit type-systems on dynamic languages > The development of languages such as Flow, TypeScript, and Typed Racket is the latest witness of this fact. [1] https://catchts.com/type-negation https://catchts.com/type-negation
spiralx 4y ago
I called it HasId, there's a withId RxJS operator to go with it that selects from an IdRecord<T> based on an inner observable that emits an ID string. Due to nominal typing in TS you don't need to explicitly implement HasId anywhere either, meaning you don't end up with it cluttering up every single type with an ID field (plus imports).
- ttymck 4y ago
  Is "nominal typing" the same as structural or duck typing?
  - jcparkyn 4y ago
    No, they presumably meant to write "structural" because nominal is the opposite.