Question about algebraic handler

[MarisaKirisame]

reddit thread:
https://www.reddit.com/r/haskell/comments/8ldmwu/question_about_algebraic_handler/

so I have the following code, and it expectingly fail, but is runtime failure

effect Fail : empty   (* This is equivalent to the type unit -> empty. *)
effect Decide : bool
 
let fail () = absurd (perform Fail) (* Equivalent to perform (Fail ()). *)
let decide () = perform Decide
let const x y = x
;;
 
let hfail = handler
    | x -> Some x
    | effect Fail k -> None
 
let hdecide = handler
    | x -> (fun b -> if b then x else x)
    | effect Decide k -> (fun s -> continue k s s)
;;
 
let res = with hdecide handle with hfail handle
    let x = decide () in
    if x then fail () else 10
in res false
;;
 
let res = with hfail handle with hdecide handle
    let x = decide () in
    if x then fail () else 10
in
match res with
| Some x -> x true
| None -> 100
;;

let x = fail () also fail, but according to the paper it could be cought.
what about the above large piece of code?

[zigaLuksic]

I am not sure what exactly the problem is here. If i have missed the issue please correct me.

Firstly, res is handled and it returns Some f where f is a function that might perform the effect Fail.
Then you use the function f outside of the handlers and the effect Fail is unhandled.

You must also pay attention to the fact that the inner handler is hdecide so the continuation k in hdecide is not handled by a handler that handles the effect Fail which allows it to escape once you reuse the continuation outside of the handlers.

[MarisaKirisame]

Yes, I get that part completely. What I am saying is, can effect system catch this at compile time?

[zigaLuksic]

The effect system described in old papers turned out to be lackluster and has currently been disabled. Eff currently uses only the type system and not the effect system as well.

The branch explicit-effect-subtyping is the current prototype of a stronger effect system, however it is still in development. In the future it should be possible to detect the possibility of Fail being unhandled at compile time.

[MarisaKirisame]

Cool.