Имеет ли смысл головоломка продолжений инь и янь на типизированном языке?

Question

Этот вопрос относится к «Как работает головоломка Инь-Ян?» .Пример инь-янских продолжений в схеме выглядит следующим образом, согласно статье Википедии :

(let* ((yin
     ((lambda (cc) (display #\@) cc) (call-with-current-continuation (lambda (c) c))))
   (yang
     ((lambda (cc) (display #\*) cc) (call-with-current-continuation (lambda (c) c)))))
(yin yang))

Я пытаюсь написать эквивалентный фрагмент кода в (edit: статически ) типизированный язык, такой как SML / NJ, но он дает мне ошибки при печати.Так что либо головоломка не печатается, либо я неправильно понимаю синтаксис схемы.Как будет выглядеть приведенный выше фрагмент кода в SML или Ocaml (с расширением callcc)?

Кстати, из чего состоит загадка?Откуда это взялось?

Редактировать: Кажется, я знаю ответ.Нам нужен рекурсивный тип t, удовлетворяющий t = t -> s для некоторого типа s.

Редактирование редактирования: Нет, ответ рекурсивный тип t удовлетворяетt = t -> t.

Answer 1

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

эфф

Мы собираемся работать с eff (я здесь дую свой рог, см. Ниже другой способ в OCaml с расширением Олега delimcc .) Решение объясняется в статья Программирование с алгебраическими эффектами и продолжениями .

Сначала мы определим shift и reset в eff:

type ('a, 'b) delimited =
effect
  operation shift : (('a -> 'b) -> 'b) -> 'a
end

let rec reset d = handler
  | d#shift f k -> with reset d handle (f k) ;;

Вот загадка Инь-Ян, расшифрованная в eff:

let y = new delimited in
  with reset y handle
    let yin = (fun k -> std#write "@" ; k) (y#shift (fun k -> k k)) in
    let yang = (fun k -> std#write "*" ; k) (y#shift (fun k -> k k)) in
      yin yang

Но eff жалуется, что не может решить уравнение типа α = α → β. В настоящее время eff не может обрабатывать произвольные рекурсивные типы, поэтому мы застряли. В качестве способа обмана мы можем отключить проверку типов, чтобы посмотреть, выполняет ли код, по крайней мере, то, что он должен:

$ eff --no-types -l yinyang.eff
@*@**@***@****@*****@******@*******@********@*********@*******...

Хорошо, все правильно, но типы недостаточно мощные.

OCaml

Для этого примера нам понадобится Библиотека delimcc Олега Киселева . Код выглядит следующим образом:

open Delimcc ;;

let y = new_prompt () in
  push_prompt y (fun () ->
    let yin = (fun k -> print_string "@" ; k) (shift y (fun k -> k k)) in
    let yang = (fun k -> print_string "*" ; k) (shift y (fun k -> k k)) in
      yin yang)

Опять же, Ocaml не будет компилироваться, потому что он использует уравнение рекурсивного типа. Но с опцией -rectypes мы можем скомпилировать:

ocamlc -rectypes -o yinyang delimcc.cma yinyang.ml

Работает как положено:

$ ./yinyang
@*@**@***@****@*****@******@*******@********@*********@...

OCaml вычисляет, что тип yin и yang равен ('a -> 'a) as 'a, что является его способом сказать "тип α такой, что α = α → α". Это как раз типичная характеристика нетипизированных моделей λ-исчисления. Итак, у нас это есть, головоломка Инь-Ян по существу использует особенности нетипизированного λ-исчисления.

Answer 2

Можно объявить рекурсивный функциональный тип в C #, статически типизированном языке:

delegate Continuation Continuation(Continuation continuation);

Это определение эквивалентно ML * α : α → α.

Теперь мы можем «переведите «головоломку инь-ян» на C #.Для этого требуется преобразование для call / cc, и нам нужно выполнить преобразование дважды, потому что в нем их два, но результат по-прежнему очень похож на оригинал и в нем все еще есть вызов yin(yang):

Continuation c1 = cc1 =>
{
    Continuation yin = new Continuation(arg => { Console.Write("@"); return arg; })(cc1);
    Continuation c2 = cc2 =>
    {
        Continuation yang = new Continuation(arg => { Console.Write("*"); return arg; })(cc2);
        return yin(yang);
    };
    return c2(c2);
};
c1(c1);

Теперь ясно, что переменная yang находится только в локальной области видимости, поэтому мы можем фактически оптимизировать ее:

Continuation c1 = cc1 =>
{
    Continuation yin = new Continuation(arg => { Console.Write("@"); return arg; })(cc1);
    Continuation c2 = cc2 => yin(new Continuation(arg => { Console.Write("*"); return arg; })(cc2));
    return c2(c2);
};
c1(c1);

Теперь мы понимаем, что эти маленькие встроенные функции действительно простовывести символ и ничего не делать, поэтому мы можем развернуть его:

Continuation c1 = cc1 =>
{
    Console.Write("@");
    Continuation yin = cc1;
    Continuation c2 = cc2 =>
    {
        Console.Write("*");
        return yin(cc2);
    };
    return c2(c2);
};
c1(c1);

Наконец, становится ясно, что переменная yin также избыточна (мы можем просто использовать cc1).Чтобы сохранить первоначальный дух, переименуйте cc1 в yin и cc2 в yang, и мы получим нашего любимого yin(yang) обратно:

Continuation c1 = yin =>
{
    Console.Write("@");
    Continuation c2 = yang =>
    {
        Console.Write("*");
        return yin(yang);
    };
    return c2(c2);
};
c1(c1);

Все вышеперечисленное - одна и та же программаСемантически.Я думаю, что конечным результатом является фантастическая головоломка C # сама по себе.Поэтому я бы ответил на ваш вопрос, сказав: да, ясно, что это имеет большой смысл даже в статически типизированном языке:)

Answer 3

_{См. Также мой ответ на , как работает головоломка Инь-Ян , на которую мне нужно было найти ответ, прежде чем я смог ответить на него.}

Бытие«типизированный» язык сам по себе не имеет значения, является ли эта головоломка выразимой в нем (независимо от того, насколько расплывчат термин «типизированный язык»).Тем не менее, ответить на ваш вопрос наиболее буквально: да, это возможно, потому что сама Схема является типизированным языком: каждое значение имеет известный тип.Это явно не то, что вы имели в виду, поэтому я предполагаю, что вы имеете в виду, возможно ли это в языке, где каждой переменной присваивается постоянный тип, который никогда не изменяется (он же «статически типизированный язык»).

Более того, я 'Предположим, что вы хотите, чтобы дух головоломки сохранялся при выражении на каком-либо языке.Очевидно, что можно написать интерпретатор Scheme в машинном коде x86, и, очевидно, можно написать интерпретатор машинного кода x86 на языке typed , который имеет только целочисленные типы данных и указатели на функции.Но результат не в том же «духе».Поэтому, чтобы сделать это более точным, я наложу дополнительное требование: результат должен быть выражен с использованием истинных продолжений.Не эмуляция, а реальные полные продолжения.

Итак, вы можете иметь статически типизированный язык с продолжениями?Оказывается, вы можете, но вы все равно можете назвать это обманом.Например, в C #, если мои продолжения были определены как «функция, которая принимает объект и возвращает объект», где «объект» - это тип, который может содержать что угодно, сочтете ли вы это приемлемым?Что если функция принимает и возвращает «динамический»?Что если у меня есть «типизированный» язык, где каждая функция имеет один и тот же статический тип: «функция», без определения типов аргументов и возвращаемых типов?Является ли результирующая программа в том же духе, даже если она использует истинные продолжения?

Моя точка зрения заключается в том, что свойство «статически типизированный» по-прежнему допускает огромное количество изменений в системе типов, достаточное для того, чтобы всеразличия.Так что просто для удовольствия, давайте рассмотрим, что система типов должна поддерживать, чтобы квалифицировать ее как нечестную по любой мере.

Оператор call/cc(x) также может быть записан как x(get/cc), что значительнолегче понять на мой взгляд.Здесь x - это функция, которая принимает Continuation и возвращает значение, а get/cc возвращает Continuation.Continuation имеет все черты функции;он может быть вызван с одним аргументом и будет заменять значение, переданное туда, где изначально находился get / cc, который его создал, дополнительно возобновляя выполнение в этой точке.

Это означает, что get / cc имеетНеловкий тип: это function, но то же самое местоположение в конечном итоге вернет значение, тип которого мы еще не знаемПредположим, однако, что в духе статически типизированных языков мы требуем, чтобы возвращаемый тип был фиксированным.То есть, когда вы вызываете объект продолжения, вы можете передавать только значения предопределенного типа.При таком подходе тип функции продолжения может быть определен с помощью рекурсивного выражения вида T = function T->T.Как указал друг, этот тип может быть фактически объявлен в C #: public delegate T T(T t);!

Так что у вас есть;«печатание» не исключает и не гарантирует, что вы можете выразить эту головоломку, не изменяя ее природу.Однако, если вы разрешите статический тип «может быть чем угодно» (известный как object в Java и C #), то единственное, что вам нужно, - это поддержка истинных продолжений, и головоломка может быть представлена ​​без проблем.

---

Подходя к тому же вопросу с другой точки зрения, подумайте о том, чтобы переписать головоломку в нечто более напоминающее традиционный императивный язык со статической типизацией, который я объяснил в связанном ответе :

yin = (function(arg) { print @; return arg; })(get-cc);
yang = (function(arg) { print *; return arg; })(get-cc);
yin(yang);

Здесь тип yin и yang никогда не меняется .Они всегда хранят "продолжение C, которое принимает C и возвращает C" .Это очень совместимо со статической типизацией, единственное требование которой состоит в том, чтобы тип не изменялся при следующем выполнении этого кода.