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

Ответ 1

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

эфф

Мы будем работать с eff (я дую свой собственный рог здесь, см. ниже по другому пути в OCaml с Расширение Oleg 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 --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, что является его способом сказать "тип α такой, что α = α → α". Это как раз тип, характерный для нетипизированных моделей λ-исчислений. Итак, мы имеем это, головоломка инь-ян в основном использует черты нетипизированного λ-исчисления.

Ответ 2

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

delegate Continuation Continuation(Continuation continuation);

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

Теперь мы можем "перевести" загадку инь-ян в С#. Для этого требуется преобразование для вызова /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);

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

Ответ 3

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

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

Кроме того, я полагаю, что вы хотите, чтобы дух головоломки сохранялся, когда выражался на каком-то языке. Очевидно, что возможно написать интерпретатор Схемы в машинный код x86 и, очевидно, его можно написать интерпретатор машинного кода x86 на типизированном языке, который имеет только целые типы данных и указатели функций. Но результат не в том же "духе". Поэтому, чтобы сделать это более точным, я поставлю дополнительное требование: результат должен быть выражен с использованием истинных продолжений. Не эмуляция, а реальное полное продолжение.

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

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

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

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

Итак, у вас это есть; будучи "напечатанным", не исключает и не гарантирует, что вы можете выразить эту загадку, не изменяя ее характер. Тем не менее, если вы разрешаете статический тип "может быть что угодно" (известный как object в Java и С#), тогда вам нужна только одна вещь для поддержки настоящих продолжений, и головоломка может быть без проблем.

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

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

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