Sum/union types

[GregorySech]

[Edit by eernstg: I removed 'type matching' from the title because Dart has pattern matching today.]

I'd like to import some features from functional languages like OCaML and F#.
The main feature I'm proposing is the possibility of using typedef to define sum types. They can be thought of as type enumerations.
This will, in some cases, reduce the need for dynamic making for sounder typing.
For example json.decode would no longer return dynamic but JSON a sum type, something like:

typedef JSON is Map<String, JSON> | List<JSON> | Literal;

Sum types could power a new behaviour of switch case that resolves the type based on the typed enumerated. Kind of like assert and if does with contemporary is syntax.

typedef T is A | B | C;
...
void foo(T arg) {
  switch(arg) {
    case A: // here arg is casted to A
      break;
    case B: // here arg is casted to B
      break;
    case C: // here arg is casted to C
      break;
  }
}

A better syntax for this type of switch case might be of order, maybe something like dart-lang/sdk#57173.

typedef T is A | B | C;
...
void foo(T arg) {
  switch(arg) {
    case A -> ... // here arg is A
    case B -> ... // here arg is B
    case C -> ... // here arg is C
  }
}

This would be a powered down version of OCaML and F# match <arg> with as I've not included a proposition for type deconstruction, which would probably require tuples (or more in general product types) as discussed in dart-archive/linter#68.

[eernstg]

First note that it should be possible to categorize this issue as a request or a feature. The request would articulate a non-trivial and practically relevant shortcoming in terms of software engineering that would justify considerations about adding new features to Dart. A feature description is a response to a request, that is, every feature under consideration should be grounded in a need for the feature in terms of an underlying software engineering problem, it should never just be "I want feature X just because that's a cool concept to have in a language". It may well be a non-trivial exercise to come up with such a request, and it may not necessarily have just one feature as its "corresponding solution", but that's a good thing, not a bug. ;-)

This issue is clearly a feature issue, specifically promoting a language construct (or a family of closely related ones). So we need a request issue which describes a software engineering problem more broadly, such that some notion of sum types would be an appropriate response to that request.

That said, requests for sum types are of course not a new thing. A couple of pointers: https://github.com/dart-lang/sdk/issues/4938 has been the main location for discussing union types, and the feature discussed in this issue may or may not be covered under that umbrella.

In particular, this proposal may or may not assume tags. If tags are assumed, typedef JSON would be similar to a class hierarchy like this:

class Json {}
class JsonMap implements Json {
  Map<String, Json> value;
}
class JsonList implements Json {
  List<Json> value;
}
class JsonLiteral implements Json {
  ... // Whatever is needed to be such a literal.
}

This would provide run-time support for discriminating all cases, because anything of type "Map<String, JSON>" would actually be wrapped in an object of type JsonMap, and a simple is JsonMap test would reveal whether we're looking at such an object. In a functional language you'd declare all cases in a single construct, and it would thus be easy to detect at compile time whether any given deconstruction is exhaustive. With an OO class hierarchy you'd need a concept like a 'sealed' class hierarchy in order to get a similar statically known exhaustiveness guarantee. (OCaml supports extensible variant types, and they require an explicit 'default' case in every pattern match, so we got the same trade-off there, albeit with the sealed design as the default.) In any case, tagged unions is the easy way to do this, and it may be somewhat costly at run time, because we have to create and navigate a lot of "wrapper" objects.

However, if we assume untagged unions then we cannot expect run-time support for O(1) discrimination. For instance, a recursive untagged union type could be defined like this (assuming that Dart is extended to support recursive union types):

typedef NestedIntList = int | List<NestedIntList>;

If we're simply considering the type NestedIntList to be the (infinite) union of int and List<int> and List<List<int>> and so on, then it would be possible for a variable of type NestedIntList to refer to an instance of int, and it could also refer to an instance of List<int>, etc. There would not be any wrapper objects, and we would have no support to tell in time O(1) that any given object (say, a List<int>) is in fact of type NestedIntList. This means that the expression e is NestedIntList would need to perform an unbounded number of type checks, and it would in principle be unable to stop at any finite level (if it's looking at a List<List<.....<String>.....>> it wouldn't be able to say "no" before it hits the String, which could be nested any number of levels.)

So we need to clarify whether sum types are intended to be similar to SML algebraic data types (that is, tagged unions), or similar to TypeScript union types (untagged unions).

We should note that TypeScript does not support dynamic type tests (and I do not believe the user-defined workaround is a relevant replacement in Dart). Dart will remain sound in the sense that the obvious heap invariant ("a variable of type T refers to an entity of type T") is maintained at all times, based on a combination of static and dynamic checks. So we don't have the option to ignore that certain type tests / type checks are expensive.

[GregorySech]

Sorry for the missing tag, it seems I'm unable to edit them, I'll propose them in the title while I'm looking for documentation on how to do it.

Thank you for the extensive explanation, I didn't dive deep enough into the sdk issues and I apologize.

To answer the specification question: I was not aware of union types in TypeScript as I've not used it yet so I intended them to be as similar as possible to SML data types however I was ignoring the implementation details of such feature.
I'll start studying the mentioned concept in the next days.

[eernstg]

@GregorySech, first: Thanks for your input! I should have said that. Second: I guess there's some permission management in place which restricts the labeling; I'm sure those labels will be adjusted as needed, so don't worry. So the main point is simply that it would be really useful in the discussion about a topic like this to have a characterization of the underlying software engineering problem (without any reference to any particular language construct that might solve the problem), and it would be helpful if you could capture that underlying software engineering challenge for which such a feature as 'sum types' would be a relevant solution.

[yjbanov]

@eernstg

if we assume untagged unions ... There would not be any wrapper objects

Would this still be true if Dart adds unboxed types in the future? For example, imagine in the future non-nullable int is directly represented by 64-bit integer and its value is inlined into variables and fields. Now, what happens when you define a variable of type int | String?

[mdebbar]

FutureOr<T> is a real use case that is hardcoded in Dart today and would be solved neatly when Dart introduces union types. I agree they don't have to match all the specifics of other languages.

[eernstg]

.. [no] wrapper objects
Would this still be true if Dart adds unboxed types[?]

If Dart is extended to support a notion of unboxed types I would expect such instances to be compatible enough with the rest of Dart to allow a reference of type Object to refer to them, and that would require support for some notion of boxing.

You may or may not want to say that a boxed entity of type T is a wrapper object containing an unboxed entity of type T, but we're still talking about the same type (with different representations at run-time).

With a wrapper which is used as the representation of a tagged union type there is a transition from one type to another type when the wrapper is added. An example in SML would be the following:

datatype IntString = INT of int | STRING of string;
fun f (INT i) = "An integer"
  | f (STRING s) = s;
val v1 = f (INT 42);
val v2 = f (STRING "24");

Here, INT 42 is of type IntString, but a plain 42 is of type int, so there's a difference between "just being an int" and "being an int which is one of the cases in the union of int and string", and that difference amounts to an entire wrapper object. It's a compile-time error to call f with an argument of type int or string, they must be wrapped first, hence f (INT 42). You need to create that wrapper object explicitly (OK, we could try to infer that, but that's another tarpit ;-), and in return you can test for it at run time (so f knows which case to run when you call it). An extension of Dart with tagged unions would presumably have a lot of the same properties.

An extension of Dart with untagged unions would be different in many ways. I just wanted to point out the fact that this distinction matters, so we shouldn't discuss union types (or sum types) without knowing which kind we're talking about. ;-)

[eernstg]

FutureOr<T> is a real use case that is hardcoded in Dart today

Right. We knew from day one that FutureOr could be used as a playground for getting to know exactly how that special case of union types would affect the whole language.

[yjbanov]

@eernstg Thanks for the explanation! I misread your "wrapper object" as boxing. Yes, something like tagged unions does not require boxing. For example, Rust's and Swift's enum types are essentially tagged unions, and they do not box them.

[eernstg]

@yjbanov wrote:

For example, Rust's and Swift's enum types are essentially tagged unions,
and they do not box them.

Right, but I think the situation in Rust and Swift is slightly different from the situation in Dart.

In general, a range of memory cells does not have to be a full-fledged heap entity in order to be able to contain a primitive value (like an integer or a pointer to an immutable string (Rust: &str)) as well as a reference to an associated value (Swift) or a tuple or struct with no subtype relations (Rust) such that the size of the whole thing is known statically as soon as we know which "case" of the enum type we are working on, and we can compute how much space is needed in order to be able to store any of the declared cases.

But at this point we do not have general support for non-heap entities in Dart of any other size than that of a primitive, so if we want to support that kind of composite entity in Dart I think we will have to keep them in the heap (that is, we need to box them). That could still be useful, however, because an enum with an associated value is similar to a tagged union where the enum value itself is the tag.

The ability to work on unboxed entities of arbitrary size would be an orthogonal feature in Dart, and we would be able to introduce support for this separately (and sort out how they would work in dynamic code), and then we could use it for entities of any kind, including enum-with-associated-value.

[stt106]

If this is implemented + non-nullable types, then Dart will be the best language ever!
Sum types (and records) are incredibly powerful constructs to model domains.

[GregorySech]

Let's say that Dart had a non-nullable type ancestor called Thing, Object might be Thing | Null. I'm still unaware of implementation implications for this features to work together but the message I'm trying to convey is that this might save a lot of refactoring if non-null is implemented.

[burakemir]

Hey Erik, since you asked for "software engineering arguments" further up, I will bite and state why algebraic data types and pattern matching is useful from a software engineering perspective.

The simple truth is:
1 - representing structured data so that it can be inspected from the outside isn't what objects were made for, and
2 - yet most data in real world applications has to deal with structured data (it started with tuples, records, relations and the "OO-SQL impedance mismatch").

Today, NULL/optional, enums etc can all provide only half-hearted solutions to case distinction. The paper "Matching Objects with Patterns" (Emir, Odersky, Williams) and also my thesis "Object-oriented pattern matching" discusses the benefits and drawbacks of the object-oriented and other encodings of algebraic data types. The "type-case" feature is also discussed, but not a notion of untagged sum type.

I'd be an advocate for the tried and tested algebraic data types which is a way to represent tuples, sum types, "value classes" and a whole bunch of other programming situations that all help with modeling and dealing with structured data. Algebraic data types would reflect the symmetry between product types and sum (=co-product) types, as known from category theory and its manifestations in functional programming in Haskell, Scala, ocaml aka Reason etc. What better software engineering argument than "it works" can there be? : ) Let me know if this is the appropriate issue or I should file a new one.

(updated, typo)