frank-lang / frank Goto Github PK

Why choose call-by-push-value as opposed to a fine-grained calculus (like Eff does)? In what sense is a lambda abstraction a computation?

Would you be open to adding a FOSS license to the repo? I'm working on a fork and it'd be nice to have some clarity on what the status is.

Nice Name I will write a parser and interpreter for graalvm

The following code

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.