data D X = d X X
interface Eff X = op : Int -> X
handle : <Eff Int> X -> X
handle x = x
handle <op x -> k> = handle (k x)
step : <Eff (D X)> Y -> [Eff X, Eff (D X)] Y
step x = x
step <op n -> k> =
let r = d (<Eff> (op n)) (<Eff> (op n)) in
<Eff(s a b -> s b b a)> (k r)
full : <Eff (D X)> Y -> [Eff X] Y
full x = x
full <m> = full (step (<Eff(s a b b -> s b a)> m!))
run : {(D X) -> [Eff X, Eff (D X)] (D X)} -> X -> [Eff X] X
run f x = let z = d x x in full (case (f z) {(d _ r) -> r})
main : {Int}
main! = handle (run {_ -> op 0} 1)
produces
frank: Unhandled command: abort.0
CallStack (from HasCallStack):
error, called at shonky/src/Shonky/Semantics.hs:248:30 in main:Shonky.Semantics
The bug is in the type checker, it reverses the order of effects in bodies of step and full, as witnessed by the adaptors used in the definitions. However, the order of effects shouldn't be reversed. When the program runs, the op effect in main is handled by handle instead of full, and thus the result of f z in run is not of type D Int, and so pattern matching fails causing the unhandled abort.
By changing <Eff(s a b -> s b b a)> to <Eff(s a b -> s a b b)> and <Eff(s a b b -> s b a)> to <Eff(s a b b -> s a b)> in the resulting shonky code, the program succeeds.
The following code
produces
The bug is in the type checker, it reverses the order of effects in bodies of
step
andfull
, as witnessed by the adaptors used in the definitions. However, the order of effects shouldn't be reversed. When the program runs, theop
effect inmain
is handled byhandle
instead offull
, and thus the result off z
inrun
is not of typeD Int
, and so pattern matching fails causing the unhandledabort
.By changing
<Eff(s a b -> s b b a)>
to<Eff(s a b -> s a b b)>
and<Eff(s a b b -> s b a)>
to<Eff(s a b b -> s a b)>
in the resulting shonky code, the program succeeds.