Хотели бы вы сыграть в игру ?
Сегодня вы станете 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 ^^
Когда вы получаете что-то, что само содержит стрелку, все слева от , что представляет ходы , которые вы делаете, а часть справа - конец этой ветви игры , давая вам еще один кусок, который вы можете использовать как часть вашей (надеюсь) выигрышной стратегии.
Прежде чем мы пойдем дальше, давайте упростим несколько вещей: аспект трансформации монады - это просто отвлечение, поэтому отбросьте это; и добавьте явные квантификаторы для каждой переменной типа.
callCC :: forall a. ((a -> (forall b. Cont b)) -> Cont a) -> Cont a
Теперь подумайте, что такое тип, как forall a. .... Если вы производите что-то с таким типом, вы говорите, что можете предоставить значение для любого типа a. Если вы получаете что-то с таким типом, вы можете выбрать конкретный тип для использования. Сравните это с типом типа A -> ... для мономорфной функции; создание такой функции говорит о том, что вы знаете, как предоставить результат для любого значения типа A, а получение такой функции позволяет выбрать конкретное значение A для использования. Это похоже на ту же ситуацию, что и с forall, и на самом деле параллель справедлива Таким образом, мы можем рассматривать forall как указание на ход, в котором вы или ваш оппонент могут сыграть type , а не термин. Чтобы отразить это, я использую нотацию и напишу 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:
Мы знаем, что в обычном Хаскеле мы можем положиться на лень, чтобы все крутить и позволить вычислениям проглотить свой собственный хвост. Не беспокоясь о как , давайте представим, что мы можем сделать то же самое здесь - взяв 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..."
Увы, похоже, что единственный выигрышный ход - не играть.