Type errors when intercepting effects

Ecosystem
1

I’m experimenting with intercepting effects as in order to attach information to them, for example in order to prioritise certain fibres.

This as an idea seemingly does work, although there is many slightly weird type errors.

Throughout this I’m using the State example.

After much trial and error here is a working example.

effect Get : string
effect Priority : 'a eff * string -> 'a

let run f ~init =
  let comp =
  match f () with
  | x -> (fun s -> x)
  | effect (Priority (Get, p)) k -> (fun (s : string) -> print_endline p; continue k s s)
  in comp init

let priority f ~p =
  match f () with
  | x -> x
  | effect Get k -> let r = perform (Priority (Get, p)) in continue k r;;

let () =
  run ~init:"1" @@
  @@ fun () -> priority ~p:"p"
  @@ print_endline (perform Get)

Q1. You need to constrain the type of s in run?

Unfortunately I don’t quite understand how some of the typing constraints passes around.
For example one persistent problem was that if s is not constrained to be a string its usage in the continue k s s fails to type check:

Error: This expression has type 'a but an expression was expected of type
         effect
       This instance of effect is ambiguous:
       it would escape the scope of its equation

Why is it expecting the type to be an effect?

Q2. Polymorphic continuations cannot be passed via effects?

Additionally one change which would be nice to have would be to pass the continuation up through the priority effect, such that on the return the priority function would not need to be involved, ie:

effect Priority : 'a eff * ('a, 'b) continuation * string -> unit
let run f ~init =
  let comp = 
  match f () with
  | x -> (fun s -> x)
  | effect (Priority (Get, k, _)) _ -> fun (s : string) -> continue k s s
  in comp init

All variants I’ve tried to write using this unfortunately unify the 'b with effect, but I am not sure why this is occurring, if I manually type 'b : int, run type checks, but then it is not polymorphic.

Q3. Multiple effects leading to the same outcome?

Finally one nice simplification in these situations may be to have a match statement as follows:

let run f ~init =
  let comp =
  match f () with
  | x -> (fun s -> s)
  | effect (Priority (Get, k, _)) _ 
  | effect Get k -> fun (s : string) -> continue k s s

However this fails with the error:

Effect patterns must be at the top level of a match case

Are these style of patterns just not possible using effects? I am fairly sure that it was possible to do similar patterns for exceptions, though I am probably mistaken.

Conclusion

I’m expecting that the answer to the first two of these is that I need to better constrain the type of Priority, which I would love to hear how to do this :slight_smile: .

If there is some underlying issue with this approach that would also be great to hear!

Overall though the new effects system is very very cool, super versatile and expressive!

3 Likes
2

Perhaps it would help to see an example without effects that is the same from a typing perspective:

type 'a ef = ..

type 'a ef +=
| Get : string ef
| Priority : 'a ef * string -> 'a ef

type 'b t = Eff : 'a ef * ('a -> 'b) -> 'b t;;

let run f ~init =
  let comp =
    match f () with
    | Eff ((Priority (Get, p)), k) ->
        (fun (s : string) -> print_endline p; k s s)
    | _ -> assert false
  in
  comp init;;

If you remove the string type annotation you get:

5 |           (fun s -> print_endline p; k s s)
                                           ^
Error: This expression has type 'a but an expression was expected of type
         string 
       This instance of string is ambiguous:
       it would escape the scope of its equation
2 Likes
3

Thanks for the reply!

So the removal of the string annotation would constrain the types of the continuations in an unbounded fashion?

What is confusing me is specifically, is that I would assume in the unconstrained situation that the following unifications would occur:

Get : string ef
Priority (Get, p) => Priority (_) : string ef
Eff(Priority(_), k) => Eff : string ef * (string -> 'b) -> 'b t
(fun s -> k s s) & k : string -> 'b => s : string & 'b = (string -> 'c)

Which should type check?

Is there something I’m missing in the modelling or calculation of these constraints?

4

The Eff constructor has an existential 'a. So when you match on it you get some fresh abstract type, let’s call it ext. When you match on Get you learn that ext is equal to string. The function:

(fun s -> print_endline p; k s s)

then has two possible types:

string -> 'c

or

ext -> 'c

Those two types are equal whilst the equation from Get is in scope, but this function is being returned outside of that scope, which means that the types would become unequal and its not clear which one of them should be used. This is why the type-checker is complaining about ambiguity. If you add a type annotation then it is no longer ambiguous.

2 Likes
5

Ah fascinating!

So this is why in the effects examples here use concrete (?) types?

Regardless thanks for the help!