強い型付けと弱い型付け

コンピュータプログラミングでは、プログラミング言語を口語的に分類する方法は数多くありますが、その 1 つに、言語の型システムが強い型付けか弱い型付け(緩い型付け) かというものがあります。しかし、これらの用語が何を意味するかについての正確な技術的定義はなく、用語の暗黙の意味や、主流のプログラミング言語の型システムの「強さ」の相対的な順位については、著者によって意見が分かれています。^{[1]このため、型システムについて明確に記述したい著者は、「強い型付け」や「弱い型付け」という用語を避け、「}型安全性」などの具体的な表現を好んで使用します。

一般的に、強く型付けされた言語はコンパイル時に厳密な型付け規則を持ちます。つまり、コンパイル中にエラーや例外が発生する可能性が高くなります。これらの規則のほとんどは、変数の割り当て、関数の戻り値、プロシージャの引数、関数の呼び出しに影響します。動的型付け言語 (実行時に型チェックが行われる言語) も強く型付けできます。動的型付け言語では、変数ではなく値に型があります。

弱く型付けされた言語は型付けのルールが緩く、予測できない結果や誤った結果が生成されたり、実行時に暗黙の型変換が行われたりすることがあります。 ^[2]異なるが関連する概念として、潜在的型付けがあります。

1974年、バーバラ・リスコフとスティーブン・ジルズは、強く型付けされた言語を「呼び出し関数から呼び出される関数にオブジェクトが渡されるときは常に、その型は呼び出される関数で宣言された型と互換性がなければならない」と定義しました。^[3] 1977年、K.ジャクソンは「強く型付けされた言語では、各データ領域は異なる型を持ち、各プロセスはこれらの型に基づいて通信要件を記述します」と書いています。^[4]

さまざまな言語設計上の決定が、「強い」型付けまたは「弱い」型付けの証拠として言及されてきました。これらの多くは、より正確には、型安全性、メモリ安全性、静的型チェック、または動的型チェックの有無として理解されています。

「強い型付け」とは、一般的に、コードの不変条件を捕捉し、その正確性を確保し、特定の種類のプログラミング エラーを確実に排除するために、プログラミング言語の型を使用することを指します。したがって、これらの目標を達成するために使用される「強い型付け」の規律は数多くあります。

一部のプログラミング言語では、ある型の値を別の型の値であるかのように簡単に使用できます。これは、「弱い型付け」と呼ばれることもあります。

例えば、Aahz Maruch は次のように指摘しています。「強制は、静的に型付けされた言語があり、その言語の構文機能を使用して、ある型を別の型であるかのように強制的に使用する場合に発生します ( Cでの void* の一般的な使用を考えてみましょう)。強制は通常、弱い型付けの症状です。一方、変換は、適切な型のまったく新しいオブジェクトを作成します。」^[5]

別の例として、GCCはこれをtype-punningと呼び、厳密なエイリアシングが破られると警告しています。Thiago Macieiraはtype-punningによってコンパイラが不適切な最適化を行う際に発生する可能性のあるいくつかの問題について説明しています。^[6]

暗黙的な型変換を許可する言語の例は数多くありますが、その方法は型安全です。たとえば、C++とC# はどちらも、プログラムで演算子を定義して、明確に定義されたセマンティクスを使用して値をある型から別の型に変換できます。C++ コンパイラは、このような変換を検出すると、その操作を関数呼び出しと同様に扱います。一方、値を C 型void*に変換する操作は、コンパイラには見えない安全でない操作です。

一部のプログラミング言語では、ポインタを数値のように公開し、ユーザーがその上で演算を実行できるようにします。これらの言語は、ポインタ演算を使用して言語の型システムを回避できるため、「弱い型付け」と呼ばれることもあります。

一部のプログラミング言語では、タグなしユニオンがサポートされており、これにより、ある型の値を別の型の値であるかのように表示できます。

Luca Cardelliの論文Typeful Programmingでは、^[7]「強力な型システム」は未チェックの実行時型エラーの可能性がないシステムとして説明されています。他の文献では、未チェックの実行時エラーがないことを安全性または型安全性と呼んでいます。Tony Hoareの初期の論文では、この特性をセキュリティと呼んでいます。^[8]

これらの定義の中には矛盾するものもあれば、単に概念的に独立しているものもあり、さらに他の定義は他のより「自由な」(それほど強力ではない) 定義の特別なケース (追加の制約付き) です。これらの定義には大きな相違があるため、ほとんどのプログラミング言語は強く型付けされているか弱く型付けされているかのいずれかであるという主張を擁護できます。たとえば、次のようになります。

• Java、Pascal、Ada、C では、変数に宣言された型が必要であり、算術値を他の算術型に明示的にキャストする機能をサポートしています。Java、C#、Ada、Pascal は、C よりも型が強いと言われることがあります。これは、C ではより多くの種類の暗黙的な変換がサポートされ、ポインタ値を明示的にキャストできるのに対し、Java と Pascal ではできないためです。Java の静的型システムを回避する方法は、Java 仮想マシンの型システムによって制御されるため、Java は Pascal よりも型が強いと考えられます。C# と VB.NET はその点で Java に似ていますが、コード セグメントを明示的に「安全でないコンテキスト」に配置することで、動的型チェックを無効にすることができます。Pascal の型システムは「強すぎる」と評されてきました。配列や文字列のサイズがその型の一部であるため、一部のプログラミング タスクが非常に困難になるからです。ただし、Delphi ではこの問題は修正されています。^{[9] [10]}
• Smalltalk、Ruby、Python、Selfはすべて、実行時に型指定エラーが防止され、暗黙的な型変換がほとんど行われないという意味で「強く型付け」されていますが、これらの言語は静的型チェックを使用しません。つまり、コンパイラは型制約ルールをチェックまたは強制しません。ダック タイピングという用語は、現在、このグループの言語で使用される動的型指定パラダイムを説明するために使用されます。
• Lisp系の言語はすべて、実行時に型エラーが防止されるという意味で「強く型付け」されています。Common LispやClojureなどの一部の Lisp 方言は、さまざまな形式の型宣言^[11]をサポートしており、一部のコンパイラ ( CMU Common Lisp (CMUCL) ^{[12]および関連コンパイラ) は、これらの宣言を}型推論と組み合わせて使用​​して、さまざまな最適化と限定された形式のコンパイル時型チェックを有効にします。
• 標準の ML、F#、OCaml、Haskell、Go、Rustは静的に型チェックされますが、コンパイラはほとんどの値に対して正確な型を自動的に推論します。
• アセンブリ言語とForth は、型なし言語として特徴付けられます。型チェックは行われず、関数に渡されるデータが適切な型であることを確認するのはプログラマーの責任です。

• プログラミング言語の比較
• データ型には、型付けの問題に関するより詳細な説明が含まれています。
• 契約による設計（暗黙の契約形式としての強い型付け）
• 潜在的タイピング
• メモリの安全性
• 型安全性
• 型システム
• 厳密に型指定された識別子