如何让callCC更加动态？

发布于 2024-12-01 11:33:00 字数 1119 浏览 1 评论 0原文

我认为 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?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

草莓酥 2024-12-08 11:33:00

您想玩游戏吗？

今天，您将成为 callCC。

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

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

幸运的是，你在事情上仍然有一定的发言权。看到这里的这个箭头了吗？

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

当您收到本身包含箭头的东西时，左侧的所有内容代表您要做的动作，而右侧的部分则表示该游戏分支的末尾，给你另一块你可以用来作为你（希望）获胜策略的一部分。

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

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

现在，想想像 forall a 这样的类型是什么。 ... 相当于。如果您生成具有类似类型的东西，则表示您可以为任何类型a提供值。如果您收到类似类型的内容，您可以选择要使用的特定类型。将其与 A -> 等类型进行比较... 对于单态函数；生成这样的函数表明您知道如何为 A 类型的任何值提供结果，而接收这样的函数可以让您选择要使用的特定值 A。这似乎与 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实际上并不是游戏的结束。我们必须提供一个函数，这相当于提供另一个游戏，让我们再次扮演最右边箭头的角色。所以我们可以通过合并这些来节省一个步骤。我还将向左浮动类型参数，将它们全部放在一处。

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。另一个动作更复杂，所以我们将跳进去。

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

回到代表我们的最右边的箭头。这次我们需要生成 r1 类型的内容，其中 r1 是对手的一步棋。他们还玩了一个函数b -> r1，其中类型 b 也是他们所做的一步。因此我们需要它们的 b 或 r1 类型。不幸的是，他们给我们的只是a类型的东西，让我们处于无法获胜的境地。我猜早点玩a是一个糟糕的选择。让我们再试一次...

播放r3：如果我们将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 => a -> (b -> r1) -> r1) -> (a -> r1) -> r1

由于我们的诡计，类型参数已经消失，但是r1仍然由对手选择。所以我们在这里所做的只是重新整理事情；显然我们根本不可能希望从中得到a或r3，所以我们又陷入了另一个死胡同。

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

改变规则——玩b：

这次我们采取对手在游戏中玩的b。最里面的游戏并循环播放以作为r2。现在对手的行动看起来像这样：

(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..."

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

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.

回复收藏 0 原文

迷鸟归林 2024-12-08 11:33:00

虽然没有办法赢得这场比赛，但如果我们能稍微扭转一下比赛，我们就能赢！

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

正如我们在另一个答案中所看到的，我们面临的问题是，为了获胜，我们必须为对手所玩的任意类型生成一个值，但我们不知道该怎么做。

通过强制所有原始类型（r 和 a）被 Maybe 修饰，我们可以绕过这个问题，并且能够生成一个值任何也许t——只需给他们什么都没有！

我们必须证明这是一个 Monad。

instance Monad m => Monad (ContT' m) where
    return a = ContT' $ \k -> k (Just a)
    a >>= f = ContT' $ \c -> runContT' a (
        maybe (return Nothing) (\v -> runContT' (f v) c))

然后我们可以实现callCC：

class Monad m => MonadCont' m where
    callCC' :: ((a -> forall b.m b) -> m a) -> m a

instance Monad m => MonadCont' (ContT' m) where
    callCC' k = ContT' $ \c -> 
        runContT' (k (\a -> ContT' $ \_ -> c (Just a) >> return Nothing)) c

我仍在研究如何实现reset和shift。

Although there is no way to win the given game, if we can twist the game a little bit we could win!

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

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 and a) being decorated by Maybe, we can bypass this problem, and are able to generate a value of any Maybe t -- simply give Nothing to them!

We got to show this is a Monad.

instance Monad m => Monad (ContT' m) where
    return a = ContT' $ \k -> k (Just a)
    a >>= f = ContT' $ \c -> runContT' a (
        maybe (return Nothing) (\v -> runContT' (f v) c))

And then We can implement callCC:

class Monad m => MonadCont' m where
    callCC' :: ((a -> forall b.m b) -> m a) -> m a

instance Monad m => MonadCont' (ContT' m) where
    callCC' k = ContT' $ \c -> 
        runContT' (k (\a -> ContT' $ \_ -> c (Just a) >> return Nothing)) c

I am still working out how to implemen reset and shift.

回复收藏 0 原文

~没有更多了~