阴阳延续谜题在打字语言中有意义吗？

Posted 2023-03-15

【中文标题】阴阳延续谜题在打字语言中有意义吗？

【英文标题】：Does the yin yang continuations puzzle make sense in a typed language?

【发布时间】：2012-03-04 06:17:05

【问题描述】：

此问题与"How the yin-yang puzzle works?" 有关。方案中延续的阴阳例子是这样的，根据Wikipedia article：

(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))

我正在尝试用（编辑：静态）类型的语言（例如 SML/NJ）编写等效的代码，但它给我输入错误。所以要么拼图没有输入，要么我误解了方案语法。上面这段代码在 SML 或 Ocaml 中会是什么样子（带有callcc 扩展名）？

顺便问一下，这个谜题的来源是什么？它是从哪里来的？

编辑：我想我知道答案。对于某些类型s，我们需要一个满足t = t -> s 的递归类型t。

编辑编辑：不，不是，答案是递归类型t满足t = t -> t。

【参考方案1】：

我想我会回答我自己的问题。我将展示两种解决方案，一种在 eff 中，另一种在 Ocaml 中。

有效

我们将与eff 合作（我在这里吹自己的号角，请参阅下面的在OCaml 中使用Oleg's delimcc extension 的另一种方式。）解决方案在论文Programming with algebric effects and continuations 中进行了解释。

首先我们在eff中定义shift和reset：

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

对于这个例子，我们需要Oleg Kiselyov's delimcc library。代码如下：

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，这是它的说法“a type α such as α = α → α”。这正是无类型 λ 演算模型的类型特征。所以我们有了它，阴阳谜题本质上使用了 untyped λ-演算的特征。

【讨论】：

我在 SML 中尝试了 this，但在递归（循环）类型上遇到了同样的限制。

【参考方案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# 难题。所以我会这样回答你的问题：是的，很明显，即使在静态类型的语言中它也很有意义:)

【讨论】：

这很酷，但你没有使用延续，这是阴阳谜题的核心。不要误会我的意思，你所做的很整洁，只是不是原来的拼图。相反，您使用了 λ-演算，因为您的解决方案可以用纯函数重写。 C# 并没有真正的一流延续，不是吗？不幸的是，我不能在这里编写等效的 OCaml 代码。我应该将其作为单独的答案发布吗？

我认为它确实使用延续。它只是不使用 C# 所没有的 call-with-current-continuation。我的程序是编译器必须对带有 call/cc 的程序进行第一次转换后得到的。仅仅因为它编译掉 call/cc 并不意味着它编译掉了延续。

对。尽管如此，虽然原版看起来令人恐惧和混乱，但这个看起来只是令人困惑:-)

@AndrejBauer：你的问题不是关于恐惧或混乱，而是关于“这个谜题在打字语言中是否有意义”。

这个讨论是没有意义的，因为你是否“太多”地改变了这个谜题在很大程度上是一个见仁见智的问题。无论如何，答案是，这个谜题在具有足够递归类型的语言中是有意义的（但是，在这种语言中任何事情都是有意义的）。

【参考方案3】：

_{另请参阅我对how the yin yang puzzle works 的回答，我必须先找到答案才能回答这个问题。}

作为一种“类型化”语言本身并不会影响这个谜题是否可以用它来表达（无论“类型化语言”这个词有多么模糊）。但是，从字面上回答您的问题：是的，这是可能的，因为 Scheme 本身就是一种类型化语言：每个值都有一个已知类型。这显然不是你的意思，所以我假设你的意思是在每个变量都被分配一个永不改变的永久类型的语言中这是否可能（又名“静态类型语言”）。

此外，我假设您希望以某种语言表达拼图的精神。显然可以用 x86 机器码编写 Scheme 解释器，显然也可以用只有整数数据类型和函数指针的 typed 语言编写 x86 机器码解释器。但结果不是同一个“精神”。所以为了更精确，我将提出一个额外的要求：结果必须使用真正的延续来表达。不是模拟，而是真正的全面延续。

那么，你能拥有一种带有延续的静态类型语言吗？事实证明你可以，但你仍然可以称之为作弊。例如，在 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);！

所以你有它;被“打字”并不排除或保证你可以在不改变其性质的情况下表达这个谜题。但是，如果您允许静态类型“可以是任何东西”（在 Java 和 C# 中称为 object），那么您唯一需要的另一件事就是支持真正的延续，并且可以表示拼图没有问题。

---

从不同的角度处理同一个问题，考虑一下我将这个谜题改写成更让人想起传统静态类型命令式语言的东西，我在linked answer 中对此进行了解释：

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

这里，yin 和 yang 的类型永远不会改变。他们总是存储一个“接受一个C并返回一个C的延续C”。这与静态类型非常兼容，静态类型的唯一要求是下次执行该代码时类型不会改变。

【讨论】：

感谢您的详细回答，但您并没有真正回答我的问题。我明确询问了关于静态类型的 la ML。我认为我在我的问题中对此很清楚，但也许不是。 javascript 并没有真正为答案添加任何内容，因为就像方案一样，它不是静态类型的。翻译成不那么冗长但更精确的语言，你的答案是我们需要递归类型 α = α → α。这很有趣，因为 eff 告诉我有问题的方程是 α = α → β。必须 α = β？

@AndrejBauer 首先，“明确地”肯定是错误的 :) 其次，我 am 谈论的是静态类型语言；我不是在谈论 JavaScript。我确实提到过 JS syntax 一次；我会删除它。

还有什么比“我正在尝试用 SML/NJ 等类型化语言编写等效的代码，但它给我输入错误”更明确的呢？我想“静态”这个词不见了。好的，我会添加它只是为了让你看起来很糟糕;-)无论如何，这并不重要。

@AndrejBauer 在我的辩护中，我从未听说过这种语言，而且运行时也会出现“输入错误” :) 无论如何，很高兴你得到了答案。

您输入正确，它是 α = α → α 而不是 α = α → β，正如 eff 中的输入错误所报告的那样。 OCaml 可以计算类型，请参阅我更新的答案。此外，正确的结论是阴阳谜题本质上是无类型的，因为yin 和yang 的类型与为无类型λ-演算提供类型所需的类型相同。