ymdryo

use std;

effect State {
    get() Int
    put(Int) ()
}

let hState = handler {
    return(x) {
        fn(s: Int) {

ymdryo

-- 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 ""

ymdryo

callCC :: forall r m a. (Shift r <<: m, Monad m) => ((a -> m r) -> m a) -> m a
callCC f = shift @r \k -> k =<< f (k >=> exit)

exit :: (Shift r <<: m, Applicative m) => r -> m a
exit r = shift \_ -> pure r

ymdryo

elaborateShift ::
    (MonadFreer c fr, Union u, c (Eff u fr eh ef), HFunctor (u eh)) =>
    Eff u fr (Shift ': eh) ef ~> Eff u fr eh ef
elaborateShift a =
    a & interpretKAllH_ pure \k ->
        (\(Shift f) -> elaborateShift $ f (raiseH . k))
            |+: (k <=< injectH . hfmap elaborateShift)

data Shift m a where
    Shift :: (forall (r :: Type). (a -> m r) -> m r) -> Shift m a

ymdryo

test :: (Local Int !! Ask Int + (!) (State Bool + IO)) ()
test = do
    raise $ send0 $ put False
    k <- getCC
    local @Int (+ 1) do
        unlessM (raise $ send0 get) k
        raise $ send0 $ put True
        env <- ask @Int
        raise $ send0 $ sendIns $ print env

ymdryo

callCC ::
    (MonadFreer c fr, Monad (fr f), c (FreerChurch f)) =>
    (forall r. (a -> fr f r) -> fr f a) ->
    fr f a
callCC f = reencodeFreer $ callCcChurch \exit -> reencodeFreer $ f (reencodeFreer . exit)

callCcChurch :: (forall r. (a -> FreerChurch f r) -> FreerChurch f a) -> FreerChurch f a
callCcChurch f = FreerChurch $ FT \k g -> runFT (unFreerChurch $ f $ pure . runIdentity . k) k g

getCC :: (MonadFreer c fr, Monad (fr f), c (FreerChurch f)) => fr f (fr f ())

ymdryo

括弧が見づらいので()に加えて[],{}も括弧の代わりに使います
つまり[]はいわゆるHaskellのリストの型ではないので注意してください

まず前提として
Hefty h a = Return a | Op [h (Hefty h) (Hefty h a)]
Coyoneda f a = ∀b. (b -> a,  f b)
です
(cf. https://twitter.com/ymdfield/status/1743235218847465546)

ここでCoyonedaの高階版を定義します

ymdryo

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE UndecidableInstances #-}

-- 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/.

module Control.Hefty where

import Control.Applicative (Alternative)

ymdryo

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- This Source Code Form is subject to the terms of the Mozilla Public

ymdryo

-- 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/.

class HFunctorT (e :: SigClass) where
    type HFTDict e :: ((Type -> Type) -> Type -> Type) -> Type
    type HFTDict _ = (:~:) IdentityT

    hfmapT :: (forall t. HFTDict e t -> t f ~> t g) -> e f ~> e g