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

ついでに追加。

型推論：変数や式の型をプログラマが宣言しなくても、言語処理系が文脈から推論してくれる機構。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、JavaやC#のgenericsなどがある。部分型多相性の例としては、オブジェクト指向の継承がメジャー。場当たり的多相性の例としては、多数の言語の四則演算（整数と浮動小数点数に使用可能）がある。

（狭義の）多相性：パラメタ的多相性のこと。

超遅追記：

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

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

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

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

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