阴阳延续难题在类型化语言中是否有意义？ [英] Does the yin yang continuations puzzle make sense in a typed language?

问题描述

这个问题与阴阳之谜如何工作？有关。一>。根据维基百科文章 a>：

 （let *（（yin 
（（lambda（cc）（display＃\ @） cc）（call-with-current-continuation（lambda（c）c））））
（yang 
（（lambda（cc）（display＃\ *）cc） （b）（b）（b）（b）（b） p>我试图在（编辑：静态）类型语言（如SML / NJ）中编写一段代码，但它给我输入错误。所以要么拼图没有输入，要么我误解了方案的语法。上面那段代码在SML或Ocaml中的样子（ callcc 扩展名）> 
顺便说一句，难题的根源是什么？它来自哪里？
 
 
 
 编辑：我想我知道答案。我们需要一个递归类型 t 满足 t = t  - >对于某些类型 s 。
 
 
 
 编辑它不是，答案是递归类型 t 满足 t = t  - > 
      我想我会回答我自己的问题。我将展示两种解决方案，一种在eff中，另一种在Ocaml中。 
 
 
 eff 
 
 
 
我们将开始工作与 eff （我在这里吹响自己的号角，参见下面的另一种方式在OCaml中使用 Oleg的delimcc扩展）。该解决方案在使用代数效果和延续编程。  
 
首先我们在eff中定义 shift 和 reset   
 
 
  type（'a，'b）分隔= 
效果
操作shift：（（''a - > b） - >'b） - > 'a 
结束
 
让rec复位d =处理程序
 | d＃shift f k  - >重置d句柄（f k）;; 
  
这里是阴阳益智转录为eff： 
 
 
  let y =在
中新定界，并且复位y处理
 let yin =（fun k  - > std＃write@; k）（在
中让yang =（fun k  - > std＃write*; k）（y＃shift（fun k  - > kk））in $ b $ y y＃shift（fun k-> kk） b $ b yin yang 
  
但是eff却抱怨它无法解决类型方程
α=α→β。目前eff不能处理任意递归类型，所以我们被卡住了。作为一种欺骗手段，我们可以关闭类型检查，看看至少代码是否应该做到这一点： 
 
 
  $ eff --no-types -l yinyang.eff 
 @ * @ ** @ *** @ **** @ ***** @ ****** @ **** *** @ ******** @ ********* @ ******* ... 
  
好吧，它正在做正确的事情，但是类型不够强大。 
 
 
 OCaml 
 
 
 
在这个例子中，我们需要 Oleg Kiselyov的delimcc库。代码如下： 
 
 
 打开Delimcc ;; 
 
 let y = new_prompt（）in 
 push_prompt y（fun（） - > 
 let yin =（fun k  - > print_string@; k） 
 yang =（fun k  - > print_string*; k）（shift y（fun k  - > kk））in 
 yin yang ）
  
同样，Ocaml不会编译，因为它碰到递归类型方程。但是使用 -rectypes 选项，我们可以编译：
  ocamlc -rectypes -o yinyang delimcc.cma yinyang.ml 
  
它按预期工作： 
  $ ./yinyang 
 @ * @ ** @ *** @ **** @ *** ** @ ****** @ ******* @ ******** @ ********* @ ... 
  
 OCaml计算出 yin 和 yang 是（'a  - >'a）为'a ，这就是α类型使得α=α→α的方式。这正是无类型λ演算模型的类型特征。所以我们有了它，阴阳益智基本上使用了 untyped λ演算的特征。 
This question is related to "How the yin-yang puzzle works?". The yin yang example of continuations in scheme looks like this, according to 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))
I am trying to write an equivalent piece of code in a (edit: statically) typed language, such as SML/NJ, but it is giving me typing errors. So either the puzzle does not type, or I am misunderstanding the scheme syntax. What would the above piece of code look like in SML or Ocaml (with callcc extension)?

By the way, what is the source of the puzzle? Where did it come from?

Edit: I think I know the answer. We need a recursive type t satisfying t = t -> s for some type s.

Edit of edit: No it is not, the answer is a recursive type t satisfying t = t -> t.
解决方案
I think I am going to answer my own question. I will show two solutions, one in eff and another in Ocaml.

eff

We are going to work with eff (I am blowing my own horn here, see below for another way  in OCaml with Oleg's delimcc extension.) The solution is explained in the paper Programming with algebric effects and continuations. 

First we define shift and reset in 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) ;;
Here is the yin yang puzzle transcribed into 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
But eff complains about it that it can't solve the type equation 
α = α → β. At present eff cannot handle arbitrary recursive types, so we are stuck. As a way of cheating, we can turn off type checking to see if at the very least the code does what it is supposed to:
$ eff --no-types -l yinyang.eff
@*@**@***@****@*****@******@*******@********@*********@*******...
Ok, it's doing the right thing, but the types are not powerful enough.

OCaml

For this example we need Oleg Kiselyov's delimcc library. The code is as follows:
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)
Again, Ocaml won't compile because it hits a recursive type equation. But with the -rectypes option we can compile:
ocamlc -rectypes -o yinyang delimcc.cma yinyang.ml
It works as expected:
$ ./yinyang
@*@**@***@****@*****@******@*******@********@*********@...
OCaml computes that the type of yin and yang is ('a -> 'a) as 'a, which is its way of saying "a type α such that α = α → α". This is precisely the type characteristic of the untyped λ-calculus models. So there we have it, the yin yang puzzle essentially uses features of the untyped λ-calculus.

                        
这篇关于阴阳延续难题在类型化语言中是否有意义？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！