iso- と equi- と OCaml の再帰型
-
- いいね！0
m2ym
@m2ym
ocaml -rectypesしてtype untyped = untyped -> untypedを定義すれば型無しラムダ計算をエミュレートできるらしいよ
2011-01-31 10:58:45
m2ym
@m2ym
let succ = fun (n:untyped) -> fun (f:untyped) -> fun (z:untyped) -> n f (f z) とか
2011-01-31 11:00:09
m2ym
@m2ym
というかわけわからん部分も多い。いまだに謎なのがOCamlで-rectypes付けなくてもバリアントを使えば再帰的データ型が定義できること
2011-01-31 15:37:57
m2ym
@m2ym
やっぱりデフォはiso-recursiveで-rectypesつけるとequi-recursiveになるってのは間違ってると思う。デフォは謎の挙動で-rectypesつけるとequi-recursiveだな
2011-01-31 15:55:19
Jun Furuse
@camlspotter
明示的には無いですがループを作ればおけ QT @m2ym: うーん、そもそもμα.τを表すような型構築子がtype_descに無いな>OCaml
2011-01-31 18:39:31
m2ym
@m2ym
ループってどういうことでしょうか RT @camlspotter: 明示的には無いですがループを作ればおけ QT @m2ym: うーん、そもそもμα.τを表すような型構築子がtype_descに無いな>OCaml
2011-01-31 18:59:20
Jun Furuse
@camlspotter
内部的に type_expr で自分の親のノードを参照すればループができます。μα....α... をループのあるグラフで表している。 QT @m2ym: ループってどういうことでしょうか
2011-01-31 19:08:09
Jun Furuse
@camlspotter
caml では (... α ... as α) とプリントされます。printtype.ml の tree_of_type_expr か何か(いまアクセスできない)等にループを見つけるコードがある。 @m2ym
2011-01-31 19:13:58
Jun Furuse
@camlspotter
再帰データ型定義内で自己参照は TConstr(id, ...) になって、ループは名前で表される、なのでこのループ制限には抵触しない
2011-01-31 19:21:04
m2ym
@m2ym
@camlspotter 情報ありがとうございます。実装面での状況は大体把握できたのですが、やはり背景となる理論が不明なので、もやもや感が拭えません。OCamlは不動点演算子を定義できないのに、再帰的データ型を提供していると言えるのかどうか、とか
2011-02-01 11:18:26
Jun Furuse
@camlspotter
kwsk QT @m2ym: OCamlは不動点演算子を定義できないのに、再帰的データ型を提供していると言えるのかどうか、とか
2011-02-01 11:53:09
Jun Furuse
@camlspotter
type t = ... で不動点入るから問題ないが？ QT @m2ym: OCamlは不動点演算子を定義できないのに、再帰的データ型を提供していると言えるのかどうか、とか
2011-02-01 11:57:58
m2ym
@m2ym
@camlspotter 大堀先生の「プログラミング言語の基礎理論」を読んでいるのですが、これによるとIso-recursive typesでもEqui-recursive typesでも適切な推論規則や評価規則があれば、不動点演算子を定義し得るとあります。（続く）
2011-02-01 11:59:46
m2ym
@m2ym
@camlspotter そしてその両者を総じて再帰型と呼ぶそうです。ところでOCamlではlet recを使わずに純粋に不動点演算子を定義できないので、本当の意味での再帰型は提供されてないのでは？というのが僕の疑問です
2011-02-01 12:02:26
Jun Furuse
@camlspotter
iso とか equi とか知らんからなんとも(^_^;) QT @m2ym: @camlspotter 大堀先生の「プログラミング言語の基礎理論」を読んでいるのですが、これによるとIso-recursive typesでもEqui-recursive typesでも適切な推論
2011-02-01 12:02:49