MonadTransformer for typecheck for completed action
Preamble
This is one of those questions where I think someone has already solved my problem, but I don't know where to look.
Question
I'm looking for a MonadTransformer that carries the idea of being complete or incomplete in such a way that the monad's stack action won't be checked if it doesn't complete.
My situation
I have a stateful Monad stack that contains MVar. Failure to comply with this MVar will result in an exception thread blocked indefinitely in an MVar
. I could just test the MVar myself, but passing it to another thread (which follows the same rules) is also a valid way to populate the MVar (as the error does).
I'm looking for a way to get typechecker to throw an error if one of these conditions is not met by the time the monad starts. I can check at runtime, but I think there might be a way to use the type system.
source to share
Sounds like an indexed monad . Indexed monads allow or deny certain operations according to some level of type state.
We could also rely on polymorphism:
{-# language RankNTypes #-}
import Control.Monad
import Control.Monad.Trans.State
-- Receives an v and returns a "proof" token
newtype Gulp token v = Gulp (v -> IO token)
-- Computation polymorphic on the token
type EnsuredWrite v r = forall token. StateT (Gulp token v) IO (token,r)
The idea is that actions of the type EnsuredWrite
should return a value token
, but only know how to create it by feeding a function to Gulp
. If they return at all, they should have called this function.
The actual token type is not important, it can be simple ()
. But actions EnsuredWrite
do not have to know, therefore forall
.
This solution does not prohibit rewriting.
source to share