iso- と equi- と OCaml の再帰型

Keigo Imai @keigoi

@m2ym let recを使わない不動点演算子なら @camlspotter さんの fix2 が回答なんじゃないかと(さっきはideone閲覧できなかった)。再帰型を許すなら再帰的なデータ構造を構成できるってことなので、関数型言語ならそれを利用して再帰関数なりYを作れる

m2ym @m2ym

@camlspotter @keigoi Wikipediaのやつで確かに不動点演算子が定義できました。どうもありがとうございます。In, outがroll, unrollの操作に対応するわけですね。ただ、このバリアントに関してはいまだに釈然としないところがありまして…

m2ym @m2ym

バリアントによる自己参照はμα.τを構成するってことでいいのかな

Keigo Imai @keigoi

@m2ym 例えば型aのリストlist = a * list + nil は F(X)=a*X + nil の不動点 μt.(a*t + nil)と等しいですよね。再帰型の宣言は実際にはそういう型構成子の不動点を宣言してると思えば。型付けとは別の、意味論の話なんでしょうね

Keigo Imai @keigoi

@m2ym さかいさんがHaskellの再帰は最大不動点だとかおっしゃっていたような気がするけどそのへんもググればでてくるのでは

m2ym @m2ym

@keigoi なるほど。それならiso-recursiveと呼べそうです。帰ったら定義を確認してみます。

m2ym @m2ym

@keigoi type t = t -> intは何らかの理由でダメだけど、type t = T of (t -> int)は再帰型と見做していいよっていう話ですよね

Yoshihiro Imai @yoshihiro503

@m2ym -rectypesもlet rec構文も使わず再帰関数を定義できます。 http://d.hatena.ne.jp/yoshihiro503/20100724#p1 #ocaml

m2ym @m2ym

@yoshihiro503 どうもありがとうございます。解決しました

Keigo Imai @keigoi

@m2ym その話がどう関係するのかよくわからないです。単に前者はequi-recursive型だから-rectypesが無いと駄目というだけの話かなと。何度もいうように型付けの話であって再帰の意味がどうという話とは違うのかなと私は思ってます。間違ってる可能性もかなりありますけど

m2ym @m2ym

あれ、またわけわかんなくなってきたぞ…再帰超むずい。意味論とかさっぱり

山本和彦 @kazu_yamamoto

.@m2ym 酒井さんを講師に招いて、勉強会をしましょう！

m2ym @m2ym

@keigoi すみません、初歩的な質問なんですがtype t = t -> intはequi-recursiveなんですか？この等号ってequi-recursiveの等号ではなく、正規木を連立方程式に変換したときの等号のようですが（「プログラミング言語の基礎理論」によると）

m2ym @m2ym

超賛成です RT @kazu_yamamoto: .@m2ym 酒井さんを講師に招いて、勉強会をしましょう！

Keigo Imai @keigoi

@m2ym 私の理解ですけど、再帰型t=t->intを、type t = T of t -> int と宣言すると、この型tをt->intとして扱うためにはパターンマッチでTを外す操作しないと駄目ですよね。それがiso-recursiveという再帰型の型付けの方法だと思ってます

Keigo Imai @keigoi

@m2ym 一方, type t=t->int という定義は t と t->int を同一視できる(=equi-recursive).

Keigo Imai @keigoi

@m2ym 構造だけ見れば type t=T of t->int と type t=t->int は同じだけど、型tとt->intを等しくするためには何か操作を間にはさまないといけない前者がiso-で、tとt->intを等しいとする後者がequi-recursiveな型付け

Keigo Imai @keigoi

色んな術語が間違ってる感じはすごくある

m2ym @m2ym

@keigoi 先の話だとtype t = t -> intでtはμα.α->intという型を持ちますよね。そのとき、μα.α->intと(μα.α->int)->intを等価と見做すかどうかは、その定義では決まらないと思うのですが、どうなんでしょう

m2ym @m2ym

あれ、なんかおかしいぞ。もうだめぽ

Keigo Imai @keigoi

@m2ym 等価とみなすかどうかは型の定義うんぬんではなくどういう型システムを選ぶかで決まります。 rectypesはequi-recursiveな型システムを有効にするので t=t->tみたいな型の等価性を許すのです。結果としてtype t=t->tみたいな型宣言も可能になる

m2ym @m2ym

ラベル付きバリアントとラベル無しバリアントって本質的に型付けが違うんだっけ。同じならtype t = t -> intもtype t = T of (t -> int)も同じ型になるはず？

Jun Furuse @camlspotter

ラベル無しバリアントなどない。前者はエイリアスを導入しているだけで、文字通り同一視するという意味ですよ QT @m2ym: ラベル付きバリアントとラベル無しバリアントって… 同じならtype t = t -> intもtype t = T of (t -> int)

m2ym @m2ym

@camlspotter すみません勘違いしてました

m2ym @m2ym

バリアントの推論規則を読み直さないと、何も言えないな