Function subtyping in requirement satisfaction

[dabrahams]

This discussion is a placeholder for discussing whether and to what extent, things like the following should be legal

trait P {
  fun f() throws
  fun g(_: sink Int)
}

type X: P {
  fun f() {}
  fun g(_: Int) {}
}

I suppose doing something like this would also imply subtyping of function types… I know we have a little subtyping already and I forget whether that's included.

I can see real problems with not supporting this in some form if we start doing things like rejecting throws on functions that can't throw or rejecting sink on parameters that aren't consumed in the callee (or even warning of these things!)

[kyouko-taiga]

I don't know if we want subtyping on function types but it is not necessarily the end of the world if we do. That being said, I think we should actually implement compiler-blessed conversions (😱) instead of using subtyping.

AFAICT the question is relevant in two cases:

• The construction of witness tables
• Passing lambdas to parameters

In both cases, we really really want some kind of flexibility. For example, the following has to work IMO:

type Box: Regular {
  // ...
  public fun map<E>(_ f: inout [E](Int) inout -> Int) { ... }
}

public fun main() {
  var b Box()
  b.map((x) => x + 1) // Note: the type of the lambda is `[Void](Int) let -> Int`
}

The way I see that working is that we teach the compiler a bunch of ways in which it can create thin wrappers around functions during eta-expansion. We do the same for witness tables.

[kyouko-taiga]

Note that there are non-trivial cases to consider. For example, you can technically satisfy (sink T) -> U with (let T) -> U but only if T is deinitializable.

Also, we need to think about our story for polymorphic effects because it'd be nice if the map function above can accept a throwing and/or unsafe lambda. I'm still hoping we can smuggle capabilities in the lambda environment but if we can't we'll have to do something similar to Swift.

I don't like rethrows so much, in part because reunsafe doesn't make any sense. Perhaps throws? and unsafe?. But that's bike shedding at this point. A design with capabilities is clearly preferable IMO, if we can make it work.