haskell - 这像镜头吗？ (安全搜索变压器/组合器)

在自动定理证明（证明搜索）中，我组成了

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部分很重要，因为这些转换器会做大量工作（称为外部进程），并且我可能要施加超时。

最佳答案

我无法轻易地看到镜头如何帮助实现这一目标。但是，对monadic堆栈进行重新排序并使用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)