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 typesafe 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/orIxMonadThrow
/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 typesafe web server that is backendindependent. 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 backendindependent 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 backendindependent 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 `purescriptindexedmonad`
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 capabilitybased 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 capabilitybased 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 purescripttransformers
. I’ve created a branch showing just that in my fork’s indexedtransformers
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 enduser 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
IxMonadError
computations  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/orIxMonadThrow
/IxMonadError
to get around the type unification errors described above?