Effects, Capabilities, and Boxes

• Website
• Authors:
  • Jonathan Immanuel Brachthäuser
  • Philipp Schuster
  • Edward Lee
  • Aleksander Boruch-Gruszecki

This paper introduces System C, which is inspired by System Ξ from the paper Recovering Purity with Comonads and Capabilities. The basic idea is that we want to be able to reason about effects at the type level when closing over an environment, but also to not need to manually track the effect types when they’re available in the encoring environment.

The problem is that these two methods of reasoning are at odds:

• Type based reasoning is explicit, but flexible
  • You can safely return typed capabilities around as values
  • A bit of a PITA to track and/or polymorphise things that are obviously in scope
• Scope-based reasoning is implicit but dangerous
  • i.e. How to avoid accidentally leaking capabilities?

The approach — adapted from Recovering Purity with Comonads and Capabilities — is to introduce a concept of “boxing”: capturing the capabilities in scope as a value which can be passed around and returned from a function.

Analogy to RIO

RIO’s core type looks like this:

newtype RIO env a = ReaderT env (IO a)

The idea is that if you operate in RIO, you can get good performance and perform all of the actions that you would need from more complicated types by putting handlers in the env.

It’s not a perfect analogy to this paper, because you still need to do all of the monadic wrapping/unwrapping, but I think that you can get pretty close! Here’s some pseudocode:

module Control.Monad.EffCap 
  ( EffCap,
  , MsgCap (..)
  ) where
 
import Data.Has
import RIO
 
-- Avoid adding a MonadIO instance!
newtype EffCap env a = EffCap {uncap :: RIO env a}
  deriving newtype
    ( Functor
    , Applicative
    , Monad
    , MonadReader env
    , HasStateRef s env => MonadState s
    -- ...
    )
 
-- Not exported, since caps have no introduction rule
sendIO :: IO a -> EffCap env a
sendIO = EffCap . liftIO
 
box :: EffCap env env
box = ask
 
unbox :: env -> EffCap env a -> EffCap env a
unbox env action = local (const env) action
 
-------------
-- Example --
-------------
 
newtype SendMsgCap = SendMsgCap (Text -> IO ())
newtype GetMsgCap  = GetMsgCap  (IO Text)
 
-- Monomorphic for simplicity,
-- but we could always get polymorohic gere
data Messenger = Messenger
  { send :: SendMsgCap
  , get  :: GetMsgCap
  }
 
sendMsg :: Has SendMsgCap env => Text -> EffCap env ()
sendMsg txt = do
  handler <- asks sendMsg
  sendIO $ handler txt
 
getMsg :: Has SendMsgCap env => Text -> EffCap env Text
getMsg = asks getMsg >>= sendIO
 
-----------------
-- Scope Based --
-----------------
 
-- Contains *at least* MsgCap
scopeToType :: Has GetMsgCap env => EffCap env (Text, env)
scopeToType = do
  msg <- getMsg
  env <- box
  (msg, env)
 
----------------
-- Type Based --
----------------
 
-- Contains *exactly* MsgCap
typed :: Messenger -> Text -> Text
typed caps txt = do
  inbound <- caps.getMsg
  let shout = upcase inbound
  
  unbox caps do
    sendMsg shout
    (msg, _) <- scopeToType
    return msg