動的に型付けされた言語と静的に型付けされた言語について、大騒ぎがありました。しかし、私の目には、静的に型付けされた言語を使用すると、コンパイラ (またはインタプリタ) はユーザーの意図についてもう少し知ることができますが、伝えられることの表面をかろうじてかじっただけにすぎません。実際、一部の言語には、注釈でもう少し情報を提供するための直交メカニズムがあります。
私は Agda や Coq のような強く型付けされた言語を知っています。私はそれらにあまり興味がありません。むしろ、あなたが意図していることについてコンパイラーに説明できることの豊かさを拡張する言語または理論が存在するのだろうかと思っています。たとえば、可変ベクトルがあり、それを単位ベクトルに変換する場合、コンパイラは、計算コストの高い一般的な形式ではなく、ベクトル射影の単位ベクトル形式を選択できなかったのはなぜでしょうか? 型は変更されていません-必要なすべての型を構築するために必要な作業は、Haskellなどの驚くほど簡単な型付けを備えた言語でさえ不快です-それでも、コンパイラーは多くのことを知ることができるように思われます.状況について。
標準的な型理論の外部またはより高度なブランチのいずれかで、一部の言語はすでにこのようなことを可能にしていますか?