阴阳延续难题在打字语言中是否有意义？

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

我试图用(编辑:静态)类型的语言编写一个等效的代码片段,例如SML/NJ,但是它给了我输入错误.所以要么拼图不输入,要么我误解了方案语法.上面的代码在SML或Ocaml(带callcc扩展名)中会是什么样的？

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

编辑:我想我知道答案.我们需要一种t满足t = t -> s某种类型的递归类型s.

编辑编辑:不,不是,答案是一个t令人满意的递归类型t = t -> t.

Answer 1

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

EFF

我们将使用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的

在这个例子中,我们需要Oleg Kiselyov的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,这是它说"一个类型α,使得α=α→α"的方式.这正是无类型λ演算模型的类型特征.所以我们有了它,阴阳拼图基本上使用了无类型的 λ演算的特征.