Как callCC реализован на строго функциональных языках?

Question

Рассмотрим следующий пример в Haskell функции quux наряду с определениями продолжения монады и callCC,

instance Monad (Cont r) where
    return x = cont ($ x)
    s >>= f  = cont $ \c -> runCont s $ \x -> runCont (f x) c

callCC :: ((a -> Cont r b) -> Cont r a) -> Cont r a
callCC f = cont $ \h -> runCont (f (\a -> cont $ \_ -> h a)) h

quux :: Cont r Int
quux = callCC $ \k -> do
    let n = 5
    k n
    return 25

Как я понимаю этот пример. Блок do можно рассматривать как

k n >>= \_ -> return 25 == 
cont $ \c -> runCont (k n) $ \x -> runCont ((\_ -> return 25) x) c

И мы можем видеть из определения k который \a -> cont $ \_ -> h a что в приведенном выше \x -> runCont ((\_ -> return 25) x) c быть переданным в аргумент, который игнорируется с подчеркиванием. В конечном итоге return 25 фактически "игнорируется", потому что аргумент подчеркивания никогда не используется, поэтому из ленивых вычислений он никогда не оценивается.

Так что, насколько я могу судить, эта реализация callCC сильно принципиально зависит от ленивых оценок. Как бы это callCC быть сделано на строгом (не ленивом) функциональном языке?

Answer 1

Нет. Эта реализация callcc не зависит от ленивой оценки Чтобы доказать это, я реализую это на строгом функциональном языке и покажу, что после k n не выполняется вообще.

Строгий функциональный язык, который я буду использовать, - это JavaScript. Поскольку JavaScript не является статически типизированным, вам не нужно объявлять newtype, Поэтому мы начнем с определения return а также >>= функции Cont монада в JavaScript. Мы назовем эти функции unit а также bind соответственно:

function unit(a) {
    return function (k) {
        return k(a);
    };
}

function bind(m, k) {
    return function (c) {
        return m(function (a) {
            return k(a)(c);
        });
    };
}

Далее мы определяем callcc следующее:

function callcc(f) {
    return function (c) {
        return f(function (a) {
            return function () {
                return c(a);
            };
        })(c);
    };
}

Теперь мы можем определить quux следующее:

var quux = callcc(function (k) {
    var n = 5;

    return bind(k(n), function () {
        alert("Hello World!");
        return unit(25);
    });
});

Обратите внимание, что я добавил alert внутри второго аргумента bind проверить, выполнено ли это. Теперь, если вы позвоните quux(alert) будет отображаться 5 но он не будет отображаться "Hello World!", Это доказывает, что второй аргумент bind никогда не был казнен. Посмотрите демо для себя.

Почему это происходит? Давайте начнем с quux(alert), По бета-уменьшению это эквивалентно:

(function (k) {
    var n = 5;

    return bind(k(n), function () {
        alert("Hello World!");
        return unit(25);
    });
})(function (a) {
    return function () {
        alert(a);
    };
})(alert);

При бета-уменьшении это снова становится:

bind(function () {
    alert(5);
}, function () {
    alert("Hello World!");
    return unit(25);
})(alert);

Далее по бета-версии сокращения bind мы получаем:

(function (c) {
    return (function () {
        alert(5);
    })(function (a) {
        return (function () {
            alert("Hello World!");
            return unit(25);
        })(a)(c);
    });
})(alert);

Теперь мы можем понять, почему "Hello World!" никогда не отображался. По сокращению бета мы выполняем function () { alert(5); }, Задача этой функции - вызывать аргумент, но он этого не делает. Из-за этого выполнение останавливается и "Hello World!" никогда не отображается. В заключение:

callccфункция не зависит от ленивой оценки.

Функция, созданная callcc заканчивается после k называется не из-за ленивой оценки, а потому что k разрывает цепочку, не вызывая ее первый аргумент и, следовательно, немедленно возвращается.

Это возвращает меня к вашему вопросу:

И мы можем видеть из определения k который \a -> cont $ \_ -> h a что в приведенном выше \x -> runCont ((\_ -> return 25) x) c быть переданным в аргумент, который игнорируется с подчеркиванием. В конечном итоге return 25 фактически "игнорируется", потому что аргумент подчеркивания никогда не используется, поэтому из ленивых вычислений он никогда не оценивается.

Вы ошибаетесь Как вы видете k является (\a -> cont $ \_ -> h a) и функция (\x -> runCont ((\_ -> return 25) x) c) передается в аргумент, который игнорируется k, Вы были правы до тех пор. Однако это не значит, что return 25 не оценивается из-за ленивой оценки. Это просто не оценивается, потому что функция (\x -> runCont ((\_ -> return 25) x) c) никогда не называется. Я надеюсь, что все прояснилось.