静的型付けと動的型付け

静的型付けはプログラム実行前に型をチェックする一方、動的型付けは実行中にチェックします。段階的型付けは、この2つを1つの言語内で組み合わせようとします。

Definition

静的型付けは、コンパイル時に型制約を検証し、適切に型付けされたプログラムが実行前に受け入れられるようにします。動的型付けは、型チェックを実行時まで延期し、不適切な型の値に操作が適用されたときにエラーを発生させます。

Scope

このトピックでは、型チェックがいつ、どのように行われるかという範囲を扱います。コンパイル時に不正な型のプログラムを拒否する静的チェック、実行時に型エラーを検出する動的チェック、そして両者の共存を可能にする段階的またはオプションの型付けです。それぞれの保証、柔軟性、パフォーマンスへの影響、および型チェック規律の健全性について説明します。

Core questions

• 静的チェックが防止できるエラーのクラスで、動的チェックでは事前に防止できないものは何ですか？
• 動的型付けはどのような柔軟性を提供し、その代償は何ですか？
• 段階的型付けは、型付けされたコードと型付けされていないコードをどのように健全に混在させることができますか？
• 静的型規律の健全性はどのように確立されますか？

Key theories

段階的型付け

SiekとTahaは、プログラムの一部を静的に型付けし、他の部分を動的に型付けすることを可能にする型システムを定義しました。このシステムでは、境界での安全な相互作用を管理する一貫性関係が規定されています。

静的型付けの健全性

WrightとFelleisenの進行と保存のメソッドは、健全な静的型システムが、適切に型付けされたプログラムが停止状態に陥ることがないことを保証することを示し、静的チェックの安全性を形式化しました。

Clinical relevance

静的型付けと動的型付けの選択は、開発者のワークフロー、ツール、および信頼性を形成します。動的言語に重ねて実装されるような段階的およびオプションの型付けシステムは、チームが既存の大規模なコードベースに静的な保証を段階的に追加することを可能にします。

History

初期の言語は、静的型付け（Algol、Pascal、ML）と動的型付け（Lisp、Smalltalk）の系統に分かれていました。動的言語が生産性のために人気を博すにつれて、研究者たちはこれらのアプローチを調和させようとしました。SiekとTahaによる2006年の段階的型付けと、同時期のオプション型に関する研究は、動的言語の上に構築された広く使用されている段階的型付けシステムにつながりました。

Debates

段階的型付けのコストと健全性

研究者たちは、健全な段階的型付けが、型付けされたコードと型付けされていないコードの境界での法外な実行時チェックコストを回避できるかどうか、また、健全ではない「オプションの」型付けがより良い実用的なトレードオフであるかどうかについて議論しています。

Key figures

• Benjamin Pierce
• Jeremy Siek
• Walid Taha
• Matthias Felleisen

Seminal works

• pierce2002
• siek2006
• wright1994

Frequently asked questions

静的型付けは常に動的型付けよりも優れていますか？

どちらか一方が常に優れているわけではありません。静的型付けはより多くのエラーを早期に検出し、ツールを支援しますが、動的型付けは柔軟性と迅速なプロトタイピングを提供します。したがって、適切な選択はプロジェクトの信頼性と俊敏性のニーズに依存します。

段階的型付けとは何ですか？

段階的型付けは、単一のプログラム内で静的に型付けされた部分と動的に型付けされた部分を混在させることができます。境界で実行時チェックを挿入することで、型付けされたコードはその保証を維持し、型付けされていないコードは柔軟性を保ちます。