[HN Gopher] Programming with union, intersection, and negation t...
___________________________________________________________________
Programming with union, intersection, and negation types
Author : pbowyer
Score : 18 points
Date : 2022-07-07 20:14 UTC (2 hours ago)
(HTM) web link (arxiv.org)
(TXT) w3m dump (arxiv.org)
| galaxyLogic wrote:
| Isn't Union Types just the same as "Sum Types" (as in Haskell
| etc.)?
|
| But does Haskell have Intersection Types and Negation Types?
| dragonwriter wrote:
| > 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]
| spion wrote:
| 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 wrote:
| 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 wrote:
| Maybe<T> is a tagged union between T and None.
|
| Nullable<T> is an untagged union between T and None.
| choeger wrote:
| 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)
| Sharlin wrote:
| 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 _un_ tagged 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.
| quickthrower2 wrote:
| 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 wrote:
| 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
| spiralx wrote:
| 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 wrote:
| Is "nominal typing" the same as structural or duck typing?
___________________________________________________________________
(page generated 2022-07-07 23:01 UTC)