如何使callCC更具动态性？ [英] How to make callCC more dynamic?

问题描述

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

  newtype ContT m a = ContT {runContT :: forall r。 （a  - > m r） - > mr} 
  

和其他控制操作符

  shift :: Monad m => （全部（a→ContT m r）→ContT m r）→> ContT m a 
 reset :: Monad m => ContT m a  - > （a  - >（所有r.ContrT m r）） - > ContT m a） - > ContT ma 
  

不幸的是，我无法使 callCC 类型检查，并不知道如何去做。
我设法让转移和重置类型检查

  reset :: Monad m => ContT m a  - > ContT m a 
 reset e = ContT $ \ k  - > runContT e return>> = k 
 
 shift：Monad m => （全部（a→ContT m r）→ContT m r）→> ContT m a 
 shift e = ContT $（k :: a  - > m r） - > 
 runContT（（e $ \ v  - > ContT $ \c-> kv>> = c）:: ContT mr）return 
  pre> 
 
 
但仍然不能使用 shift 和 reset  
 
  newtype H rm = H（H rm  - > ContT mr）
 
 unH（H x）= x 
 
 test = flip runContT return $ reset $ do 
 jump<  -  shift（\f  - > f（H f） ）
升。打印$hello
 unH跳跃
  
有没有人尝试过？
解决方案
您想玩游戏？
 
 
 
今天，您将获得 callCC 。
 
 
 
 $ b 
  callCC ::（（a  - >（forall r。ContT mr ）） - > ContT ma） - > ContT ma 
  - 你在这里^^ 
  

该函数左侧的所有内容arrow是你的对手所做的动作。箭头右侧是游戏结束。要赢得比赛，你必须只使用你的对手所提供的棋子构建与右侧相匹配的东西。



幸运的是，你仍然有一些事情要说。在这里看到这个箭头？

callCC ::（（a - >（forall r。ContT mr）） - > ContT ma） - > ContT ma
- 这是你的对手^^


当你收到本身包含的东西一个箭头，左边的所有内容代表您正在制作的动作 ，以及右边那个游戏分支的结尾部分，为您提供另一个可用的部分作为你的（有希望的）获胜策略的一部分。

在我们进一步讨论之前，让我们简化几件事情：单变换器方面仅仅是一种分心，并为每个类型变量添加显式量词。

$ b

  callCC :: forall a。 （（a  - >（全部b.Conb）） - > Cont a） - >继续阅读
  

现在，考虑像这样的类型。 ... 等于。如果你用这种类型的东西产生东西，你可以说任何类型的 a 都可以提供值。如果您使用类似的类型接收，您可以选择要使用的特定类型。将它与 A - > ... 为单形函数;产生这样一个函数说，你知道如何为 A 类型的任何值提供一个结果，而接收这样的函数可以让你选择一个特定的值一个来使用。这似乎与 forall 的情况相同，实际上并行保持。因此，我们可以将 forall 视为指示您或您的对手玩起了类型而不是术语的移动。为了反映这一点，我会滥用记谱法并写 forall a。 ... 为 a => ;我们可以像（ - >）一样对待它，除非它必须出现在被绑定的类型变量的任何使用的左边。

我们还可以注意到，可以直接使用 Cont a 类型值的唯一方法是应用 runCont 就可以了。因此，我们将提前做到这一点，并将所有相关量词直接嵌入 callCC 类型。

  callCC :: a => （a  - >（b =>（r1 =>（b→r1）→r1）））
  - >（r2 =>（a  - > r2） - > r2）
） - > （r3 =>（a  - > r3） - > r3）
  

因为我们能够像对待其他功能箭头一样对待 forall ，我们可以对事物重新排序并删除多余的括号来整理一些东西。特别值得注意的是， callCC 实际上并不是游戏的结尾，事实证明，我们必须提供一个功能，这相当于提供另一个游戏，我们再次扮演最右边的箭头角色。所以我们可以通过合并这些步骤来保存一个步骤。我还会将类型参数浮动到左边，以便将它们全部放在一个地方。

$ b

  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 以取得进展。

$ b $

播放 a ：如果我们播放 code>作为 r2 ，那么我们可以将 id 作为 a - > R2 。另一个举动比较复杂，所以我们会跳到这一步。



b => r1 => a - > （b→r1）→> r1


返回代表我们的最右箭头。这一次，我们需要产生一些类型为 r1 的东西，其中 r1 是对手的一招。他们还演奏了一个功能 b - > r1 ，其中类型 b 也是他们所做的一个举动。所以我们需要一些类型的 b 或者 r1 。不幸的是，他们给我们的只是 a 类型的东西，让我们处于一个无法取胜的境地。猜猜之前播放 a 是一个不错的选择。让我们再试一次......

播放 r3 ： $ c> r3 作为 r2 ，我们还需要播放一个函数 a - > R3 ;幸运的是，对手已经发挥了这样的功能，所以我们可以简单地使用它。我们再次跳入另一个步骤：

  b => r1 => a  - > （b→r1）→> r1 
  

...只是发现它和以前完全一样的不可能的情况。在对手选择 r1 的情况下，不要求他们提供一种方法来构造一个让我们陷入困境。

也许有点欺骗会帮助你吗？

弯曲规则 - 演奏 r1 ：

我们知道，在常规的Haskell中，我们可以依靠懒惰来扭转事物并让计算吞下自己的尾巴。不用担心太多 ，让我们假设我们可以在这里做同样的事情 - 以我们的对手在内部游戏中玩的 r1 并将其拉出并回放，使其成为 r2 。

再一次，这是对手的举动：

  r2 => （b => r1 => a→（b→r1）→r1）→> （a→r2）→> r2 
  

经过我们打结的诡计之后，它终于等于这个：

$ b （b - > r1） - > r1） - > （a - > r1） - > r1

由于我们的诡计，类型参数已经消失，但是 r1 仍然被对手选中。因此，我们在这里完成的所有事情都在洗牌;我们显然没有办法希望得到 a 或 r3 ，所以我们又遇到了另一个死胡同。

所以我们做了一个最后的绝望尝试：

弯曲规则 - 演奏 b ：

这次我们把 b 由对手在最里面的游戏中进行游戏，然后循环播放为 r2 。现在对手的举动看起来像这样：
$ b

 （r1 => a  - >（b - > r1） - > r1） - > （a  - > b） - > b 
  

然后回到内部游戏：

  r1 => a  - > （b→r1）→> r1 
  

继续诡计，我们可以将 b 上面的结果，以及给予函数 b - > r1 ，接收我们需要的 r1 。成功！

退出后，我们仍然有一个问题。我们必须玩类型 a - > B'/ code>。没有明显的方法可以找到它，但我们已经有了一个 b ，所以我们可以使用 const on放弃 a 和 -

- 但是等等。类型 b 的值来自哪里？把自己简单地放在我们的对手的鞋子里，他们唯一能得到的地方就是来自我们 的动作结果。如果我们拥有的唯一 b 是他们给我们的，我们最终会绕着圈子走;游戏永远不会结束。

---

因此，在 callCC ，我们唯一的策略导致了损失或永久僵局。

$ b

callCC： ：forall a。 （（a - >（全部b.Conb）） - > Cont a） - >续a
callCC =错误一个奇怪的游戏......


唯一胜出的举动是不玩。

I thought the right type for ContT should be

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

and other control operators

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

Unfortunately, I can not make callCC type check, and don't know how to do it. I managed to make shift and reset type check

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

but still, I can't use shift and reset in recursive jumpings like this?

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

Have anyone tried this before?

解决方案

Would you like to play a game?

Today, you get to be callCC.

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

Everything to the left of that function arrow are the moves your opponent has made. To the right of the arrow is the end of the game. To win, you must construct something matching the right side using only the pieces your opponent has provided.

Fortunately, you still have some say in matters. See this arrow here?

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

When you receive something that itself contains an arrow, everything to the left of that represents moves you get to make, and the part to the right the end of that game branch, giving you another piece you can use as part of your (hopefully) winning strategy.

Before we go further, let's simplify a few things: The monad transformer aspect is merely a distraction, so discard that; and add explicit quantifiers for every type variable.

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

Now, think about what a type like forall a. ... amounts to. If you produce something with a type like that, you're saying you can provide a value for any type a whatsoever. If you receive something with a type like that, you can pick a specific type to use. Compare that to a type like A -> ... for a monomorphic function; producing such a function says that you know how to provide a result for any value of type A, while receiving such a function lets you pick a specific value A to use. This seems to be the same situation as with forall, and in fact the parallel holds. So, we can treat forall as indicating a move where you or your opponent gets to play a type, rather than a term. To reflect this, I'll abuse notation and write forall a. ... as a =>; we can then treat it just like (->) except that it must appear to the left of any uses of the type variable being bound.

We can also note that the only thing that can be done directly with a value of type Cont a is applying runCont to it. So we'll do that in advance, and embed all the relevant quantifiers directly into the type for callCC.

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

Because we're able to treat forall just like other function arrows, we can reorder things and remove superfluous parentheses to tidy things up a bit. In particular, note that callCC isn't actually the end of the game, as it turns out; we have to provide a function, which amounts to providing another game to play in which we again take the role of the rightmost arrow. So we can save a step by merging those. I'll also float type arguments to the left to get them all in one place.

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

So... our move.

We need something of type r3. Our opponent has made four moves, which we've received as arguments. One move is to choose r3, so we're at a disadvantage already. Another move is a -> r3, meaning that if we can play an a, our opponent will cough up an r3 and we can coast to victory. Unfortunately, our opponent has also played a, so we're back where we started. We'll either need something of type a, or some other way to get something of type r3.

The final move our opponent made is more complicated, so we'll examine it alone:

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

Remember, this is the move they made. So the rightmost arrow here represents our opponent, and everything to the left represents the type of moves we can make. The result of this is something of type r2, where r2 is something we get to play. So clearly we'll need to play either r3 or a to make any progress.

Playing a: If we play a as r2, then we can play id as a -> r2. The other move is more complicated, so we'll jump inside that.

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

Back to the rightmost arrow representing us. This time we need to produce something of type r1, where r1 is a move the opponent made. They also played a function b -> r1, where the type b was also a move they made. So we need something of either type b or r1 from them. Unfortunately, all they've given us is something of type a, leaving us in an unwinnable position. Guess playing a earlier was a bad choice. Let's try again...

Playing r3: If we play r3 as r2, we also need to play a function a -> r3; fortunately, the opponent already played such a function, so we can simply use that. Once again we jump inside the other move:

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

...only to find that it's exactly the same impossible situation as before. Being at the mercy of the opponent's choice of r1 with no requirement that they provide a way to construct one leaves us trapped.

Perhaps a bit of trickery will help?

Bending the rules -- playing r1:

We know that in regular Haskell we can rely on laziness to twist things around and let computations swallow their own tail. Without worrying too much about how, let's imagine that we can do the same here--taking the r1 that our opponent plays in the inner game, and pulling it out and back around to play it as r2.

Once again, here's the opponent's move:

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

After our knot-tying shenanigans, it ends up equivalent to this:

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

The type arguments have disappeared thanks to our trickery, but r1 is still chosen by the opponent. So all we've accomplished here is shuffling things around; there's clearly no way we can even hope to get an a or r3 out of this, so we've hit another dead end.

So we make one final, desperate attempt:

Bending the rules -- playing b:

This time we take the b played by the opponent in the innermost game and loop that around to play as r2. Now the opponent's move looks like this:

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

And then back in the inner game:

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

Continuing the trickery we can twist the b result above around as well, to give to the function b -> r1, receiving the r1 we need. Success!

Stepping back out, we still have one problem left. We have to play something of type a -> b. There's no obvious way to find one, but we already have a b lying around, so we can just use const on that to discard the a and--

--but wait. Where's that value of type b coming from in the first place? Putting ourselves briefly in our opponent's shoes, the only places they can get one are from the results of the moves we make. If the only b we have is the one they give us, we'll end up going around in circles; the game never ends.

---

So, in the game of callCC, the only strategies we have lead to either a loss or a permanent stalemate.

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

Alas, it seems that the only winning move is not to play.

这篇关于如何使callCC更具动态性？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！