这是不是类似于一个镜头？（证明搜索变换器/组合器）

Question

在自动定理证明（证明搜索）中，我组成了类型的转化器。

t :: Claim -> IO (Maybe (Claim, Proof -> Proof))

这里的意思是：当 t c 返回 Just (c', f) 时，c' 意味着 c，并且可以通过计算 f p' 来从证明 p' 获得证明 c。

这是一个镜头吗？（如果是，它有什么帮助吗？）

还有一个更一般的情况（适用于多个或零个子目标）

ts :: Claim -> IO (Maybe ([Claim], [Proof] -> Proof))

IO 部分非常重要，因为这些转换器会执行大量的工作（调用外部进程），我可能需要设置超时。

- d8d0d65b3f7cf42

Answer 1

我无法立即看出透镜可以如何帮助解决这个问题。然而，重新排列您的单子栈并使用单子变换器应该会使组合更容易，并且还可以打开在不需要杂质的情况下从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)

- duplode