一个MonadTransformer到类型检查了已经完成的动作

Question

序言

这是那些我认为，有人已经解决了我的问题的问题之一，但我不知道去哪里找。

问题

我要找携带的是这样的单子堆栈的操作将无法进行类型检查，除非它是完整的完全或不完全的想法MonadTransformer。

我的情况

我有一个单子与持有兆乏的状态叠加。未能写入此MVar将导致thread blocked indefinitely in an MVar异常。我可以检查MVar本身，但将它交给另一个线程（遵循相同的规则）也是获得MVar填充的有效方法（正如抛出一个错误）。

我正在寻找某种方式让typechecker抛出一个错误，如果其中一个条件没有被monad运行时所满足。我可以在运行时检查，但我认为可能有一种使用类型系统的方法。

Answer 1

听起来像某种indexed monad可能有所帮助。索引monad允许或禁止某些类型级别的操作。

---

我们还可以依靠多态性

{-# 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) 

的想法是，EnsuredWrite类型的动作需要返回token值，但只知道如何通过Gulp喂养函数产生一个。如果他们回来了，他们一定会调用这个功能。

令牌的实际类型并不重要，它可以是一个简单的()。但EnsuredWrite行动不应该知道，因此forall。

虽然这个解决方案并不禁止重复写入。