Polysemy: Final

In a previous log, we introduced Higher-order effects definition and interpretation through tactics.

We'll see in another log an alternative way to define them.

Polysemy recommends using Final instead of Embed for interpreters.

It's defined as follows:

newtype Final m z a where
  WithWeavingToFinal
    :: ThroughWeavingToFinal m z a
    -> Final m z a

don't worry, it does aim to be used directly.

Hopefully, it's basic usage is identical to Embed:

runFinal $ embedFinal $ putStrLn "Hello, world!"

See the full the code here.