Created
July 1, 2022 14:22
-
-
Save layus/ccbeee965ec8cb6841810206cd223300 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# language DataKinds #-} | |
{-# language FlexibleContexts #-} | |
{-# language GADTs #-} | |
{-# language LambdaCase #-} | |
{-# language PolyKinds #-} | |
{-# language RankNTypes #-} | |
{-# language ScopedTypeVariables #-} | |
{-# language TypeApplications #-} | |
{-# language TypeOperators #-} | |
{-# language TypeFamilies #-} | |
{-# language TemplateHaskell #-} | |
{-# language BlockArguments #-} | |
{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-} | |
{-# LANGUAGE AllowAmbiguousTypes #-} | |
import Data.Typeable | |
import Data.Functor (($>), (<$)) | |
import Control.Monad | |
import Polysemy.Reader | |
import Polysemy.Embed | |
import Polysemy.Final | |
import Polysemy.State | |
import Polysemy.Error | |
import Polysemy.Internal | |
import Polysemy.Internal.Union | |
import Polysemy.Internal.Tactics | |
import Polysemy hiding (run) | |
import Data.Map as Map | |
import Data.Map (Map) | |
import Data.IORef | |
import Unsafe.Coerce (unsafeCoerce) | |
import Type.Reflection | |
import Debug.Trace (traceM) | |
--- -_- | |
data MaybeValue (r :: EffectRow) a = {- forall f. (Typeable f, Functor f) => -} Action (Sem r (Maybe a)) | Value (Maybe a) | |
type Ref = IORef | |
data Thunk (r :: EffectRow) a = Thunk String (Ref (MaybeValue r a)) (Ref Bool) | |
data Memo r a :: Effect where | |
Force :: Thunk r a -> Memo r a m (Maybe a) | |
Defer :: String -> m a -> Memo r a m (Thunk r a) | |
makeSem ''Memo | |
-- interpretH | |
-- :: (forall rInitial x . e (Sem rInitial) x -> Tactical e (Sem rInitial) r x) | |
-- -- ^ A natural transformation from the handled effect to other effects | |
-- -- already in 'Sem'. | |
-- -> Sem (e ': r) a | |
-- -> Sem r a | |
-- interpretH f (Sem m) = Sem $ \k -> m $ \u -> | |
-- case decomp u of | |
-- Left x -> k $ hoist (interpretH f) x | |
-- Right (Weaving e s d y v) -> do | |
-- fmap y $ usingSem k $ runTactics s d v (interpretH f . d) $ f e | |
-- | |
-- hoist :: (forall x. m x -> n x) -> Union r m a -> Union r n a | |
-- hoist f' (Union w (Weaving e s nt f v)) = | |
-- Union w $ Weaving e s (f' . nt) f v | |
-- | |
-- runMemo :: forall a r x. (Show a, Member (Embed IO) r) => Sem (Memo r a : r) x -> Sem r x | |
-- runMemo (Sem (runner :: forall m. Monad m => (forall resultType. Union (Memo r a : r) (Sem (Memo r a : r)) resultType -> m resultType) -> m x)) = | |
-- Sem $ \(k :: forall x1. Union r (Sem r) x1 -> m x1) -> | |
-- runner $ \(u :: Union (Memo r a : r) (Sem (Memo r a : r)) resultType) -> | |
-- case decomp u of | |
-- Left | |
-- (Union | |
-- (w :: ElemOf e' r) | |
-- (Weaving -- @f_ @e_ @rInitial @a @resultType @mAfter | |
-- (wEffect :: e' (Sem rInitial) x3) | |
-- (wState :: f' ()) | |
-- (wDistrib :: forall x. f' (Sem rInitial x) -> Sem (Memo r a : r) (f' x)) | |
-- (wResult :: f' x3 -> resultType) | |
-- (wInspect :: forall x. f' x -> Maybe x) | |
-- ) :: Union r (Sem (Memo r a : r)) x0) | |
-- -> k $ | |
-- ((Union w $ Weaving wEffect wState (runMemo . wDistrib) wResult wInspect) :: Union r (Sem r) x0) | |
-- Right (Weaving -- @f_ @e_ @rInitial @a @resultType @mAfter | |
-- (wEffect :: (Memo r a) (Sem rInitial) a1) | |
-- (wState :: f' ()) | |
-- (wDistrib :: forall x. f' (Sem rInitial x) -> Sem (Memo r a : r) (f' x)) | |
-- (wResult :: f' a1 -> resultType) | |
-- (wInspect :: forall x. f' x -> Maybe x) | |
-- :: Weaving (Memo r a) (Sem (Memo r a : r)) x1) -> do | |
-- case wEffect of | |
-- ((Force (Thunk name ref _)) :: (Memo r a (Sem rInitial) a1)) -> do | |
-- content <- usingSem k $ embed @IO (readIORef ref) | |
-- case content of | |
-- Failed v -> pure $ wResult (myCoerce v) | |
-- Value v -> pure $ wResult (v <$ wState) | |
-- Action (action :: Sem r (f a)) -> do | |
-- value :: f' a <- myCoerce <$> usingSem k action | |
-- let evaluated :: MaybeValue r a = maybe (Failed value) (Value) (wInspect value) | |
-- usingSem k $ embed @IO (writeIORef ref evaluated) | |
-- return $ wResult value | |
-- ((Defer name (action :: Sem rInitial a)) :: (Memo r a (Sem rInitial) a1)) -> do | |
-- let z :: (Sem r (f' a)) = runMemo $ wDistrib $ action <$ wState | |
-- ref <- usingSem k $ embed @IO (newIORef (Action z)) | |
-- lock <- usingSem k $ embed @IO (newIORef False) | |
-- return $ wResult $ Thunk name ref lock <$ wState | |
-- runTactics s d v d' ... of Right (Weaving Op s' _ y _) -> | |
-- GetInitialState = pure $ y $ s <$ s' | |
-- HoistInterpretation na = pure $ y $ (d . fmap na) <$ s' | |
-- HoistInterpretationH na fa = (y . (<$ s')) <$> runSem (d' (fmap na fa)) k | |
-- GetInspector s' _ y _) -> pure $ y $ Inspector v <$ s' | |
-- | |
-- getInspectorT :: forall e f m r. Sem (WithTactics e f m r) (Inspector f) | |
-- getInspectorT = send @(Tactics _ m (e ': r)) GetInspector | |
-- | |
-- pureT :: Functor f => a -> Sem (WithTactics e f m r) (f a) | |
-- pureT a = do | |
-- istate <- getInitialStateT | |
-- pure $ a <$ istate | |
-- | |
-- we get the f' (), and then force feed the a into it, so we get f' a. | |
-- pureT a = a <$ wState | |
-- | |
-- runTSimple :: m a | |
-- -- ^ The monadic action to lift. This is usually a parameter in your | |
-- -- effect. | |
-- -> Tactical e m r a | |
-- runTSimple na = do | |
-- istate <- getInitialStateT | |
-- bindTSimple (const na) istate | |
-- | |
-- getInitialStateT = GetInitialState | |
-- | |
-- bindTSimple f s = send @(Tactics _ _ (e ': r)) $ HoistInterpretationH f s | |
-- runTSimple action = fmap (wResult . (<$ wState')) (usingSem k ((runMemo . wDistrib) (action <$ wState))) | |
-- | |
-- runT na = do | |
-- istate <- getInitialStateT | |
-- na' <- bindT (const na) | |
-- pure $ na' istate | |
-- | |
-- bindT f = send $ HoistInterpretation f | |
-- bindT na = pure $ wResult $ (wDistrib('?) . fmap na) <$ wState | |
-- runT na = do | |
-- na' <- pure $ wResult $ (wDistrib('?) . fmap (const na)) <$ wState' | |
-- pure $ na' wState | |
-- | |
-- where | |
-- interpreter :: forall rInitial x. (Memo a) (Sem rInitial) x -> Tactical (Memo a) (Sem rInitial) r x | |
-- interpreter = \case | |
-- Force (Thunk ref _) -> do | |
-- content <- embed @IO (readIORef ref) | |
-- case content of | |
-- Value v -> pureT v | |
-- Action (action :: m a) -> do | |
-- -- Todo: check the lock for force loops. | |
-- Inspector ins <- getInspectorT | |
-- value <- ins <$> runTSimple action | |
-- embed @IO (writeIORef ref (Value value)) | |
-- pureT value | |
-- Defer (action :: m a) -> do | |
-- ref <- embed @IO (newIORef (Action action)) | |
-- lock <- embed @IO (newIORef False) | |
-- pureT (Thunk ref lock) | |
runMemo :: forall a r x. (Typeable a, Member (Embed IO) r) => Sem (Memo r a : r) x -> Sem r x | |
runMemo = interpretH interpreter | |
where | |
interpreter :: forall rInitial x. (Memo r a) (Sem rInitial) x -> Tactical (Memo r a) (Sem rInitial) r x | |
interpreter = \case | |
Force (Thunk name ref _) -> do | |
content <- embed @IO (readIORef ref) | |
case content of | |
Value v -> pureT v | |
Action (action :: Sem r (Maybe a)) -> do | |
-- Todo: check the lock for force loops. | |
-- We _know_ it is the same f, as long as no-one plays around with several Thunk types. | |
-- How to enforce that f = f' in the types ? | |
-- We need something like functional dependencies, where rInitial, r -> f | |
-- f is fixed by the set of effects that have run before us. | |
-- it is only known in the final step, where we interpret everything. | |
-- If only we could make it opaque and private to a given runMemo invocation where all the types are know... | |
-- Inspector ins <- getInspectorT | |
-- embed $ putStrLn . (\s -> "Forcing " ++ name ++ " with type " ++ s) . show $ Type.Reflection.typeRep @(a) | |
value :: Maybe a <- myCoerce <$> raise action | |
-- embed $ putStrLn . (\s -> "Forcing " ++ name ++ " with forced type " ++ s) . show $ Type.Reflection.typeRep @(a) | |
-- !! You need Typeable in the Thunk type :-) | |
let evaluated = Value value | |
embed @IO (writeIORef ref evaluated) | |
pureT value | |
Defer name (action :: Sem rInitial a) -> do | |
Inspector ins <- getInspectorT | |
value :: Sem r (Maybe a) <- fmap ins . runMemo <$> runT action | |
-- embed $ putStrLn . (\s -> "Thunking " ++ name ++ " with state " ++ s) . show $ Type.Reflection.typeRep @(f a) | |
ref <- embed @IO (newIORef (Action value)) | |
lock <- embed @IO (newIORef False) | |
pureT (Thunk name ref lock) | |
myCoerce :: a -> b | |
myCoerce = unsafeCoerce | |
{-# NOINLINE myCoerce #-} | |
main :: IO () | |
main = do | |
print =<< runApp 1 mainApp | |
putStrLn $ "#==> between <==#" | |
print =<< runApp 0 mainApp | |
-- runApp :: Sem '[Reader Int, Memo String, Error String, Embed IO, Final IO] a -> IO (Either String a) | |
runApp i = runFinal . embedToFinal @IO . evalState True . runMemo . runError . runReader i | |
mainApp :: forall r r'. (Members [Reader Int, Memo r' String, Embed IO, Error String, State Bool] r) => Sem r String | |
mainApp = do | |
embed @IO $ putStrLn "Hello" | |
t1 <- defer "(echoAction \"Foo\")" (echoAction "Foo") | |
(i :: Int, t2) <- runState 4 $ defer "lol" $ do | |
put 5 | |
echoAction "Bar" | |
embed $ print i | |
t3 <- defer "(someAction \"Lol\" t1)" (someAction "Lol" t1) | |
t4 <- defer "(someAction \"bar\" t2)" (someAction "bar" t2) | |
t5 <- defer "(mainApp)" (mainApp) | |
show <$> force t4 | |
echoAction :: (Members [Embed IO, Reader Int, State Bool] r) => String -> Sem r String | |
echoAction s = do | |
i <- ask | |
b <- get | |
embed @IO (putStrLn ("Echo: " ++ s ++ " outer " ++ show i ++ " inner " ++ show b)) | |
pure s | |
-- Postfix style, to make torsten happy | |
someAction :: | |
Members '[Reader Int, Memo r' String, Error String, State Bool] r => | |
String -> | |
Thunk r' String -> | |
Sem r String | |
someAction s t = do | |
i <- ask | |
modify not | |
w <- local (const 10) $ force t | |
ss <- ((s ++ " " ++ show i ++ " " ++ show w ++ " is ") ++) . show <$> force t | |
when (i == 0) $ throw $ "Error reached at " ++ ss | |
pure ss | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment