haskell - 用于对已完成操作进行类型检查的 Monad Transformer

Question

序言

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

问题

我正在寻找一个 MonadTransformer，它带有完整或不完整的想法，这样 monad 堆栈的操作将无法进行类型检查，除非它是完整的。

我的情况

我有一个 Monad 堆栈，其状态包含一个 MVar。无法写入此 MVar 将导致 thread blocked indefinitely in an MVar异常(exception)。我可以只检查 MVar 本身，但将其交给另一个线程(遵循相同的规则)也是填充 MVar 的有效方法(就像抛出错误一样)。

我正在寻找某种方法，让类型检查器在 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 中的函数来生成一个值。如果它们最终返回，则它们一定调用了该函数。

token 的实际类型并不重要，它可以是一个简单的 () 。但是EnsuredWrite操作不应该知道这一点，因此 forall .

不过，此解决方案并不禁止重复写入。