-
kazu_yamamoto
- 7751
- 0
- 12
- 1
-
- いいね！1
山本和彦
@kazu_yamamoto
.@camlspotter うーん。僕がよく聞く型検査と @camlspotter さんの型検査の定義は違うようです。。。。
2011-05-02 19:39:46
山本和彦
@kazu_yamamoto
.@camlspotter the implementation of functional languages は、type checking という言葉が出てきますが、一体これは何ですか？
2011-05-02 19:40:36
Jun Furuse
@camlspotter
Type inference とか type reconstruction とか言うのメンドイし type check とか言っちゃうのよね complete だと特に…;;
2011-05-02 19:44:54
Jun Furuse
@camlspotter
検査はできても推論が決定不能な型システムはいくらもあるので、そういう文脈では区別はしてほしいです。例えばタソウ再帰は推論がムリポなので人が書いてあげて推論器は検査しかしないか、なんかヒューリスティックスを入れて一部の例は推論できるけど、それ以外はやっぱ夜露死苦みたいな;;
2011-05-02 19:56:37
おしいれのぼうけん
@osiire
@camlspoter @kazu_yamamoto MilnerのWの論文でもcheckとinferenceとinstantiationとassignmentが出てきますね。http://bit.ly/jVitoS
2011-05-02 20:11:40
おしいれのぼうけん
@osiire
@camlspotter @kazu_yamamoto 私は最初にcamlspotterさんが言ってた話で違和感なかったのですが...
2011-05-02 20:13:42
Atsushi Igarashi
@50storms
@osiire @camlspotter @kazu_yamamoto 文脈は全然理解してないのですが、プログラム中にどの程度型情報が入っているかという観点は考慮されておりますか？
2011-05-02 20:40:38
Atsushi Igarashi
@50storms
例えば、System F の type inference は簡単ですが、untyped term に対する2nd-order の型付けを考えた時の type inference/checking はともに決定不能です。
2011-05-02 20:45:38
Atsushi Igarashi
@50storms
Type inference/checking の定義は @camlspotter さんのが専門分野の中では標準的とされていると思います。
2011-05-02 20:47:47
Atsushi Igarashi
@50storms
@camlspotter それはありがちですね (ｰｰ;) っていうか、自分も(特に日本語文章だと)濫用してるかも。
2011-05-02 20:56:45
Atsushi Igarashi
@50storms
あと、Type assignment という用語はuntyped term (束縛変数の型が書いてない) が対象、というのが標準的だと思います。
2011-05-02 21:03:50
Atsushi Igarashi
@50storms
補足しておくと、inference/checking の違いに敏感なのは型システムのアルゴリズム的側面(決定可能性とか計算量)を問題にする時で、他の場面ではプログラミング言語の論文でもわりといい加減だと思います。
2011-05-02 21:27:49
Jun Furuse
@camlspotter
え？ウィキペの話なの？ QT @osiire: @kazu_yamamoto @camlspotter @50storms「OCamlは型推論を健全に保つことで型検査と同等の検査能力を実現している」という文章が妥当かと思いますが、どうなのでしょう。
2011-05-02 21:35:46
おしいれのぼうけん
@osiire
@camlspotter あ、いえ、Wikipediaの話ではなく、「OCaml には、型検査があるのか、ないのか、はっきりさせる」という意味で、「型検査がない」というとあまり適当ではない感じがして、じゃぁ、妥当な文章は何かなと思いまして。
2011-05-02 21:37:42
Nobuo Yamashita
@nobsun
ああなるほど．完全にぐちゃぐちゃに考えてた > orz儂 RT @camlspotter Γ |- e : τ が与えられたときそのデリベーションを探すのが型検査。Γ と e が与えられたときに型検査に通るような τ を探すのが型推論。嘘だったらゴメンナサイネー;;
2011-05-02 21:41:47
おしいれのぼうけん
@osiire
@kazu_yamamoto すみません、包含するというのが分かりませんが、Γ と e が与えられたときに型検査に通るような τ を探せて、それが正しいと考えられるなら、もう一度Γ |- e : τ の型検査をする必要はない気がします。
2011-05-02 21:45:37
Nobuo Yamashita
@nobsun
なるほど． RT: 補足しておくと、inference/checking の違いに敏感なのは型システムのアルゴリズム的側面(決定可能性とか計算量)を問題にする時で、他の場面ではプログラミング言語の論文でもわりといい加減だと思います。 (via @50storms)
2011-05-02 21:47:01