haskell - 这是像镜头一样的东西吗？ (证明搜索变压器/组合器)

Question

在自动定理证明(证明搜索)中，我编写了类型的变压器

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

使得:当t c返回Just (c', f)时，则c'意味着c c 的证明是通过计算 f p' 从 c' 的证明 p' 获得的。

这是一个镜头吗？ (如果是的话，有什么帮助？)

还有一个更一般的情况(对于多个或零个子目标)

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

IO 部分很重要，因为这些转换器做了大量工作(调用外部进程)，并且我可能想施加超时。

Answer 1

我无法轻易看出镜头如何帮助解决这个问题。但是，重新排序您的单子(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)