& as a conformance conjunction

[dabrahams]

I've always had problems with the use of that symbol to say Equatable & Comparable in Swift and I wonder if we should be following that precedent. I remember Doug resisting that symbol for C++ years ago so I was surprised when it ended up in Swift.

Problems:

• already means mutation / bitwise AND
• tends to imply there will be |

I /think/ we could just replace it with comma without ambiguity.

[kyouko-taiga]

I disagree, for a couple of reasons.

There is precedent in several languages for using & the way Swift (and currently Hylo) does. If T & U reads as an intersection type, then indeed Equatable & Comparable describes a witness of both Equatable and Comparable, which FWIW is exactly what we would use in Scala.

The dual of an intersection type is a union type and I think we should indeed consider using | as a sugar for Union<...>. The fact that we can write Int[8] suggests that we must special case some expressions anyway because otherwise Int[8] would be a subscript application rather than a buffer type expression. Sadly, Int | String is harder to handle for some annoying name resolution reasons, which is why we went for Union<...> (and should probably stick with that for the time being).

There are other instances of "operators" having different semantics if applied on types or terms. For example, Int[8]. There's also precedent for operators having different semantics when applied on different types.

• + means addition and concatenation in Swift depending on its operands;
• ! means negation and forced unwrap;
• many (myself not included) advocate that / should be a concatenation operator for paths;
• etc.

Finally note that we can't replace all occurrences of & with commas without introducing ambiguities in generic parameter lists. For example:

// How many generic parameters are there?
fun f<T: P, Q, R>(_ x: T) { ... }

We'd need a verbose where clause or parentheses, the latter I find more confusing, subjectively of course:

fun f<T, R where T: P, T: Q>(x: T) { ... }
fun f<T: (T, Q), R>(x: T) { ... }

[dabrahams]

If T & U reads as an intersection type, then indeed Equatable & Comparable describes a witness of both Equatable and Comparable

Well OK, but T isn't a type. A trait is a set of requirements, and T&U is a dis-junction (union) of the requirements of T and U.

Anyway, my point about | isn't that it doesn't belong anywhere in the type system (it's perfect for unions), just that it doesn't belong in constraints as a means of composing trait bounds. There's a long and misguided history of people wanting to be able to do that in C++ with concepts, without any real use cases, but still insisting that it ought to be possible.

In fact, if I am understanding intersection types correctly from wikipedia's typescript example:

// given a chicken, produces an egg; given a cow, produces milk
let animalToFood: ((_: Chicken) => Egg) & ((_: Cow) => Milk) =
    function (animal: any) {
        return animal.produce();
    };

what & means in an intersection type is not what we mean in a constraint at all, but in fact what people wanted | to mean in C++, which I'll rephrase as Hylo:

fun f<T: P | Q>(_ x: T) {
  x.something()
}

Where something() happens to be available in both traits, just like produce() happens to be available in both animals above. There are lots of arguments against allowing that. Jaakko once proved that it blows up typechecking (although we may have stepped over that line already 😢) and anyway the chances P and Q choose the same name with the same semantics without establishing any refinement relationship is vanishingly small.

[The Wikipedia Scala example is only apparently using intersection types as a means of analyzing the structure of types rather than to constrain anything and I'm not sure how to connect it to this discussion, though curiously it does seems like it's describing a conjunction of requirements]

Also, this doesn't currently work:

public type Array<Element: Movable & Deinitializable>: Movable & Deinitializable {

The second one has to be a comma. In what way does this make sense?

[kyouko-taiga]

The Wikipedia Scala example is only apparently using intersection types as a means of analyzing the structure of types rather than to constrain anything and I'm not sure how to connect it to this discussion, though curiously it does seems like it's describing a conjunction of requirements.

I am talking about this example:

rait Resettable:
  def reset(): Unit

trait Growable[A]:
  def add(a: A): Unit

def f(x: Resettable & Growable[String]): Unit =
  x.reset()
  x.add("first")

The intersection does "the API of Resettable and the API of Growable. I understand it may be confusing that the API of P & Q is a union of members and conversely the API of P | Q is an intersection, but that is well-established in type theory and mainstream languages (e.g., TypeScript, Scala).

Well OK, but T isn't a type. A trait is a set of requirements, and T&U is a dis-junction (union) of the requirements of T and U.

A trait is in fact a type. It is a generic type parameterized by the type conforming to the described concept. As we have discussed elsewhere, a conformance T: P can be understood as an instance of P<T>. So T: P & Q is a witness of type P<T> & Q<T>, which again is expressible as-is in Scala:

trait P[Self]:
  extension (self: Self) def f(x: Int): Int = x
trait Q[Self]:
  extension (self: Self) def g(x: Int): Int = x

// This function accepts a witness of `T: P & Q` as an explicit parameter.
def h[T](t: T, w: P[T] & Q[T]): Unit =
  println(w.f(t)(1) + w.g(t)(2))

// This is notionally a witness of `String: P & Q`.
val w: P[String] & Q[String] = new P[String] with Q[String]

@main def M =
  h("abc", w)

The second one has to be a comma. In what way does this make sense?

We probably need to change less than 5 lines in the parser to accept the & in addition to or instead of ,.