在自动定理证明（证明搜索）中，我组合了以下类型的变换器
t :: Claim -> IO (Maybe (Claim, Proof -> Proof))
这样：当t c返回时Just (c', f)，则c'隐含c，并且从计算的证明中c获得证明。p'c'f p'
这是一个镜头，不知何故？（如果是，有什么帮助？）
还有一个更一般的情况（对于几个或零个子目标）
ts :: Claim -> IO (Maybe ([Claim], [Proof] -> Proof))
这IO部分很重要，因为这些转换器做了大量工作（调用外部进程），我可能想强制超时。
我不能轻易看出镜头如何帮助解决这个问题。但是，重新排序您的 monad 堆栈并使用 monad 转换器应该使组合更容易，并且还开辟了在IO不需要杂质的情况下进行抽象的可能性：
t' :: Claim -> MaybeT IO (Claim, Proof -> Proof)
如果您想要或需要继续使用现有的实现，t尽管类型更繁琐，您可以将其结果提升为MaybeT：
(MaybeT . return =<<) . lift :: m (Maybe b) -> MaybeT m b
值得注意的是，Claim -> (Claim, Proof -> Proof)它等价于State Claim (Proof -> Proof)，因此可能会走得更远：
t'' :: StateT Claim (MaybeT IO) (Proof -> Proof)