haskell - 提升内部延续

Question

我有 type 的延续(a -> b) -> b。我还有一个函数“几乎”是一个合适的上下文，带有 type Monad m => a -> m b。有没有办法将 continuation 从 升级(a -> b) -> b到(a -> m b) -> m b？我的直觉是否定的，但我想在这件事上是错的。

标签： haskellfunctional-programming

Answer 1

这确实是不可能的，至少在m可以是任意单子的一般情况下。

假设 monadm是 continuation monad (- -> r) -> r。（为了清楚起见，我省略了newtype包装）。

然后，您想要的是一种转换(a -> b) -> b为(a -> (b -> r) -> r) -> (b -> r) -> r. 换句话说，你想要一个类型的多态项

t :: ((a -> b) -> b) -> (a -> (b -> r) -> r) -> (b -> r) -> r

我们证明t矛盾不能存在。让我们假设这样一个t存在。我们可以通过选择r~a和b~Void（空类型）来专门化它。

t :: ((a -> Void) -> Void) -> (a -> (Void -> a) -> a) -> (Void -> a) -> a

现在，回想一下，我们有一个（总计！）函数absurd :: Void -> a（本质上是absurd x = case x of {}）。然后我们得到

\ x -> t x (\y _ -> y) absurd
:: ((a -> Void) -> Void) -> a

通过Curry-Howard 同构，以下将是直觉逻辑中的逻辑重言式：

((A -> False) -> False) -> A

但是上面的公式是Not (Not A) -> A，即双重否定消除，这在直觉逻辑中是不可能证明的。因此，我们得到一个矛盾，我们必须得出结论，没有t这种类型的术语。

请注意，t其他 monad 可能存在m。