Skip to content

Instantly share code, notes, and snippets.

@LightAndLight
Last active August 4, 2021 00:15

Revisions

  1. LightAndLight revised this gist Aug 4, 2021. 1 changed file with 8 additions and 6 deletions.
    14 changes: 8 additions & 6 deletions Plugins.hs
    Original file line number Diff line number Diff line change
    @@ -121,7 +121,7 @@ doubleAndPrint =

    doubleIfTrue :: Plugin
    doubleIfTrue =
    Plugin "DoubleAndPrint" $
    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 IO $ Cons Pure Nil)
    [double, doubleIfTrue, doubleAndPrint] 2
    putStrLn $ "runPlugins: final result is " <> show i
    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
  2. LightAndLight revised this gist Aug 4, 2021. 1 changed file with 22 additions and 8 deletions.
    30 changes: 22 additions & 8 deletions Plugins.hs
    Original 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 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 :: 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 cs c)
    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 :: cs => Capabilities m cs -> Capabilities m cs' -> Maybe (Sub cs cs')
    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 :: c => Int -> m Int
    , _hookCode :: Constraints c => Int -> m Int
    }

    data Plugin
    @@ -121,7 +132,7 @@ doubleIfTrue =
    then 2 * x
    else x

    runPlugins :: (MonadIO m, cap) => Capabilities m cap -> [Plugin] -> Int -> m Int
    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 <-
  3. LightAndLight revised this gist Aug 4, 2021. No changes.
  4. LightAndLight created this gist Aug 4, 2021.
    145 changes: 145 additions & 0 deletions Plugins.hs
    Original 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