型検査と型推論

山本和彦 @kazu_yamamoto

専門家間の厳密な定義と、一般人への分かり易い表現は、分けて考えるべき。一致していれば幸福だけど。型推論と行った場合、型検査も含んでいると、一般の人が思ってくれるかどうか。。。型検査の一要素が型推論と思われているのではないか。。。。

おしいれのぼうけん @osiire

なるほど、型アノーテーションの強制箇所と型付け規則の性質が良くて型推論が単一化問題に落とせるなら、型推論は型検査の機能も持ちつつ推論もできるという機能包含関係になるんですね。

Jun Furuse @camlspotter

@kazu_yamamoto 型推論の仕事は、検査に通る適切な型を自動的に探す事、と言えば問題ないでしょう。さすれば、検査を通らないような型付を求める推論器はおかしい、とか、検査に通るような型付があるのに推論器の力が足りなくて推論してくれない、とかも理解できるはず。

Jun Furuse @camlspotter

まあ、偶然今日のブローグにも書きましたけど、こんな事区別してもしなくても正しい型推論器は正しい型付できるプログラムしか通しませんから、ぶっちゃけ気にしなくていいですよ。それよりコメント書いてくださいよ頼みますよお願いしましたよ本気で。

Jun Furuse @camlspotter

プログラムの各場所から型間の満たすべき制約を集めてきて解く、解があればオッケー、解が無ければ型エラー、解があるか無いか判らなければもっと型をクレロン、というのが型推論

Jun Furuse @camlspotter

そんなん推論とちゃうやん。 Inference ちゃうやん。自明やン。 int x; なら &x : int* と同じレベルやン。 (ノ｀Д´)ノ

Jun Furuse @camlspotter

そんなん型推論とか言ってたら ML とか触ったらショックで死んでしまうデ

Jun Furuse @camlspotter

型推論…つまり、それは……型制約と型制約の鬩ぎ合いだ!!

山本和彦 @kazu_yamamoto

.@camlspotter 関数型の利点で型推論があるというのは止めませんか？ 型を厳密に検査する機能と型を推測する機能があるって方が分かり易いと思います。型推論という言葉は、専門家の押しつけのような気がしてきました。

山本和彦 @kazu_yamamoto

infer と deduce と reasoning の違いがよく分からない！

Jun Furuse @camlspotter

そんなメンドクサイ。型推論。モナド。何か問題でも？ QT @kazu_yamamoto: .@camlspotter 関数型の利点で型推論があるというのは止めませんか？ 型を厳密に検査する機能と型を推測する機能があるって方が分かり易いと思います。

Jun Furuse @camlspotter

モナドやアプリカティブ、背景ははっきり説明できない人でも、みんな使ってプログラムを書けている。型システムの健全性、推論アルゴリズムの決定可能性、知らなくても型システムの恩恵は受ける事ができる。キャッチーなキーワードとして使えば問題ない。

Jun Furuse @camlspotter

モナドはモナド則を知っていると新しいモナドを作成できて嬉しい。型推論も(MLであれば)型の単一化とか知っていれば型エラーの意味が把握しやすい。でも知らないからといってモナドやMLを使えないわけではないし門前払いするわけでもない。

Jun Furuse @camlspotter

モナディックプログラミングも型システムも、アカデミックペーパーを書くなら、それこそ専門家レベルの知識が必要なのは言うまでもないが、別にユーザーにはそれは押し付けてはいないですよ。

Jun Furuse @camlspotter

Haskell だとモナドがあって便利! とか、強い型付言語で型推論があると便利! とか言いたければ、モナドって何ですか？型推論って何ですか？とか言われた時にそれなりに答えられるようにしといたほうがカッコいいかなあ

m2ym @m2ym

大堀先生の本にもTAPLにも型検査(Type checking）の厳密な定義が書かれていないようですが（少なくともIndexには）、与えられたΓ, e, τに対してΓ|-e:τとなる型判定が存在するかどうかを型検査問題とするならば、この問題は型推論問題の特殊ケースと考えられます

m2ym @m2ym

（一般化された）型推論問題とは、与えられたeに対して{(Γ,τ)|Γ|-e:τ}となる型判定の集合を見つけ出す問題です（大堀先生の本より。若干記述が異なります）。つまり、型検査問題とは型推論問題の特殊ケースと言えると思います