[swift-dev] A constraint system / type variable question

[John McCall]

> On Sep 26, 2017, at 11:22 AM, Joe Groff via swift-dev <swift-dev at swift.org> wrote:
>> On Sep 25, 2017, at 7:53 PM, David Zarzycki <dave at znu.io> wrote:
>>> On Sep 25, 2017, at 21:59, Joe Groff via swift-dev <swift-dev at swift.org> wrote:
>>> On Sep 25, 2017, at 3:41 PM, David Zarzycki <dave at znu.io> wrote:
>>> 
>>>> 
>>>> 
>>>>> On Sep 25, 2017, at 18:23, Joe Groff <jgroff at apple.com> wrote:
>>>>> 
>>>>> 
>>>>> 
>>>>>> On Sep 25, 2017, at 1:04 PM, David Zarzycki <dave at znu.io> wrote:
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>>> On Sep 25, 2017, at 14:37, Joe Groff <jgroff at apple.com> wrote:
>>>>>>> 
>>>>>>> 
>>>>>>> 
>>>>>>>> On Sep 23, 2017, at 10:36 PM, Robert Widmann via swift-dev <swift-dev at swift.org> wrote:
>>>>>>>> 
>>>>>>>> Why is the arrow carrying the “Has Value Semantics Bit” rather than it being part of a protocol composition on an argument type, or a convention bit on the parameter like ‘inout’?
>>>>>>> 
>>>>>>> Value semantics is a property of operations, not really of types. I would say the function arrow is the right place for it, since not-value-semantics propagates in the same manner as an effect like "throws". Dave, you might in fact look at how 'throws' type checking is implemented as a model for what you're trying to do.
>>>>>> 
>>>>>> Hi Joe,
>>>>>> 
>>>>>> In fact, I tried to replicate the “closureCanThrow()” logic before emailing this list, but that didn’t work due to a chicken-and-egg problem that arrises between when a ClosureExpr's body is type checked and knowing the type of the ClosureExpr. In other words, a closure has value semantics iff all operations within it have value semantics.
>>>>>> 
>>>>>> As I wrote earlier in this email thread, the “value semantics” implementation I’m working on is sufficient for the research that I’m doing. That being said, I took some shortcuts to get it working and the closure type shortcut bothered me the most. That is why I emailed this list about how to propagate the contextual ExtInfo bit onto the closure type. Based on John’s helpful email, I think I’ll just live with the shortcuts I made for now.
>>>>> 
>>>>> If you have something working well enough for your prototype, then great. If you do decide to look at this again, I think it might be easier to flip the polarity of the check—a closure is not-value-semantics if it does anything that's not-value-semantics—which should make it the exact same kind of problem as `throws` propagation.
>>>> 
>>>> Thanks. FWIW – I thought about that because ExtInfo has a bias towards “false” as the default for flags within it, and that forced me to contemplate what the default semantics should be. Unfortunately, either default doesn’t work for the same reason: the ExtInfo bits are stored in the type, but closure body type checking is done after the type of the closure is needed.
>>> 
>>> The other thing `throws` does is establish a subtype relationship from nonthrowing to throwing functions, so if analysis determines a closure doesn't throw, but we later determine that we need a throwing one, we can implicitly convert. I think it'd be appropriate to allow a similar conversion from pure-value-semantics to non-value-semantics, and I think that'd address your issue.
>> 
>> Ya, the “throws” subtyping and related conversion was useful to crib from, but I don’t see how that helps the contextual ClosureExpr type scenario. Unlike “throws” (and absent a contextual type), deducing the value semantic nature of a closure requires type checking the body first. Am I missing something? Is there a scenario that I can crib from where ExtInfo bits of the contextual function type propagate onto the type of a ClosureExpr?
> 
> Checking whether a function throws or not also requires type-checking the body, since otherwise we don't know whether 'catch' blocks are exhaustive or whether 'try' subexpressions actually cover a failable operation. I'm definitely not an expert on the type checker, so I'm probably missing something, but it seems like the same problem.

We actually just use a heuristic to infer it from scratch, by looking for 'try's that aren't inside any apparently-exhaustive do/catch.  It's not illegal for 'try' to not cover a failable operation, but in practice the heuristic seems to have worked well.

It is something we would probably need to completely rewrite if we had typed-throws, of course.

John.