Last active
August 4, 2021 00:15
Revisions
-
LightAndLight revised this gist
Aug 4, 2021 . 1 changed file with 8 additions and 6 deletions.There are no files selected for viewing
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 charactersOriginal file line number Diff line number Diff line change @@ -121,7 +121,7 @@ doubleAndPrint = doubleIfTrue :: Plugin doubleIfTrue = Plugin "DoubleIfTrue" $ Hook (Cons RWState Nil) fn where fn :: MonadState Bool m => Int -> m Int @@ -152,8 +152,10 @@ unrestricted = Cons RWState $ Cons IO $ Cons Pure Nil main :: IO () main = do i <- runPlugins (Cons Pure Nil) [double, doubleIfTrue, doubleAndPrint] 2 putStrLn $ "runPlugins: final result (only pure plugins) is " <> show i putStrLn "\n-----\n" i <- runPlugins (Cons IO $ Cons Pure Nil) [double, doubleIfTrue, doubleAndPrint] 2 putStrLn $ "runPlugins: final result (pure and IO plugins) is " <> show i -
LightAndLight revised this gist
Aug 4, 2021 . 1 changed file with 22 additions and 8 deletions.There are no files selected for viewing
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 charactersOriginal file line number Diff line number Diff line change @@ -1,3 +1,5 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -7,6 +9,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-} module Main where import Data.Kind (Constraint, Type) @@ -22,23 +25,23 @@ data Name :: (Type -> Type) -> Constraint -> Type where IO :: Name m (MonadIO m) RWState :: Name m (MonadState Bool m) data Capabilities :: (Type -> Type) -> [Constraint] -> Type where Cons :: Name m c -> Capabilities m c' -> Capabilities m (c ': c') Nil :: Capabilities m '[] data Dict :: Constraint -> Type where Dict :: c => Dict c data Sub :: Constraint -> Constraint -> Type where Sub :: a => Dict b -> Sub a b member :: forall cs m c. Constraints cs => Name m c -> Capabilities m cs -> Maybe (Sub (Constraints cs) c) member name cs = case cs of Nil -> Nothing Cons name' rest -> let mSub :: Maybe (Sub (Constraints cs) c) mSub = case (name, name') of (Pure, Pure) -> Just $ Sub Dict @@ -63,7 +66,11 @@ member name cs = Just (Sub Dict) -> Just (Sub Dict) implies :: Constraints cs => Capabilities m cs -> Capabilities m cs' -> Maybe (Sub (Constraints cs) (Constraints cs')) implies cs1 cs2 = case cs2 of Nil -> @@ -77,10 +84,14 @@ implies cs1 cs2 = Sub Dict <- implies cs1 cs2' pure $ Sub Dict type family Constraints cs :: Constraint where Constraints '[] = () Constraints (c ': cs) = (c, Constraints cs) data Hook m = forall c. Hook { _hookCapabilities :: Capabilities m c , _hookCode :: Constraints c => Int -> m Int } data Plugin @@ -121,7 +132,7 @@ doubleIfTrue = then 2 * x else x runPlugins :: (MonadIO m, Constraints cap) => Capabilities m cap -> [Plugin] -> Int -> m Int runPlugins caps plugins i = case plugins of [] -> pure i @@ -136,6 +147,9 @@ runPlugins caps plugins i = liftIO $ putStrLn $ "runPlugins: finished running " <> name runPlugins caps ps i' unrestricted :: Capabilities m '[MonadState Bool m, MonadIO m, Monad m] unrestricted = Cons RWState $ Cons IO $ Cons Pure Nil main :: IO () main = do i <- -
LightAndLight revised this gist
Aug 4, 2021 . No changes.There are no files selected for viewing
-
LightAndLight created this gist
Aug 4, 2021 .There are no files selected for viewing
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 charactersOriginal file line number Diff line number Diff line change @@ -0,0 +1,145 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE FlexibleContexts #-} module Main where import Data.Kind (Constraint, Type) import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Applicative ((<|>)) class Monad m => MonadState s m | m -> s where get :: m s put :: s -> m () data Name :: (Type -> Type) -> Constraint -> Type where Pure :: Name m (Monad m) IO :: Name m (MonadIO m) RWState :: Name m (MonadState Bool m) data Capabilities :: (Type -> Type) -> Constraint -> Type where Cons :: Name m c -> Capabilities m c' -> Capabilities m (c, c') Nil :: Capabilities m () data Dict :: Constraint -> Type where Dict :: c => Dict c data Sub :: Constraint -> Constraint -> Type where Sub :: a => Dict b -> Sub a b member :: forall cs m c. cs => Name m c -> Capabilities m cs -> Maybe (Sub cs c) member name cs = case cs of Nil -> Nothing Cons name' rest -> let mSub :: Maybe (Sub cs c) mSub = case (name, name') of (Pure, Pure) -> Just $ Sub Dict (Pure, IO) -> Just $ Sub Dict (Pure, RWState) -> Just $ Sub Dict (IO, Pure) -> Nothing (IO, IO) -> Just $ Sub Dict (IO, RWState) -> Nothing (RWState, Pure) -> Nothing (RWState, IO) -> Nothing (RWState, RWState) -> Just $ Sub Dict in case mSub of Nothing -> case member name rest of Nothing -> Nothing Just (Sub Dict) -> Just (Sub Dict) Just (Sub Dict) -> Just (Sub Dict) implies :: cs => Capabilities m cs -> Capabilities m cs' -> Maybe (Sub cs cs') implies cs1 cs2 = case cs2 of Nil -> case cs1 of Nil -> Just $ Sub Dict Cons{} -> Just $ Sub Dict Cons name cs2' -> do Sub Dict <- member name cs1 Sub Dict <- implies cs1 cs2' pure $ Sub Dict data Hook m = forall c. Hook { _hookCapabilities :: Capabilities m c , _hookCode :: c => Int -> m Int } data Plugin = Plugin { _pluginName :: String , _pluginHook :: forall m. Hook m } double :: Plugin double = Plugin "Double" $ Hook (Cons Pure Nil) fn where fn :: Monad m => Int -> m Int fn x = pure $ 2 * x doubleAndPrint :: Plugin doubleAndPrint = Plugin "DoubleAndPrint" $ Hook (Cons IO Nil) fn where fn :: MonadIO m => Int -> m Int fn x = do let x' = 2 * x liftIO $ print x' pure x' doubleIfTrue :: Plugin doubleIfTrue = Plugin "DoubleAndPrint" $ Hook (Cons RWState Nil) fn where fn :: MonadState Bool m => Int -> m Int fn x = do b <- get pure $ if b then 2 * x else x runPlugins :: (MonadIO m, cap) => Capabilities m cap -> [Plugin] -> Int -> m Int runPlugins caps plugins i = case plugins of [] -> pure i Plugin name (Hook pluginCaps hook) : ps -> case implies caps pluginCaps of Nothing -> do liftIO . putStrLn $ "runPlugins: skipping " <> name <> " because we didn't provide enough capability" runPlugins caps ps i Just (Sub Dict) -> do liftIO . putStrLn $ "runPlugins: running " <> name i' <- hook i liftIO $ putStrLn $ "runPlugins: finished running " <> name runPlugins caps ps i' main :: IO () main = do i <- runPlugins (Cons IO $ Cons Pure Nil) [double, doubleIfTrue, doubleAndPrint] 2 putStrLn $ "runPlugins: final result is " <> show i