Proposed changes to terms and syntax regarding types

[cpurdy]

The Ecstasy type algebra defines three operators:

• | for "intersection type"
• + for "union type"
• - for "difference type"

But internally, there are actually five composite type concepts that result from these three operators:

• T1 | T2 usually means "either a T1 or a T2", but it can also mean "the traits shared by both the T1 and T2 types" (the "intersection" in set theory)
• T1 + T2 means "both a T1 and a T2", which is (for all practical purposes) the same as "the union of the traits in T1 with the traits in T2"
• T1 - T2 usually means "a T1 and not a T2", but it can also mean "the remaining traits after the set of traits in T2 are subtracted from from the set of traits in T1" (the "relative complement" or "set-theoretic difference" in set theory)

In addition to the above, we had reserved an operator for the explicit "and-not" use case, and we planned to introduce a syntax for specifying difference types without a nominal type for the subtrahend.

Gene and I have a proposed set of changes that addresses all of the above:

• We will rename the "intersection type" to the "either type". The | type operator will define an either type.
• There will still exist an intersection type which is implied by the presence of an either type. For example, with some object o whose compile time type is known to be T1|T2, the compile-time available traits of o are defined by the intersection of the set of traits from T1 and the set of traits from T2.
• The union type will continue to be known as the union type. (We are choosing to not rename it to the "both type".)
• We will rename the typical use case of the existing "difference type" to be the "and not" type. For example, Int32-Unchecked specifies an Int32 and not @Unchecked.
• We expect that the algebraic difference type (the set-wise relative complement) will be used within the delegates clause and the into clause. We decided to retain the "difference type" meaning when the - operator is used to define a delegation type.
• The syntax for an anonymous pure type is "{" traitspecifiers "}", where traitspecifiers is a semicolon delimited/terminated list of traitspecifier, each of which is either a method/property name or a method/property signature. This syntax is permitted in specific constructs:
  • within a typedef statement
  • within a delegates clause
  • within an into clause
  • for the type specified within an .is() or .as() expression
  • within an extended type expression, as the addend of a union type expression or the subtrahend of a difference type expression
• When an anonymous pure type is used as a subtrahend, the result is a difference type, and not an and not type.

This syntax is expected to be fairly uncommon. It will be primarily useful for defining delegation sub-sets. While rare, it is an important capability, and we believe that this syntax allows us to "square up" a missing corner of the type algebra, without polluting the general purpose type forms.

Additionally, the terminology changes should help avoid some confusion, particular for anyone with existing knowledge of type theory applied in languages using the terms difference type and/or intersection type. Ecstasy's conceptual types are based on set theory, and the use of the set theory terms we previously selected was based on actul set operations. Nonetheless, we expect that there may be some initial confusion for new developers about our use of the term union type, primarily because of the type-unsafe manner in which the term is abused in other languages (C/C++ for example). Specifically, our union type is actually a type formed from the union of two types. What some languages refer to as a tagged union (confusingly referred to as a sum type by at least one existing language) or a discriminated union, is actually equivalent to an Ecstasy either type, which as discussed above, further implies an intersection type.

Regardless, we gave up on using some terms because the confusion created wasn't worth it. For one example of the confusion, look no further than Wikipedia itself (emphasis added):

Union types are types describing values that belong to either of two types. For example, in C, the signed char has a -128 to 127 range, and the unsigned char has a 0 to 255 range, so the union of these two types would have an overall "virtual" range of -128 to 255 that may be used partially depending on which union member is accessed. Any function handling this union type would have to deal with integers in this complete range. More generally, the only valid operations on a union type are operations that are valid on both types being unioned. C's "union" concept is similar to union types, but is not typesafe, as it permits operations that are valid on either type, rather than both.

[cpurdy]

From a reddit thread (you may need to expand comments):

• "[Ecstasy] literally uses "union" and "intersection" in the exact opposite of the standard usage." (u/o11c)
• "When you refer to the "intersection of T1 and T2" (as in T1 | T2) you mean the intersection of the (collections of) traits of T1 and T2: values of this type have both the traits of T1 and the traits of T2. However, while this is an intersection of traits it is not an intersection of types. From the description in the link, a value has type T1 | T2 if it has type T1 or if it has type T2. This is a union of the two types. In T1 | T2, traits are being "and-ed" and while the types are being "or-ed". Therefore, it's an intersection of traits but it's also a union of types. This makes it a bit confusing, IMO, to call it an "intersection type" since it is, in a literal sense, a union of types. Likewise for T1 + T2 being called a "union type"." (u/Roboguy2)
• "I'm assuming that T1 | T2 is an untagged union of types (corresponding to a set theoretical union of types, rather than a set theoretical disjoint union of types). [..] I personally like "union type." For example, skimming some papers, it looks like this is a pretty common naming convention [..] I might be biased from my Haskell background, but to me "either type" suggests a disjoint union. Admittedly, the word "either" doesn't inherently mean that in English. I also would suggest that T1+T2 should be an "intersection type" (which, I believe, is also the naming convention used in some of those papers)." (u/Roboguy2)
• "How something is “tagged” is an implementation detail, yeah. But whether it’s tagged is really fundamental. A sum type is non-idempotent (T + T ≠ T) so it must store a record of the choice of which T it holds. Whereas an untagged union type is idempotent (T ∨ T = T), so there’s no need to record anything." (u/evincarofautumn)

Conclusions:

• Rename "intersection type" to "union type"
• Rename "union type" to "intersection type"
• Be careful to not refer to Ecstasy "union type" as a tagged or disjoint union

Edit: (18 July 2022) - renaming changes committed

[cpurdy]

Trying this again, from the top:

The Ecstasy type algebra defines three operators:

• | for "union type"
• + for "intersection type"
• - for "difference type"

But internally, there are actually five composite type concepts that result from these three operators:

• T1 | T2 is a union type, and means "either a T1 or a T2", but it also implies "the traits shared by both the T1 and T2 types" (representing the "intersection" of traits in set theory)
• T1 + T2 is an intersection type, and means "both a T1 and a T2" (representing "the union of the traits in T1 with the traits in T2" in set theory)
• T1 - T2 usually indicates "a T1 and not a T2", but in some contexts it instead indicates "the remaining traits after the set of traits in T2 are subtracted from from the set of traits in T1" (the "relative complement" or "set-theoretic difference" in set theory)

Resulting state:

• There will still exist a type which is implied by the presence of a union type. For example, with some object o whose compile time type is known to be T1|T2, the compile-time available traits of o are defined by the intersection of the set of traits from T1 and the set of traits from T2. This corresponds to the '&' operator on Type; however, this type does not have an explicit type notation in the Ecstasy type algebra (i.e. you cannot currently declare a variable of this explicit type).
• We refer to the typical use case for the type - operator as the "and not" type; for example, Int32-Unchecked specifies an Int32 and not @Unchecked.
• We expect that the algebraic difference type (the set-wise relative complement) will be used within the delegates clause and the into clause. We decided to retain the "difference type" meaning when the - operator is used to define a delegation type.
• The syntax for an anonymous pure type is "{" traitspecifiers "}", where traitspecifiers is a semicolon delimited/terminated list of traitspecifier, each of which is either a method/property name or a method/property signature. This syntax is permitted in specific constructs:
  • within a typedef statement
  • within a delegates clause
  • within an into clause
  • for the type specified within an .is() or .as() expression
  • within an extended type expression, as the addend of a union type expression or the subtrahend of a difference type expression
• When an anonymous pure type is used as a subtrahend, the result is a difference type, and not an and not type.

The anonymous pure type syntax is expected to be fairly uncommon. It will be primarily useful for defining delegation sub-sets. While rare, it is an important capability, and we believe that this syntax allows us to "square up" a missing corner of the type algebra, without polluting the general purpose type forms.

Additionally, the terminology changes should help avoid some confusion, particular for anyone with existing knowledge of type theory applied in languages.