如何使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在递归jumpings这样吗？

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

你想玩游戏吗？

今天,你会成为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视为指示您或您的对手发挥类型而不是术语的移动.为了反映这一点,我会滥用符号,写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..."

唉,似乎唯一获胜的举动就是不玩.