おそらく、ATS 開発の背後にある最も大きな動機は、ATS をオペレーティングシステムのカーネルの中で実行される安全で信頼できるプログラムを効果的に構築できるようなプログラミング言語にしたいという要求です。 一見したところ自然なアプローチは、C言語の "安全な" サブセットを苦心して作り上げることに集中したり、C言語の "安全でない" プログラミングの機能のラッパーを作ったりすることでしょう。 このようなアプローチの代わりに、ATS は定理証明によるプログラミングのパラダイムを信頼しています。 このおかげで、メモリのようなリソースが誤って使用されたり誤って処置されたりするのを防ぐことができます。 一般化と柔軟性を両立した安全性のためにこのアプローチを支持しています。 例えば、ATS ではポインタ演算がサポートされているにもかわらず、ATS で構築された型付けされたプログラムは実行時にバッファオーバーランを引き起しません。 より具体的には、もしポインタがデリファレンスされると、ATS はデリファレンス操作の安全性を実証するような証明を要求します。 このような証明は線形命題の正当性を立証することで構築されます。 この線形命題は ATS では観 (view) と呼ばれ、リソースおよび性能を分類します。
この章で紹介するコードは オンライン から入手できます。
観は命題 (prop) の線形バージョンです。 線形 (linear) という単語は、Jean-Yves Girard によって考案されたリソースを意識した論理である線形論理に由来します。 観を表わす静的な項のためにビルトインの種 view があります。 型 T とメモリ位置 L が与えられた時、T@L という観を作ることができ、 これは型 T の値が位置 L にあるメモリに格納されていることを示しています。 @ は中置の特殊演算子です。 この形の観は実用上非常に一般的で、それらはしばしば駐観 (at-view) と呼ばれます。 例として、次の関数テンプレート ptr_get0 と ptr_set0 は、与えられたポインタを通して読み書きをし、駐観を含む型が割り当てられています:
// fun{a:t@ype} ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a) // fun{a:t@ype} ptr_set0 {l:addr} (pf: a? @ l | p: ptr l, x: a): (a @ l | void) //
ptr は型コンストラクタで、種 addr の静的な項 L に適用されると型 ptr(L) を作ることに注意してください。 型 ptr(L) の唯一の値は L によって示された位置を指すポインタです。
型 T が与えられた時、関数 ptr_get0<T> には次の型が割り当てられます:
これは観 T@L の証明とどこか L について型 ptr(L) のポインタに適用すると、関数 ptr_get0<T> が観 T@L の証明と型 T の値を返すことを示しています。 直感的に言うと、T@L が線形であるようなリソースである観 T@L の証明は、ptr_get0<T> に渡された時に 消費 (consumed) されます。 さらに同じ観 T@L の別の証明が ptr_get0<T> が返る時に生成されます。 観 T@L の証明が返らなければならないことに注意してください。 さもなければ後続のメモリ位置 L へのアクセスは不可能になります。同様に、関数 ptr_set0<T> には次の型が割り当てられます:
T? は未初期化であることを仮定したサイズ sizeof(T) の値のための型であることに注意してください。 関数 ptr_set0<T> は、観 T?@L の証明と型 ptr(L) のポインタ、型 T の値に適用されると、観 T@L の証明を返します。 観 T?@L の使用は、ptr_set0<T> が呼び出された時に、L のメモリ位置が未初期化であると仮定されていることを示しています。
例として、与えられた2つの位置にあるメモリコンテンツをスワップする関数テンプレート swap0 は次のように実装されます:
fn{a:t@ype} swap0 {l1,l2:addr} ( pf1: a @ l1, pf2: a @ l2 | p1: ptr (l1), p2: ptr (l2) ) : (a @ l1, a @ l2 | void) = let val (pf1 | x1) = ptr_get0<a> (pf1 | p1) val (pf2 | x2) = ptr_get0<a> (pf2 | p2) val (pf1 | ()) = ptr_set0<a> (pf1 | p1, x2) val (pf2 | ()) = ptr_set0<a> (pf2 | p2, x1) in (pf1, pf2 | ()) end // end of [swap0]
対応するC言語の実装と比較して、ATSでのこの実装が冗長であることは明白です。 特に、リソースを使用する関数の呼び出しを通じて、線形の証明が 分断 されてしまうため、 多くの 管理上の コードを書くことになってしまいます。 ここで、このような管理上のコードの必要性を大きく緩和するために、いくつか特別な構文を紹介します。
関数テンプレート ptr_get1 と ptr_set1 は次のようなインターフェイスを持ちます:
// fun{a:t@ype} ptr_get1 {l:addr} (pf: !a @ l >> a @ l | p: ptr l): a // fun{a:t@ype} ptr_set1 {l:addr} (pf: !a? @ l >> a @ l | p: ptr l, x: a): void //
fn{a:t@ype} swap1 {l1,l2:addr} ( pf1: !a@l1, pf2: !a@l2 | p1: ptr l1, p2: ptr l2 ) : void = let val x = ptr_get1<a> (pf1 | p1) val () = ptr_set1<a> (pf1 | p1, ptr_get1<a> (pf2 | p2)) val () = ptr_set1<a> (pf2 | p2, x) in // nothing end // end of [swap1]
swap1 のさらに簡単な実装は次のようになります:
どこか L について型 ptr(L) のポインタ p が与えられた時、!p はメモリ位置 L に保存された値を生じます。 !p を型検査すると、型検査器はまずはじめに現在有効な全ての証明の中で T について 観 T@L の証明を検索します: もしそのような証明 pf が見つかったら、!p は本質的に ptr_get1(pf | p) に詳細化されて、型検査は終わります。 !p が左辺値 (詳細は後に説明します) である場合、 なんらかの値 v について !p := v のような割り当てで使うこともできます。 もし現在有効な全ての証明の中である型 T について駐観 T@L の証明が見つかれば、 型検査器は型検査のために !p := v を ptr_set1(pf | p, v) に詳細化します。 swap1 のこの実装は線形の証明を明示的に扱うための管理上のコードを使っていないことに注意してください。