LocalShiftElaboration.hs

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

main :: IO ()
main = do
    putStrLn "[elaborateLocalThenShift]"
    elaborateLocalThenShift

    putStrLn ""
    putStrLn "[elaborateShiftThenLocal]"
    elaborateShiftThenLocal

{-
===== result =====

[elaborateLocalThenShift]
[local scope outer] env = 1.0
[local scope inner] env = 2.0
[local scope outer] env = 1.0
[local scope inner] env = 2.0
[local scope outer] env = 1.0
[local scope inner] env = 2.0
[local scope outer] env = 1.0
[local scope inner] env = 2.0
[local scope outer] env = 1.0
[local scope inner] env = 2.0
[local scope outer] env = 1.0

[elaborateShiftThenLocal]
[local scope outer] env = 1.0
[local scope inner] env = 2.0
[local scope outer] env = 2.0
[local scope inner] env = 4.0
[local scope outer] env = 4.0
[local scope inner] env = 8.0
[local scope outer] env = 8.0
[local scope inner] env = 16.0
[local scope outer] env = 16.0
[local scope inner] env = 32.0
[local scope outer] env = 32.0

-}

elaborateLocalThenShift :: IO ()
elaborateLocalThenShift =
    prog
        & interpretH elaborateLocal
        & interpretAsk 1.0
        & runEff
        & runShift
        & evalState 0
        & runEff
  where
    prog :: (Local Double !! Ask Double + Shift () !! State Int + IO) ()
    prog = do
        k <- send1 getCC
        env <- ask @Double
        send1 $ sendIns $ putStrLn $ "[local scope outer] env = " ++ show env
        local @Double (* 2) do
            whenM (send1 (get @Int) <&> (< 5)) do
                send1 $ modify @Int (+ 1)
                env' <- ask @Double
                send1 $ sendIns $ putStrLn $ "[local scope inner] env = " ++ show env'
                send1 k

elaborateShiftThenLocal :: IO ()
elaborateShiftThenLocal = do
    prog
        & runShift_
        & interpretH elaborateLocal
        & interpretAsk 1.0
        & evalState 0
        & runEff
  where
    prog :: (Shift_ :+: Local Double !! Ask Double + State Int + IO) ()
    prog = do
        k <- getCC_
        env <- ask @Double
        sendIns $ putStrLn $ "[local scope outer] env = " ++ show env
        local @Double (* 2) do
            whenM (get @Int <&> (< 5)) do
                modify @Int (+ 1)
                env' <- ask @Double
                sendIns $ putStrLn $ "[local scope inner] env = " ++ show env'
                k

shift-then-localのほうが「素直」な挙動で（階層が1つだけのため）、local-then-shiftのほうは階層が分かれてる分説明が難しい挙動っぽい
階層の数は型に登場する!!の数を数えれば一応わかります

shift-then-localの挙動が普通な挙動で、local-then-shiftの方はむしろひと工夫必要であって、ひと工夫必要な挙動を強引に実現するためにひと工夫した構造を持ってくる必要がある、みたいな…

一応local-then-shiftの方の挙動の説明を軽く付けておくと、
(Local Double !! Ask Double + Shift () !! State Int + IOなHefty構造の下でsend1 getCCにより継続を取得すると、「localのelaborationの影響を受ける前の命令書としての継続」を取得することができ、これを呼び出すとlocal内でも改変の影響を受けずに振る舞う、みたいな感じです
shift-then-localは普通にAEの意味論の通り