提升内部延续

Question

我有 type 的延续(a -> b) -> b。我还有一个“几乎”适合上下文的函数，类型为Monad m => a -> m b。有没有办法将延续升级(a -> b) -> b为(a -> m b) -> m b？我的直觉是不，但我想在这方面是错误的。

Answer 1

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

假设 monadm是延续 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。