Can't scan with a body that has an effect

[axch]

I thought I could write an expression that computes the first few squares like this:

run_state 0 \ref.
  scan 0 \i:(Fin 100) s.
    val = s * get ref
    ref := 1 + get ref
    (s + 1, val)

But the body of scan is type-annotated to be pure, so I got

> Type error:
> Expected: {}
>   Actual: {State h|a}
> (Solving for: [a])
>
>     val = s * get ref
>               ^^^^

I could try to generalize scan, like so

def my_scan {a b n eff} [Ix n] (init:a)
  (body:n->a-> {|eff} (a&b))
  : {|eff} (a & n=>b) =
  swap $ run_state init \s. for i.
    c = get s
    (c', y) = body i c
    s := c'
    y

but then I get this type error

> Type error:
> Expected: {State h|a}
>   Actual: {|eff}
> (Solving for: [a])
>
>     (c', y) = body i c
>               ^^^^^

Is that supposed to happen? Is there a good reason?

[axch]

I know this problem can be worked around by just hand-inlining the definition of scan, but that seems lame.

I know that for the state effect it can also be worked around by including the external state I want to carry in the scan's carries, but (i) that also seems lame; (ii) it will cause extra copies if I don't actually update the external state in every iteration; and (iii) it loses information if the external effect is accum rather than state, and doesn't work at all if the external effect is IO or something like that.

[dougalm]

I discussed this offline with @xnning and she helped me understand the problem.

The effect rules we use during inference, which are stricter than the ones we use during checking, work as follows. Given some effect context, {e1,e2,...|eff}, we can only apply a function if the function's effects can be extended on the right to exactly match the effects in the effect context. "Exactly match" is up to reordering of the concrete effects. So in your my_scan example, if the lambda has effects {State h|eff}, each application in its body must have one of these effects:

1. {State h|eff} Exact match, no right-extension needed.
2. {} Pure, matches exactly if you give it a right-extension of {State h|eff}
3. {State h} Closed effect, matches exactly if you give it a right-extension of {|eff}

The effect of body i c in the above is {|eff} which is not valid, even though informally it feels like a subset of the allowable effects {State h|eff}. It's an "open effect", meaning that it has polymorphic tail, |eff, so it can't be extended on the right at all and it has to match the effect context exactly.

Why do we have this funny rule? It was my attempt at adapting Koka's rules, particularly see Section 2.3 of Daan Leijen's row-polymorphic effect types paper. The advantage of this system, versus something that models bags of effects more directly, is that it almost gives you the behavior of "you get to use any subset of the allowed effects" but without having to deal with inequality constraints during inference.

Note that our type checking rules, i.e. TypeCheck.checkExtends, are more liberal. To make things more confusing, checkExtends is even used during inference in the checkAllowedUnconditionally path. Both of these were added much later and I don't think we gave them much thought.

Where does this leave us with the my_scan example? Ningning points out that it's easy to make it work if we just borrow another feature from Koka, mask, which lets you call body, hiding the calling context's State h effect. mask is sort of the opposite of the handlers like run_state in that it lets you run a computation with fewer effects than the calling context. For us, mask would only be for type checking, but in a system with user-definable effect handlers it would affect semantics too by hiding the topmost handler and potentially exposing a different one underneath.

But maybe we should rethink the effect rows altogether? One big different between Dex and Koka is that we're very to have explicit effect annotations on functions. If we relax the requirements on type inference and ask users to be more explicit maybe a bag-of-effects system can work?