Plugins.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
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. 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
            (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 ::
  Constraints cs =>
  Capabilities m cs ->
  Capabilities m cs' ->
  Maybe (Sub (Constraints cs) (Constraints 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

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
  = 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 "DoubleIfTrue" $
  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, Constraints 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'

unrestricted :: Capabilities m '[MonadState Bool m, MonadIO m, Monad m]
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