haskell - 提升内部延续

Question

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

Answer 1

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

假设单子(monad) m是延续单子(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 isomorphism以下将是直觉逻辑中的逻辑重言式:

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

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

请注意 t可能存在于其他单子(monad) m .