iso- と equi- と OCaml の再帰型 (2ページ目)

めしくってくる QT @m2ym: @camlspotter そしてその両者を総じて再帰型と呼ぶそうです。ところでOCamlではlet recを使わずに純粋に不動点演算子を定義できないので、本当の意味での再帰型は提供されてないのでは？というのが僕の疑問です

2011-02-01 12:16:27

ideoneがみれなくなった。 let rec y f x = f (y f) x;; let fact = y (fun f x -> if x=0 then 1 else f (x-1) * x);; fact 10

2011-02-01 13:10:04

@m2ym ocaml は iso rec 。

2011-02-01 13:10:31

@m2ym OCamlも -rectypes を使えばめでたくequi-recursiveになりますけどそこはオッケーでしょうか。あと単にYコンビネータが欲しければ-rectypes無しでも let rec y f x = f (y f) x で得られます

2011-02-01 13:34:07

http://ideone.com/JzYen QT @m2ym: @camlspotter 不動点演算子を定義するためには少なくともμα.α->τを表現できないとダメだと思うのですが、どうなのでしょう

2011-02-01 13:42:19

というわけで安心して本物(?)の再帰型を使ってください

2011-02-01 13:52:26

山本和彦 @kazu_yamamoto

.@m2ym @camlspotter よく分かっていませんが、それは名前で再帰できない型付きラムダ計算での話ではないですか？ http://d.hatena.ne.jp/kazu-yamamoto/20100519/1274240859

2011-02-01 13:53:36

Jacques Garrigue @garriguejej

@keigoi let rec は要らんよ。#rectypes;; let y f = (fun x -> f (fun y -> x x y)) (fun x -> f (fun y -> x x y));;

2011-02-01 14:00:51

再帰データ型の理論からみたそういう話です QT @kazu_yamamoto: .@m2ym @camlspotter よく分かっていませんが、それは名前で再帰できない型付きラムダ計算での話ではないですか？

2011-02-01 14:01:56

@m2ym -rectypes にすると equi が使えるようになる、のかな？

2011-02-01 14:03:16

ocaml rectypes equi で検索すれば名古屋が最強という結論が得られた。

2011-02-01 14:04:42

@garriguejej @m2ym はい、説明するのをおもいっきりサボってしまいました… let rec y f ... は -rectypes 無しでもYが定義できるよと言いたかったのです。-rectypesならガリグ先生がおっしゃるとおりrecすら要らなくなります。こわい。

2011-02-01 14:05:36

@keigoi -rectypes付ければequi-recursiveになるのは確認済みです。ただ、let recで不動点演算子を定義できる、というのは反則な気がします。というのもlet rec自身が裏で特別な不動点演算子を持ってますから

2011-02-01 14:39:10

これもlet recですよね RT @camlspotter: http://ideone.com/JzYen QT @m2ym: @camlspotter 不動点演算子を定義するためには少なくともμα.α->τを表現できないとダメだと思うのですが、どうなのでしょう

2011-02-01 14:39:54

そです RT @camlspotter: @m2ym -rectypes にすると equi が使えるようになる、のかな？

2011-02-01 14:40:58

@kazu_yamamoto newtype I a = I (I a -> a)はおそらくequi-recursiveになってるので不動点演算子を定義できるのでしょう

2011-02-01 14:43:37

集会の自由 @oskimura

RT @m2ym: これもlet recですよね RT @camlspotter: http://ideone.com/JzYen QT @m2ym: @camlspotter 不動点演算子を定義するためには少なくともμα.α->τを表現できないとダメだと思うのですが、どうなのでしょう

2011-02-01 14:44:51

@m2ym 反則とはどういう文脈で？？たんなる再帰が反則ならOCamlもHaskellも反則なのかな。だとすればぜひCoqでも使ってみればいいんじゃないかと。止まる再帰しか書けなくなってるので気に入るのではないかと。

2011-02-01 14:45:00

@keigoi ちょっと混乱してきたので経緯を説明します。僕は今「プログラミング言語の基礎理論」を読んでいまして、再帰的データ型の解釈（？）にはIso-recursive typesとEqui-recursive typesがあります、という事が書いてありました。（続く）

2011-02-01 14:48:01

@m2ym それequi-recursiveじゃないですよ。TAPL読んでみれば載ってますけど、何かしらμを展開するために操作が必要なのがiso-で、無くても型チェック通るのがequiですよね。

2011-02-01 14:48:04

equi-とiso-って、再帰データ型の解釈とかおおげさな話ではなく、単に再帰型の型付け規則の話じゃないのかな。

2011-02-01 14:50:38

@keigoi それじゃOCamlはどっちなんだろうと思ってググってみますと、OCamlはIso-recursiveであるという記事をいくつか見つけました。それならOCamlで不動点演算子を定義できるはず、と思ってやってみましたが、結局できませんでした

2011-02-01 14:50:40

fix2 はつかってねえよ QT @m2ym: これもlet recですよね RT @camlspotter: http://ideone.com/JzYen

2011-02-01 14:54:02