xnning / EvEff

Efficient Haskell effect handlers based on evidence translation.
BSD 3-Clause "New" or "Revised" License
81 stars 5 forks source link

Latent Effects #8

Open noughtmare opened 3 years ago

noughtmare commented 3 years ago

To continue exploring expressivity from issue #5, let us consider the notion of latent effects from "Staged Effects and Handlers for Modular Languages with Abstraction" by Casper Bach Poulsen, Cas van der Rest and Tom Schrijvers (link to their repo on github).

They consider an effectful program with lambda bindings:

prog :: (Lam :? e, State Val :? e) => Eff e Val
prog = do
  put (IntVal 0)
  clos <- lambda "x" get -- the x argument is ignored
  put (IntVal 42)
  apply clos (IntVal 0)

Assuming these definitions exist (they can probably be implemented with the scoped effects technique from #5):

put :: State s :? e => s -> Eff e ()
get :: State s :? e => Eff e s
lambda :: Lam :? e => String -> Eff e Val -> Eff e Val
apply :: Lam :? e => Eff e Val -> Eff e Val -> Eff e Val

And Val is some value type of an embedded language that supports function closures and integer constants. E.g.:

data Val = Var String | Lam String Val | App Val Val | IntVal Int

If we now handle the State effect first then in the normal view the get will be evaluated under the lambda and become the constant value 0. Then handling Lam will yield the result IntVal 0.

But we would like to be able to handle our functions in such a way that the get under the lambda will be delayed or treated as a latent effect that is only evaluated at the place where the lambda is applied. Then the result should be IntVal 42.