Thunks forced within a handle block don’t infer as needing the provided abilities

It looks like handle blocks don’t add abilities they handle to the wanted abilities of thunks that are forced within the block.

Example:

ability Foo where
  foo : Nat

Foo.handler : Request {Foo} a -> a
Foo.handler = cases
  { a } -> a
  { Foo.foo -> k } -> handle k 0 with Foo.handler

blah a = handle !a with Foo.handler

This infers the type

blah : '{g} o ->{g} o

Which while it’s not exactly wrong, I’d much prefer it infer ’{Foo, g} o ->{g} o.

This is a regression from M2g.

I thought we'd discussed this before, but I can't find where that was if we did.

I'm not really convinced this is a good thing to infer. It seems sensible on very simple examples like the one given, but it can be the opposite on more complex examples. But part of the problem in seeing this is that unison's abilities lack a desirable runtime behavior.

One of the major updates in the revised Frank paper was making it so that (from our perspective) handlers can't intercept effects unless they're explicitly told that some thunk has them. This is crucial to hiding the implementation details of things written with handlers. And the information hiding corresponds to type:

'{e,Foo} a ->{e} a

definitely uses a Foo handler and handles the (designated) Foo effects in the thunk, and:

'{e} a ->{e} a

may or may not use a handler, but cannot handle the thunk's effects. Original Frank had no choice but to have the first type if you used the thunk within a handler, and the revised paper has an extended example of how this makes the types of a significant system really bloated.

It's not just Frank, either. Koka works this way, and there are other papers ways of achieving the same end result.

Since Unison lacks this feature, and handlers just catch every effect, the first type is obviously superior. It is a more precise description of the dynamic behavior. However, I think the nicest way to add this feature is to make the dynamic behavior be type-directed. So, the choice of type assignment determines which abilities are handled and which are passed through. This avoids having to 'lift' computations explicitly in the term level just to mirror what is going on in the types. If more explicit control is desired, it could be had via annotations, rather than requiring that everyone write such annotations always.

Now, for inference, it's just a question of which behavior is the default, not which thing you can do at all. However, it's not clear to me that inferring the handled abilities is a good default. For a top-level definition you can just look at the inferred type and see which thing happened. But for local definitions the inferred type is invisible. So, you may get the undesirable behavior by default, and have no obvious indication of why. And many local definitions may have to be annotated to get the right behavior.

I do have more written about the ability behavior over at #852.

I think it would be possible to infer types more like the one you gave, even though it's kind of contrary to the way the new algorithm works. I just don't think this one example is representative of all the consequences it would have, and am not sure the overall result would be desirable.

I understand and yeah the type-directed stuff discussed in #852 seems better long term. In the short term, given the dynamic behavior of abilities, it seems like we should infer '{e,Foo} a ->{e} a - the Foo ability will get handled by that block, so the type should reflect that. Inferring the other type is a lie right now. WDYT?

Another thing I was pondering is that a thunk could be forced multiple times in a function, each time with a different surrounding stack of handle blocks. What do you infer for the wanted abilities for that thunk, in the absence of an annotation? This seems to have no perfect answer. It could be:

• The empty set, I guess this is what the current algorithm does
• The union of all abilities available in any handle block where it gets forced
• The intersection of abilities available in the blocks where it is forced
• Something else?? Anything else seems like it would be order dependent.

I feel like we should have a point of view on what will be most ergonomic and will require the fewest annotations. I suspect no matter what you decide, there will be examples where it doesn't infer what you want when you don't provide annotations, and that is okay. But if there's a good default then that saves a bunch of manual annotating.