Как сделать 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 в рекурсивных прыжках, как это?

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 ^^

Когда вы получаете что-то, что само содержит стрелку, все слева от этого представляет ходы, которые вы делаете, а часть справа - конец этой ветви игры, давая вам еще один кусок, который вы можете использовать как часть своего (надеюсь) выигрышная стратегия.

Прежде чем мы пойдем дальше, давайте упростим несколько вещей: аспект монадного трансформера - это просто отвлечение, поэтому отбросьте это; и добавьте явные квантификаторы для каждой переменной типа.

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 :

Мы знаем, что в обычном Хаскеле мы можем положиться на лень, чтобы все крутить и позволить вычислениям проглотить свой собственный хвост. Не слишком волнуясь о том, как, давайте представим, что мы можем сделать то же самое здесь - принимая 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..."

Увы, похоже, что единственный выигрышный ход - не играть.

Answer 2

Хотя нет никакой возможности выиграть данную игру, если мы сможем немного изменить игру, мы сможем выиграть!

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

Как мы видели в другом ответе, проблема, с которой мы сталкиваемся, заключается в том, что для победы нам нужно сгенерировать значение для произвольного типа, в который играл наш оппонент, но мы не знаем, как это сделать.

Вынуждая все необработанные типы (r а также a) украшена Maybeмы можем обойти эту проблему и можем генерировать значение любого Maybe t - просто дай Nothing им!

Мы должны показать, что это 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,