Exploration - Indexed Capability Design Pattern with Indexed Monad Transformers

#1

This post is an explanation of an idea I have that ends with “Is this a good idea? If so, how could I attempt to resolve this problem?” I’ll explain the gist of it before overviewing the idea and resulting problem I’m having right now.

Two Minute Summary

To write type-safe code, I want to use this monad stack (read from bottom to top):

Layer What it does
Indexed Monad Transformers
(e.g. IxMonadState)
adds functionality to NodeServer
Indexed Capability Design Pattern
(e.g. NodeServer)
uses the capability design pattern to limit the possible index changes via the Response type class’ functions
Indexed adds indices to the underlying monad and provide default implementation of IxMonad type class hierarchy
Monad Transformers
(e.g. ReaderT)
makes it possible for NodeServer to implement the Response type class’ functions
Effect/Aff runs the code

ReaderT, StateT, and WriterT (not sure about ListT yet) and their respective type classes all have a valid indexed version. MonadThrow and MonadError have a valid indexed version, too. However, ExceptT and MaybeT can’t define a valid IxBind instance because there are two possible computation paths. The use of ibind in one path and ipure in another will lead to a type unification error.

Concluding questions:

  • If it can compile successfully, what costs would this monad stack incur (e.g verbosity, performance, etc.)?
  • Is there a different way to define IxExceptT and/or IxMonadThrow/IxMonadError to get around the type unification errors described below?

Quick Overview of Hyper

For the past two months, I’ve been playing around with hyper, an experimental type-safe web server that is backend-independent. Hyper uses indexed monads to ensure that developers write to an HTTP response in the correct order–first the status line, then the headers, then the body, then one indicates that the connection is finished. Failing to write the monadic code in the correct order results in a compiler error.

Right now, hyper uses Middleware, a variant of StateT, to get the necessary “shape” of an indexed monad, m x y a:

newtype StateT     monad state        a = StateT     (state -> monad (Tuple a state ))
newtype Middleware monad input output a = Middleware (input -> monad (Tuple a output))

Since Middleware is a variant of the state monad, its input/output/state is Conn, a backend-independent way to model an HTTP connection. Conn includes a phantom type via responseState, which is the actual index in the indexed monad, Middleware.

type Conn request response responseState components =
  { request: request
  , respones: response
  , components: components -- extensibility point
  }

In addition, there is a type class for creating an HTTP response in a backend-independent manner. It’s called Response and controls how the index changes:

class Response m body | m -> body where
  writeStatus
    :: forall request response components
     . Status
    -> m
        (Conn request response StatusLineOpen components)
        (Conn request response HeadersOpen components)
        Unit
  writeHeader
    :: forall request response components
     . Header
    -> m
        (Conn request response HeadersOpen components)
        (Conn request response HeadersOpen components)
        Unit
  closeHeaders
    :: forall request response components
     . m
        (Conn request response HeadersOpen components)
        (Conn request response BodyOpen components)
        Unit
  send
    :: forall request response components
     . body
    -> m
        (Conn request response BodyOpen components)
        (Conn request response BodyOpen components)
        Unit
  end
    :: forall request response components
     . m
        (Conn request response BodyOpen components)
        (Conn request response ResponseEnded components)
        Unit

The Indexed Capability Design Pattern

As I looked at how the library worked, it reminded me of the Capability Design Pattern. Below is the same code except it removes the indices and components part of the Conn type:

newtype Conn request response = { request :: request, response :: response }
newtype NodeServer m a = NodeServer (ReaderT (Conn HttpRequest HttpResponse) m a)

class Response m body | m -> body where
  writeStatus :: Status -> m Unit
  writeHeader :: Header -> m Unit
  closeHeaders :: m Unit
  send :: body -> m Unit
  end :: m Unit

instance responseNodeServer :: (MonadEffect m) => Response (NodeServer m) body where
  writeStatus :: Status -> NodeServer m Unit
  writeStatus status = NodeServer do
    { response } <- ask
    liftEffect (writeStatus status response)

  writeHeader :: Header -> NodeServer m Unit
  writeHeader header = NodeServer do
    { response } <- ask
    liftEffect (writeheader header response)

  closeHeaders :: NodeServer m Unit
  closeHeaders = NodeServer (pure unit)

  send :: body -> NodeServer m Unit
  send body = NodeServer do
    { response } <- ask
    liftEffect (writeBodyPart body response)

  end :: NodeServer m Unit
  end = NodeServer do
    { response } <- ask
    liftEffect (endStream response)

If we were to add the indices back into the above code, this is how it might look:

-- A newtype that adds indices (i.e. `x` and `y`) to a monad.
-- It also implements instances for the `IxMonad` type class hierarchy.
-- This is defined in `purescript-indexed-monad`
newtype Indexed m x y a = Indexed (m a)

newtype Conn request response = { request :: request, response :: response }

newtype NodeServer m x y a = NodeServer (Indexed (ReaderT (Conn HttpRequest HttpResponse) m) x y a)

-- not shown here but we would derive the 
-- `IxMonad` type class hierarchy via Indexed's instances

-- Something like this function would be used in the real implementation.
runNodeServer
  :: forall m a. Monad m =>
     NodeServer m StatusLineOpen ResponseEnded a ->
     Conn HttpRequest HttpResponse ->
     m a
runNodeServer (NodeServer (Indexed m)) conn = runReaderT m conn

class IxMonad m <= Response m body | m -> body where
  writeStatus :: Status -> m StatusLineOpen HeadersOpen Unit
  writeHeader :: Header -> m HeadersOpen HeadersOpen Unit
  closeHeaders :: m HeadersOpen BodysOpen Unit
  send :: body -> m BodysOpen BodysOpen Unit
  end :: m BodysOpen ResponseEnded Unit

instance responseNodeServer :: (MonadEffect m) <= Response (NodeServer m) body where
  writeStatus :: Status -> NodeServer m StatusLineOpen HeadersOpen Unit
  writeStatus status = NodeServer $ Indexed do
    { response } <- ask
    liftEffect (writeStatus status response)

  writeHeader :: Header -> NodeServer m HeadersOpen HeadersOpen Unit
  writeHeader header = NodeServer $ Indexed do
    { response } <- ask
    liftEffect (writeheader header response)

  closeHeaders :: NodeServer m HeadersOpen BodysOpen Unit
  closeHeaders = NodeServer $ Indexed (pure unit)

  send :: body -> NodeServer m BodysOpen BodysOpen Unit
  send body = NodeServer $ Indexed do
    { response } <- ask
    liftEffect (writeBodyPart body response)

  end :: NodeServer m BodysOpen ResponseEnded Unit
  end = NodeServer $ Indexed do
    { response } <- ask
    liftEffect (endStream response)

If we do not export NodeServer's constructor, then developers are forced to use the functions defined in Response to transition the index from one state to another. If it was exported, developers could define their own function that has a type signature, allowing an invalid transition. For example

-- allows us to rebind do notation from `bind` to `ibind`
import Control.Monad.Indexed.Qualified as Ix

resetToStatusLine :: forall m. Monad m => NodeServer m ResponseEnded StatusLineOpen Unit
resetToStatusLine = NodeServer $ Indexed (pure unit)

invalidTransition :: forall m. Monad m => NodeServer m StatusLineOpen ResponseEnded Unit
invalidTransition = Ix.do
  writeStatus status
  writeHeader header
  closeHeaders
  send body
  end

  -- At this point, the response is finished.
  -- However our function's type signature resets
  -- the index of the computation. Thus, the compiler
  -- would not produce an error when it should.
  resetToStatusLine

  writeStatus status2
  writeHeader header2
  closeHeaders
  send body2
  end

Using the Indexed Capability Design Pattern, our stack (from bottom to top) looks like this:

Layer What it does
Indexed Capability Design Pattern
(e.g. NodeServer)
uses the capability design pattern to limit the possible index changes via the Response type class’ functions
Indexed adds indices to the underlying monad and provide default implementation of IxMonad type class hierarchy
Monad Transformers
(e.g. ReaderT)
makes it possible for NodeServer to implement the Response type class’ functions
Effect/Aff runs the code

While we can run type safe computations now, the next problem we have is adding in effects like state manipulation. So, how would one use monad transformers to further enhance the logic? We would need to add Indexed Monad Transformers.

Indexed Monad Transformers: Two Possible Definitions

Before continuing, we need to clarify what is meant by ‘indexed monad transformers.’ Let’s give two examples of what we could mean by using an indexed version of MonadState, IxMonadState1 and IxMonadState2:

class Monad m <= MonadState s m | m -> s where
  state :: forall a. (s -> Tuple a s) -> m a

-- notice that the index, `x`, remains unchanged
class IxMonad m <= IxMonadState1 s m | m -> s where
  istate1 :: forall a. (s -> Tuple a s) -> m x x a

-- notice the index changes from `x` to `y`
class IxMonad m <= IxMonadState2 s m | m -> s where
  istate2 :: forall a. (s -> Tuple a s) -> m x y a

Since our capability-based type classes define how the index can change, we don’t need IxMonadState2 to account for that possibilty. Rather, it makes more sense to use IxMonadState1: the index should not change when we do a state manipulation because it should only change if we use a function from one of our capability-based type classes. If we don’t use the Indexed Capability Design Pattern, then IxMonadState2 is the only other logical possibility. (Note: one usually breaks IxMonadState2's istate2 down into get :: m x x a and put :: m x y a. Otherwise, a get could change the index when that doesn’t make any sense)

By using this first definition, we can define an indexed version of all the transformer type classes found in purescript-transformers. I’ve created a branch showing just that in my fork’s indexed-transformers branch.

Moreover, we can define indexed versions of ReaderT, StateT, WriterT, and RWST. However, a problem arises with ExceptT and MaybeT. I don’t know whether the below problem also occurs with ListT because I haven’t tried to implement it yet.

The Problem: Defining an IxBind instance for IxExceptT and IxMaybeT

If we look at IxBind, we see that ibind changes the index from x to y.

class IxApply m ⇐ IxBind m where
  ibind ∷ ∀ a b x y z. m x y a → (a → m y z b) → m x z b

In contrast, ipure from IxApplicative ensures that the index, x, does not change:

class IxApply m ⇐ IxApplicative m where
  ipure ∷ ∀ a x. a → m x x a

The problem arises when we wish to combine these two in a situation where there are two possible computation paths (e.g. failure can occur), such as defining an IxBind instance for IxExceptT. To help show why the compiler produces the error that follows this code, the type signature of result is made explicit:

newtype IxExceptT e m x y a = IxExceptT (m x y (Either e a))

instance bindIxExceptT :: IxMonad m => IxBind (IxExceptT e m) where
  ibind ∷ ∀ a b x y z. IxExceptT e m x y a → (a → IxExceptT e m y z b) → IxExceptT e m x z b
  ibind (IxExceptT m) k = IxExceptT Ix.do
    result <- m
    case result of
      Left e ->
        let
          -- the second 'y' is not a 'z' here
          result :: m y y b
          result = ipure e
        in
          result
      Right a -> case k a of IxExceptT b ->
        let
          -- since the compiler inferred via `ipure` that the result
          -- should be `m y y b`, it thinks `b` is the problem.
          -- However, the problem is that `ipure` doesn't produce
          -- an `m y z b` value, which matches the type 
          -- signature defined by `ibind`
          result :: m y z b
          result = b
        in
          result

Thus, the compiler reports:

Could not match type

    z4

  with type

    y1


while trying to match type m0 y1 z4
  with type m0 y1 y1
while checking that expression b
  has type m0 y1 t2 t3
in value declaration bindIxExceptT

where m0 is a rigid type variable
        bound at (line 0, column 0 - line 0, column 0)
      z4 is a rigid type variable
        bound at (line 0, column 0 - line 0, column 0)
      y1 is a rigid type variable
        bound at (line 0, column 0 - line 0, column 0)
      t2 is an unknown type
      t3 is an unknown type

Why is that a problem?

We can still implement an instance for IxMonadThrow and IxMonadError if we delegate that instance to a monad that occurs before we impose the indices on our monad.

instance ixMonadThrow :: MonadThrow e m => IxMonadThrow e (NodeServer m) where
  ithrowError e = NodeServer $ Indexed (throwError e)

However, this solution is problematic because we lose the guarantees of an indexed monad. If we update the Monad Transformer layer in our stack to include an ExceptT

Layer What it does
Indexed Monad Transformers adds functionality to NodeServer
Indexed Capability Design Pattern
(e.g. NodeServer)
uses the capability design pattern to limit the possible index changes to the Response type class’ functions
Indexed adds indices to the underlying monad and provide default implementation of IxMonad type class hierarchy
Monad Transformers
(e.g. ExceptT)
makes it possible for NodeServer to implement the Response type class’ functions
Effect/Aff runs the code

Then we must let the user provide a way to implement the resulting MonadThrow type class. While most would implement it via runExceptT

runExceptT (runNodeServer monadicCode conn)

… the problem is that an end-user could substitute runExceptT with something that subjugates the guarantees provided by the index change, thereby allowing an invalid state to occur in the computation.

We could get around this problem if we changed NodeServer to include ExceptT in its implementation stack. However, this creates an unnecessary performance cost for those who don’t need that in their server or only need it at various parts in their server.

Unless we can find a way solve this problem, we are stuck with these tradeoffs:

  1. keep the type guarantees of indexed monads and lose the ability to run any IxMonadError computations
  2. gain the abilty to use IxMonadError computations but risk the type guarantees of indexed monads and (possibly?) incur the performance cost of including the unindexed monad transformer.

Remaining Questions

  • If this could compile successfully, what costs would this monad stack incur (e.g verbosity, performance, etc.)?
  • Is there a different way to define IxExceptT and/or IxMonadThrow/IxMonadError to get around the type unification errors described above?
3 Likes
#2

I think the solution to this might be to define a Monad instance for NodeServer, define business logic in separate functions using type classes, and then run them inside the main computation via run<transformer> functions. However, if we must do it that way for ExceptT and MaybeT (see exceptionalCode, then we might as well do it for the other transformers as well (see computation):

serve :: m StatusLineOpen ResponseEnded
serve = Ix.do
  reqData <- getRequestData
  reqBody <- readBody
  someComp <- runExceptT exceptionalCode
  someOtherComp <- runReaderT (runStateT computation 5) reqBody)
  -- rest of http response creation code

  where
  exceptionalCode :: forall m.
                     MonadError String m =>
                     m Int
  exceptionalCode = do
    x <- doX
    y <- doY
    z <- doZ `catchError` doZ'
    pure (x <> y <> z)

  computation :: forall m. 
                 MonadAsk RequestData m => 
                 MonadState Int m => 
                 m String
  computation = do
   reqData <- ask
   -- rest of code...
   pure "The answer is 42"