SE-0413: Typed throws

[Douglas_Gregor]

@woolsweater

Somewhat minor point, but I didn't see this explicitly mentioned. A throwing protocol property requirement will also be able to specify a type? I.e.

protocol Foo {
  var bar: Bar { get throws(BarError) }
}

Yes.

@wadetregaskis

When a function signature uses a generic parameter or associated type as a thrown type, that generic parameter or associated type is implicitly inferred to conform to the Error type. For example, given this declaration for map:

func map<T, E>(body: (Element) throws(E) -> T) throws(E) { ... }

the function has an inferred requirement E: Error.

Is that for some subtle functional reason, or purely for convenience?

It's a convenience, but one that we've always had when you use generic types within a function signature. As you noted, this is what implies the Error conformance for E in Result<T, E>, and its always what implies a Hashable conformance for K in [K: V].

@wadetregaskis

It seems potentially confusing, at least, to allow 'catching' from a closure / function argument that can't actually throw. The compiler doesn't allow similar cases like using the try keyword on a statement that doesn't throw (for good reason, IMO - it suggests a misunderstanding of something or mistake - e.g. wrote the wrong function name - by the code author).

I think the uniform handling of throwing and non-throwing cases far outweighs the potential for confusion here. That's why we have Never in the type system, and why it conforms to Error in the first place.

@wadetregaskis

The pitch largely overlooks the key semantic of rethrows: that the function can only throw if and when its arguments do, and that the compiler enforces this in the implementation of that function. It mentions it only partially and only at the very end (and not even in the main proposal, but under 'Alternatives considered').

I agree that this is the key semantics of rethrows. With typed throws, this semantics mostly falls out from the definition of a generic function where the same type parameter is used for the throwing closure parameters and the resulting function. The map example:

public func map<U, E>( _ transform: (Wrapped) throws(E) -> U ) throws(E) -> U?

In the body of map, how are you going to throw an instance of type E if not by calling transform? Its only constraint is that it conforms to Error, and that protocol doesn't have any way to create a new instance. One would need to either add more constraints on E (which will show up in the signature) or do some kind of dynamic casting to create an instance of E.

@wadetregaskis

I'm not sure if it's intentional or not, but the pitch reads as having a pretty obvious subtext that it wishes rethrows were removed entirely. It almost says exactly that at the very end.

If it is in fact the proposal's intent that rethrows ultimately be removed (even if not by this specific proposal), I suggest it just say that. That's not the sort of change that should be snuck in.

I suspect that rethrows will ultimately be removed from the language. rethrows is in this unfortunate place where there are existing soundness holes in the checking; yet these soundness holes are load-bearing because there are patterns you cannot write with rethrows (the proposal shows this), and code in the wild is using these holes to provide good APIs. So rethrows either needs to be extended and made sound (e.g., the pitch I linked that proposes rethrows(unsafe)), or it needs to be removed.

This proposal isn't removing rethrows outright for several reasons:

1. It's a source-breaking change in a proposal that tries very hard not to be source-breaking.
2. It's possible that there uses of rethrows not well-covered by typed throws (although I have yet to see one).
3. The bar for removal of an existing feature is significantly higher than for the introduction of a new feature, and I don't want this proposal to be delayed by that higher bar.

It might be reasonable to immediately follow up this proposal with another one that lays out the argument for eliminating rethrows. Personally, I think we can let it sit for a year or more to see whether typed throws has subsumed all uses of rethrows.

@Zollerboy1

The proposal has the following note about this:

Note : Exhaustiveness checking in the general is expensive at compile time, and the existing language uses the presence of an unconditional catch block as the indicator for an exhaustive do...catch . See the section on closure thrown type inference for more details about inferring throwing closures.

Can someone explain what's so expensive about exhaustiveness checking? In principle we would just have to loop over every error thrown in the do block and look if it is convertible to one of the catch clauses, no? I cannot imagine why this should be any harder than exhaustiveness checking for switch statements/expressions.

It's trickier than that, because refutable patterns can also have arbitrary Boolean conditions in them. If I have series of catches that each match the HomeworkError enum and check for one of the cases of that enum, and each case is checked, is that also exhaustive?

The actual issue is in closure type inference, though. A syntactically-exhaustive do..catch in a closure means that we know the closure isn't throwing. Doing semantic exhaustiveness checks like you describe means putting the complicated exhaustiveness algorithm (like the one used for switch) in the middle of type inference, meaning it may have to be run many times with different types as input---which can explode type-checking times. We avoid this problem with switch exhaustiveness checking because it only happens later in the compiler... and even then, we had to add timeouts for super-complex switch statements because it's effectively solving the satisfiability problem.

Doug