translate/Web/cs.likai.org/ats/ml-programmers-guide-to-ats.md at master · jats-ug/translate
ATSでは、3つの世界でプログラミングをすることを覚えておくと良いでしょう。 Dynamics(動的な世界): プログラムを実行した時に評価される部分です。これは既存のプログラミング言語に馴染んだプログラマにとってもっとも親しみ深い部分でしょう。 Proofs(証明の世界): 動的な特性を静的な特性に結びつけます。Proofs(証明)はプログラムの動的な部分と考えることができます。しかし証明はコンパイル後では消滅してしまい、実行時には存在しません。コンパイラはあなたが書いた証明を検査し、動作可能なコードを生成する前に削除するのです。 Statics(静的な世界): 型検査時にコンパイラによって評価される部分です。静的な部分では静的な式の評価は常に終了しなければなりません。そのため型検査は決定可能です。 ATSの前身であるDependent MLでは、静的な世界からは依存型を通して動的な世界
Generalized Algebraic Data Types in ATS
Bluish Coder Programming Languages, Martials Arts and Computers. The Weblog of Chris Double. The ATS programming language supports defining Generalized Algebraic Data Types (GADTS). They allow defining datatypes where the constructors for the datatype are explicitly defined by the programmer. This has a number of uses and I'll go through some examples in this post. GADTs are sometimes referred to
Sorts, Statics, and Dynamics in ATS
This post explores the hierarchical types in ATS programming languages. Explains sorts, statics, types, and dynamics in ATS with examples.Note: this is moved from my old blog. This is an interesting talk given by my adviser Prof. Xi. And I will try my best to put the ideas here in a proper way. Type Systems in a Word Type systems are systems about types. They have basic types, complex types, and t
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://www.ats-lang.org/MYDATA/Xanadu-lics00.pdf
Index
