Skip to content

Instantly share code, notes, and snippets.

@layus
Created July 1, 2022 14:22
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save layus/ccbeee965ec8cb6841810206cd223300 to your computer and use it in GitHub Desktop.
Save layus/ccbeee965ec8cb6841810206cd223300 to your computer and use it in GitHub Desktop.
{-# 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