如何让callCC更加动态?
我认为 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
以前有人尝试过这个吗?
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?
如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
发布评论
评论(2)
您想玩游戏吗?
今天,您将成为
callCC
。该功能箭头左侧的所有内容都是对手所做的动作。箭头右侧是游戏结束。为了获胜,您必须仅使用对手提供的棋子构建与右侧相匹配的东西。
幸运的是,你在事情上仍然有一定的发言权。看到这里的这个箭头了吗?
当您收到本身包含箭头的东西时,左侧的所有内容代表您要做的动作,而右侧的部分则表示该游戏分支的末尾,给你另一块你可以用来作为你(希望)获胜策略的一部分。
在我们进一步讨论之前,让我们简化一些事情: monad 转换器方面只是一种干扰,所以放弃它;并为每个类型变量添加显式量词。
现在,想想像
forall a 这样的类型是什么。 ...
相当于。如果您生成具有类似类型的东西,则表示您可以为任何类型a
提供值。如果您收到类似类型的内容,您可以选择要使用的特定类型。将其与A -> 等类型进行比较...
对于单态函数;生成这样的函数表明您知道如何为A
类型的任何值提供结果,而接收这样的函数可以让您选择要使用的特定值A
。这似乎与forall
的情况相同,事实上,相似之处也成立。因此,我们可以将forall
视为指示您或您的对手开始玩类型的一步棋,而不是一个术语。为了反映这一点,我将滥用符号并为所有 a 编写。 ...
为a =>
;然后,我们可以像(->)
一样对待它,只不过它必须出现在所绑定类型变量的任何使用的左侧。我们还可以注意到,唯一可以直接使用
Cont a
类型的值完成的事情就是对其应用runCont
。因此,我们将提前执行此操作,并将所有相关量词直接嵌入到callCC
的类型中。因为我们能够像其他函数箭头一样对待
forall
,所以我们可以重新排序并删除多余的括号来稍微整理一下。特别要注意的是,事实证明,callCC
实际上并不是游戏的结束。我们必须提供一个函数,这相当于提供另一个游戏,让我们再次扮演最右边箭头的角色。所以我们可以通过合并这些来节省一个步骤。我还将向左浮动类型参数,将它们全部放在一处。所以...我们的举动。
我们需要 r3 类型的东西。我们的对手下了四步棋,我们已将其作为论据收到。第一步是选择
r3
,所以我们已经处于劣势了。另一个动作是a ->; r3
,这意味着如果我们能打出a
,我们的对手就会吐出r3
,我们就可以轻松获胜。不幸的是,我们的对手也玩了a
,所以我们又回到了开始的地方。我们要么需要a
类型的东西,要么需要其他方式来获取r3
类型的东西。我们的对手做出的最后一步更加复杂,所以我们将单独检查它:
记住,这是他们所做的一步。所以这里最右边的箭头代表我们的对手,左边的所有箭头代表我们可以采取的行动类型。其结果是
r2
类型,其中r2
是我们可以玩的东西。很明显,我们需要玩r3
或a
才能取得进展。播放
a
:如果我们将a
播放为r2
,那么我们就可以播放id
作为a -> r2
。另一个动作更复杂,所以我们将跳进去。回到代表我们的最右边的箭头。这次我们需要生成
r1
类型的内容,其中r1
是对手的一步棋。他们还玩了一个函数b -> r1
,其中类型b
也是他们所做的一步。因此我们需要它们的b
或r1
类型。不幸的是,他们给我们的只是a
类型的东西,让我们处于无法获胜的境地。我猜早点玩a
是一个糟糕的选择。让我们再试一次...播放
r3
:如果我们将r3
作为r2
播放,我们还需要播放函数a -> r3;幸运的是,对手已经发挥了这样的功能,所以我们可以简单地使用它。我们再次跳入另一个动作:
……却发现这与之前的不可能情况完全相同。受对手选择 r1 的支配,而不要求他们提供一种构建方法,这让我们陷入困境。
也许一些诡计会有所帮助?
扭曲规则——玩
r1
:我们知道,在常规的 Haskell 中,我们可以依靠惰性来扭曲事物,让计算吞掉自己的尾巴。不用太担心如何,让我们想象一下我们可以在这里做同样的事情——获取对手在内部游戏中玩的
r1
,并将其拉出并拉回来周围将其播放为r2
。再一次,这是对手的举动:
在我们的打结恶作剧之后,它最终相当于这样:
由于我们的诡计,类型参数已经消失,但是
r1
仍然由对手选择。所以我们在这里所做的只是重新整理事情;显然我们根本不可能希望从中得到a
或r3
,所以我们又陷入了另一个死胡同。所以我们做了最后一次绝望的尝试:
改变规则——玩
b
:这次我们采取对手在游戏中玩的
b
。最里面的游戏并循环播放以作为r2
。现在对手的行动看起来像这样:然后回到内部游戏:
继续这个诡计,我们也可以扭转上面的
b
结果,以赋予函数b ->; r1
,接收我们需要的r1
。成功!退一步来说,我们还剩下一个问题。我们必须玩
a ->; 类型的东西b.
。没有明显的方法可以找到一个,但我们已经有一个b
了,所以我们可以在其上使用const
来丢弃a
还有——但是等等。
b
类型的值首先来自哪里?让我们简单地站在对手的角度考虑一下,他们唯一能得到的位置就是我们采取的行动的结果。如果我们唯一的b
就是他们给我们的,我们最终会原地打转;游戏永远不会结束。因此,在
callCC
游戏中,我们唯一的策略要么导致失败,要么导致永久的僵局。唉,看来唯一的胜利之举就是不玩。
Would you like to play a game?
Today, you get to be
callCC
.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?
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.
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 typea
whatsoever. If you receive something with a type like that, you can pick a specific type to use. Compare that to a type likeA -> ...
for a monomorphic function; producing such a function says that you know how to provide a result for any value of typeA
, while receiving such a function lets you pick a specific valueA
to use. This seems to be the same situation as withforall
, and in fact the parallel holds. So, we can treatforall
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 writeforall a. ...
asa =>
; 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 applyingrunCont
to it. So we'll do that in advance, and embed all the relevant quantifiers directly into the type forcallCC
.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 thatcallCC
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.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 chooser3
, so we're at a disadvantage already. Another move isa -> r3
, meaning that if we can play ana
, our opponent will cough up anr3
and we can coast to victory. Unfortunately, our opponent has also playeda
, so we're back where we started. We'll either need something of typea
, or some other way to get something of typer3
.The final move our opponent made is more complicated, so we'll examine it alone:
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
, wherer2
is something we get to play. So clearly we'll need to play eitherr3
ora
to make any progress.Playing
a
: If we playa
asr2
, then we can playid
asa -> r2
. The other move is more complicated, so we'll jump inside that.Back to the rightmost arrow representing us. This time we need to produce something of type
r1
, wherer1
is a move the opponent made. They also played a functionb -> r1
, where the typeb
was also a move they made. So we need something of either typeb
orr1
from them. Unfortunately, all they've given us is something of typea
, leaving us in an unwinnable position. Guess playinga
earlier was a bad choice. Let's try again...Playing
r3
: If we playr3
asr2
, we also need to play a functiona -> r3
; fortunately, the opponent already played such a function, so we can simply use that. Once again we jump inside the other move:...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 asr2
.Once again, here's the opponent's move:
After our knot-tying shenanigans, it ends up equivalent to this:
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 ana
orr3
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 asr2
. Now the opponent's move looks like this:And then back in the inner game:
Continuing the trickery we can twist the
b
result above around as well, to give to the functionb -> r1
, receiving ther1
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 ab
lying around, so we can just useconst
on that to discard thea
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 onlyb
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.Alas, it seems that the only winning move is not to play.
虽然没有办法赢得这场比赛,但如果我们能稍微扭转一下比赛,我们就能赢!
正如我们在另一个答案中所看到的,我们面临的问题是,为了获胜,我们必须为对手所玩的任意类型生成一个值,但我们不知道该怎么做。
通过强制所有原始类型(
r
和a
)被Maybe
修饰,我们可以绕过这个问题,并且能够生成一个值任何也许t
——只需给他们什么都没有
!我们必须证明这是一个
Monad
。然后我们可以实现
callCC
:我仍在研究如何实现
reset
和shift
。Although there is no way to win the given game, if we can twist the game a little bit we could win!
As we have seen in the other answer, the problem we have is, to win we have to generate a value for an arbitrary type our opponent played, but we do not know how to do so.
By forcing all raw types (
r
anda
) being decorated byMaybe
, we can bypass this problem, and are able to generate a value of anyMaybe t
-- simply giveNothing
to them!We got to show this is a
Monad
.And then We can implement
callCC
:I am still working out how to implemen
reset
andshift
.