Има ли смисъл пъзелът с продълженията ин ян на въведен език?

Мисля, че сам ще отговоря на въпроса си. Ще покажа две решения, едно в eff и друго в Ocaml.

еф

Ще работим с 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, което е неговият начин да се каже "тип α такъв, че α = α → α". Това е именно типовата характеристика на нетипизираните λ-изчислителни модели. Ето го, пъзелът ин ян по същество използва функции на нетипизираното λ-изчисление.

Възможно е да се декларира рекурсивен функционален тип в C#, статично типизиран език:

delegate Continuation Continuation(Continuation continuation);

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

Сега можем да „преведем“ пъзела ин-ян на C#. Това наистина изисква трансформация за повикването/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# пъзел. Така че бих отговорил на въпроса ви, като кажа: да, очевидно има много смисъл дори на статично типизиран език :)

_{Вижте също моя отговор на как работи пъзелът ин ян, на който трябваше да намеря отговор, преди да може да отговори на този.}

Това, че е "типизиран" език, само по себе си не прави разликата дали този пъзел е изразим в него (без значение колко неясен е терминът "типизиран език"). Въпреки това, за да отговоря на въпроса ви най-буквално: да, възможно е, защото самият Scheme е типизиран език: всяка стойност има известен тип. Това очевидно не е това, което имахте предвид, така че предполагам, че имате предвид дали това е възможно на език, където на всяка променлива е присвоен постоянен тип, който никога не се променя (известен още като "статично въведен език").

Освен това ще предположа, че искате духът на пъзела да бъде запазен, когато е изразен на някакъв език. Очевидно е възможно да се напише интерпретатор на Scheme в машинен код x86 и очевидно е възможно да се напише интерпретатор на машинен код x86 на типизиран език, който има само цели типове данни и функционални указатели. Но резултатът не е в същия "дух". Така че, за да направя това по-точно, ще поставя допълнително изискване: резултатът трябва да бъде изразен с помощта на верни продължения. Не емулация, а истински пълни продължения.

И така, можете ли да имате статично въведен език с продължения? Оказва се, че можете, но все пак можете да го наречете измама. Например, в C#, ако моите продължения бяха определени като "функция, която взема обект и връща обект", където "обект" е тип, който може да съдържа всичко, ще намерите ли това за приемливо? Какво ще стане, ако функцията вземе и върне "динамика"? Какво ще стане, ако имам "типизиран" език, където всяка функция има един и същ статичен тип: "функция", без да дефинирам типовете аргументи и връщаните типове? Получената програма все още ли е в същия дух, въпреки че използва истински продължения?

Искам да кажа, че свойството "статично въведено" все още позволява огромно количество вариации в системата от типове, достатъчно, за да направи цялата разлика. Така че просто за забавление, нека помислим какво трябва да поддържа системата за типове, за да се квалифицира като неизмамна по каквато и да е мярка.

Операторът call/cc(x) може да бъде написан и като x(get/cc), което според мен е много по-лесно за разбиране. Тук x е функция, която приема продължение и връща стойност, докато 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". Това е много съвместимо със статичното писане, чието единствено изискване е типът да не се променя следващия път, когато изпълните този код.