translate/Web/cs.likai.org/ats/ml-programmers-guide-to-ats.md at master · jats-ug/translateATSでは、3つの世界でプログラミングをすることを覚えておくと良いでしょう。 Dynamics(動的な世界): プログラムを実行した時に評価される部分です。これは既存のプログラミング言語に馴染んだプログラマにとってもっとも親しみ深い部分でしょう。 Proofs(証明の世界): 動的な特性を静的な特性に結びつけます。Proofs(証明)はプログラムの動的な部分と考えることができます。しかし証明はコンパイル後では消滅してしまい、実行時には存在しません。コンパイラはあなたが書いた証明を検査し、動作可能なコードを生成する前に削除するのです。 Statics(静的な世界): 型検査時にコンパイラによって評価される部分です。静的な部分では静的な式の評価は常に終了しなければなりません。そのため型検査は決定可能です。 ATSの前身であるDependent MLでは、静的な世界からは依存型を通して動的な世界
The Ur Programming Language Family
