Black Shell

We are adding a Black Shell to HERMIT. Rather than use the bash-style, string based, dynamically typed prompt, we can run GHCi within HERMIT.

GHCi> perform :: (Perform p) => p -> IO ()

Examples

GHCi> perform display
GHCi> perform betaRewrite

Local Types

Every HERMIT type has a local reflection, as needed, that is actually a JSON Value inside. A problem with this, vs overloading, is we need to write down each primitive twice. It turns out that the primitives in the black shell tend to have higher-level types that their KURE/HERMIT primitives.

newtype RewriteH :: * -> * where
  RewriteH :: Value -> RewriteH a

newtype TransformH :: * -> * -> * where
  TransformH :: Value -> TransformH a

betaReduce :: RewriteH Core
betaReduce = RewriteH (prim 'HERMIT.Dictionary.Local.betaReduce [])

prim :: Name -> [Value] -> Value

Remote Types

We have a union type of all black shell effects, and a perform function, that does them.

data TypedEffectH :: * -> * where
  ShellEffectH           :: ShellEffect                         -> TypedEffectH ()
  RewriteLCoreH          :: RewriteH LCore                      -> TypedEffectH ()
  RewriteLCoreTCH        :: RewriteH LCoreTC                    -> TypedEffectH ()
  TransformLCorePathH    :: TransformH LCore LocalPathH         -> TypedEffectH ()

performTypedEffectH :: (MonadCatch m, CLMonad m) => TypedEffectH a -> m a

For now, all effects return (), but later we will have the transforms return the results of queries, so that the local black shell can use them.