haskell - 如何让 callCC 更有活力？

Question

我认为 ContT 的正确类型应该是

newtype ContT m a = ContT {runContT :: forall r. (a -> m r) -> m r}

和其他控制运算符

shift :: Monad m => (forall r. (a -> ContT m r) -> ContT m r) -> ContT m a
reset :: Monad m => ContT m a -> ContT m a
callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a

不幸的是，我做不到 callCC类型检查，不知道怎么做。
我设法使 shift和 reset类型检查

reset :: Monad m => ContT m a -> ContT m a
reset e = ContT $ \ k -> runContT e return >>= k

shift :: Monad m => (forall r. (a -> ContT m r) -> ContT m r) -> ContT m a
shift e = ContT $ \ (k :: a -> m r) ->
    runContT ((e $ \ v -> ContT $ \c -> k v >>= c) :: ContT m r) return

但是，我仍然无法使用 shift和 reset在这样的递归跳跃中？

newtype H r m = H (H r m -> ContT m r)

unH (H x) = x

test = flip runContT return $ reset $ do
    jump <- shift (\f -> f (H f))
    lift . print $ "hello"
    unH jump jump

有没有人试过这个？

Answer 1

你愿意play a game ?

今天，你成为 callCC .

callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
--                                       you are here ^^

该功能箭头左侧的所有内容都是您的对手所做的 Action 。箭头右侧是游戏结束。要获胜，您必须仅使用对手提供的棋子构建与右侧匹配的东西。

幸运的是，您在某些问题上仍有发言权。看到这里的箭头了吗？

callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
--                this is your opponent ^^

当您收到本身包含箭头的东西时，左侧的所有内容都代表您要进行的 Action ，右侧的部分代表该游戏分支的结尾，为您提供另一个可以用作(希望)的部分制胜策略。

在我们进一步讨论之前，让我们简化一些事情: monad 转换器方面只是一种干扰，所以丢弃它；并为每个类型变量添加显式量词。

callCC :: forall a. ((a -> (forall b. Cont b)) -> Cont a) -> Cont a

现在，想想像 forall a. ... 这样的类型总数是。如果你用这样的类型产生一些东西，你是说你可以为任何类型提供一个值 a任何。如果您收到具有此类类型的内容，则可以选择要使用的特定类型。将其与 A -> ... 之类的类型进行比较对于单态函数；生成这样的函数表示您知道如何为 A 类型的任何值提供结果。 , 而接收这样的函数让你选择一个特定的值 A使用。这似乎与 forall 的情况相同，实际上平行成立。所以，我们可以对待 forall表示您或您的对手可以使用类型而不是术语的移动。为了反射(reflect)这一点，我将滥用符号并写成 forall a. ...如 a => ;然后我们可以像 (->) 一样对待它除了它必须出现在被绑定(bind)的类型变量的任何使用的左侧。

我们还可以注意到，唯一可以直接使用 Cont a 类型的值来完成的事情。正在申请 runCont到它。所以我们会提前这样做，并将所有相关的量词直接嵌入到 callCC 的类型中。 .

callCC :: a => ( (a -> (b => (r1 => (b -> r1) -> r1))) 
               -> (r2 => (a -> r2) -> r2)
               ) -> (r3 => (a -> r3) -> r3)

因为我们能够治疗 forall就像其他函数箭头一样，我们可以重新排序并删除多余的括号以整理一些东西。特别要注意的是 callCC事实证明，这实际上并不是游戏的结束；我们必须提供一个函数，这相当于提供另一个游戏，我们再次扮演最右边箭头的角色。所以我们可以通过合并这些来节省一步。我还将向左 float 类型参数，以将它们全部放在一处。

callCC :: a => r3 => (a -> r3) 
       -> (r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2) 
       -> r3

所以……我们的举动。

我们需要 r3 类型的东西.我们的对手已经采取了四次行动，我们已将其作为参数接收。一招就是选择 r3 ，所以我们已经处于劣势了。另一个举动是 a -> r3 ，这意味着如果我们可以玩一个 a ，我们的对手会吐出 r3我们可以滑向胜利。不幸的是，我们的对手也打了 a ，所以我们又回到了起点。我们要么需要 a 类型的东西，或其他方式来获得 r3 类型的东西.

我们对手的最后一步更复杂，所以我们将单独研究它:

r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2

请记住，这是他们做出的举动。所以这里最右边的箭头代表我们的对手，左边的一切代表我们可以采取的行动类型。这样做的结果是 r2 类型的东西，其中 r2是我们可以玩的东西。很明显，我们需要播放 r3或 a取得任何进展。

正在播放 a :如果我们玩 a如 r2 ，那么我们就可以玩 id如 a -> r2 .另一个 Action 更复杂，所以我们会跳进去。

b => r1 => a -> (b -> r1) -> r1

回到代表我们的最右边的箭头。这次我们需要生产 r1 类型的东西，其中 r1是对手的举动。他们还发挥了作用 b -> r1 ，其中类型 b也是他们的举动。所以我们需要任何一种类型的东西 b或 r1从他们。不幸的是，他们给我们的只是 a 类型的东西。 ，让我们处于无法取胜的境地。猜猜玩 a早些时候是一个糟糕的选择。让我们再试一次...

正在播放 r3 :如果我们玩 r3如 r2 ，我们还需要发挥一个功能 a -> r3 ;好在对方已经发挥了这样的功能，所以我们可以简单地使用它。我们再次跳入另一个 Action :

b => r1 => a -> (b -> r1) -> r1

……才发现，这和之前的情况完全一样，不可能。任凭对手选择 r1不要求它们提供一种构建方法让我们陷入困境。

也许一些诡计会有所帮助？

打破规则——玩r1 :

我们知道，在常规 Haskell 中，我们可以依靠懒惰来扭转局面，让计算吞下自己的尾部。不用太担心如何做，让我们想象一下我们可以在这里做同样的事情——以 r1 为例。我们的对手在内部游戏中玩，然后将其拉出并返回以将其玩为 r2 .

再次，这是对手的举动:

r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2

在我们打结的恶作剧之后，它最终相当于:

(b => a -> (b -> r1) -> r1) -> (a -> r1) -> r1

由于我们的诡计，类型参数已经消失了，但是 r1还是被对手选中。因此，我们在这里所做的只是洗牌；显然，我们甚至无法希望获得 a或 r3因此，我们又走到了另一个死胡同。

所以我们做了最后的、绝望的尝试:

打破规则——玩b :

这次我们走的是 b由对手在最里面的游戏中玩，然后循环播放作为 r2 .现在对手的 Action 是这样的:

(r1 => a -> (b -> r1) -> r1) -> (a -> b) -> b

然后回到内部游戏:

r1 => a -> (b -> r1) -> r1

继续诡计，我们可以扭曲 b上面的结果也是如此，给函数 b -> r1 , 收到 r1我们需要。成功!

退一步，我们还剩下一个问题。我们必须玩 a -> b 类型的游戏.没有明显的方法可以找到，但我们已经有了 b躺着，所以我们可以使用 const在那丢弃 a和 -

- 可是等等。 b 类型的值在哪里？首先来自哪里？暂时把自己放在对手的位置上，他们唯一能得到的地方是我们采取的行动的结果。如果只有 b我们拥有的是他们给我们的，我们最终会兜兜转转；游戏永远不会结束。

所以，在 callCC的游戏中，我们唯一的策略要么导致亏损，要么导致永久僵局。

callCC :: forall a. ((a -> (forall b . Cont b)) -> Cont a) -> Cont a
callCC = error "A strange game..."

唉，看来唯一的胜利之举就是不玩了。