型推論と型検査、静的な型つけと動的な型つけ、強い型つけと弱い型つけ

ついでに追加。

型推論:変数や式の型をプログラマが宣言しなくても、言語処理系が文脈から推論してくれる機構。MLとかHaskellとか。

型検査:変数や式の型が合っていることを言語処理系が(普通は静的に)チェックしてくれる機構。CとかJavaとか、MLやHaskellも。

静的な型つけ:プログラムの実行前に型を検査する機構。MLとかHaskellとかCとかJavaとか。

動的な型つけ:プログラムの実行中に型を検査する機構。LispとかSchemeとかPerlとか。

強い型つけ:検査を通れば、安全さ(safety)が保証される、という(普通は静的な)型つけ。MLとかHaskellとかJavaとか。Javaはバグがあったりしたので少し怪しいですが。

弱い型つけ:検査を通っても、安全さ(safety)は保証されない、という型つけ。CとかPascalとか。

安全さ(safety):プログラムが言語仕様で定義されていない状態(Cのバッファオーバーフローとか)にならないこと。

型:プログラムの中の値の「種類」のこと。より正確にいうと、その値に対して、どのような操作が許可されているか、をあらわすもの。たとえばMLならstring型の値に対して掛け算はできないし、Stack.tをリストとして直接操作することはできない(たとえ実際の実装がリストでも)。

(広義の)多相性:単一のコードで複数の型を扱う処理が可能なこと。すべての型が同様に扱えるパラメタ的多相性(parametric polymorphism)、ある型に包含される型(subtype)のみ扱える部分型多相性(subtyping polymorphism)、一部の特定の型のみ扱える場当たり的多相性(ad hoc polymorphism)に分類できる。パラメタ的多相性の例としては、MLの多相型やC++のtemplate、JavaC#genericsなどがある。部分型多相性の例としては、オブジェクト指向の継承がメジャー。場当たり的多相性の例としては、多数の言語の四則演算(整数と浮動小数点数に使用可能)がある。

(狭義の)多相性:パラメタ的多相性のこと。

超遅追記:

陽な型つけ(explicit typing):CとかJava(の多くの部分)みたく、プログラマが変数や関数の型を書くような型つけ。

陰な/暗な型つけ(implicit typing):MLとかHaskell(の多くの部分)みたく、プログラマが変数や関数の型を書かなくても、型検査器が型推論してくれるような型つけ。

ちなみに「型つけ」(typing)は名詞。形容詞は「型つき」(typed)。だから「静的型を持つ言語」は「静的型つけ言語」じゃなくて「静的型つき言語」(例えば「型検査プログラム」と言ったら「型検査をするプログラム」であって「型検査されたプログラム」にはならないのと同様)。

追記の追記:「無農薬栽培リンゴ」は「無農薬栽培されたリンゴ」じゃないか、との鋭い指摘。まあすでに確立されている用語をできるだけ使ってください…>皆様

追記3:「タグ付きデータ」と「タグ付けデータ」のほうが良い例だったかも。