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
IxExceptTand/orIxMonadThrow/IxMonadErrorto 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:
- keep the type guarantees of indexed monads and lose the ability to run any
IxMonadErrorcomputations - gain the abilty to use
IxMonadErrorcomputations 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
IxExceptTand/orIxMonadThrow/IxMonadErrorto get around the type unification errors described above?