観と型を組み合わせた観型

ATS の線形型は 観型 (viewtype) という名前です。 これは線形型は2つの部分から構成されることを示しています: 一つは観 (view)でもう一つが型 (type) です。 例えば、観 V と型 T が与えられた時、タプル (V | T) は観型で、バー記号 (|) は観と型を (コンマのように) 分離しています。 少し意外かもしれませんが、反対に: それぞれの観型 VT について、VT が (V | T) と等しいような 観 V と型 T の存在を仮定できます。 形式上、ATS ではこの T は VT?! として参照されます。 この幾分意外な線形型の解釈は ATS の目立った新規性です。 それは観型の線形性は 完全に その中に存在する観部分に由来することを強調しています。

ビルトインの種 viewtypeviewt@ype は、型部分がそれぞれ種 typet@ype であるような観型を表わす静的な項です。 別の言い方をすると、前者にはポインタのサイズに等しいサイズの線形値の観型が割り当てられ、そして後者には詳細不明のサイズの線形値の観型が割り当てられます。 例えば、型と、種 viewtype の観型を作るアドレスを取るような、tptr は次のように定義されます:

vtypedef tptr (a:t@ype, l:addr) = (a @ l | ptr l)

型 T とアドレス L が与えられた時、観型 tptr(T, L) は L に格納された型 T の値を示す線形の証明とペアになった L のポインタです。 カウントを表わす整数を指すポインタを示す証明とペアになったポインタとしてのカウンタのことを考えるなら、 次に定義する関数 getinc は与えられたカウンタを1増やした後、現時点でのカウントを返します:

fn getinc {l:addr}{n:nat} ( cnt: !tptr (int(n), l) >> tptr (int(n+1), l) ) : int(n) = n where { val n = ptr_get1<int(n)> (cnt.0 | cnt.1) val () = ptr_set1<int(n+1)> (cnt.0 | cnt.1, n+1) } (* end of [getinc] *)

次は観型の特に興味深い例です:

vtypedef cloptr (a:t@ype, b:t@ype, l:addr) = [env:t@ype] (((&env, a) -> b, env) @ l | ptr l) // end of [cloptr_app]

2つの型 A と B が与えられた時、型 A の値を取り型 B の値を返すようなクロージャ関数が保管されたアドレス L を指すポインタには観型 cloptr(A, B, L) を与えることができます。 クロージャ関数は、外から導入されたクロージャ関数本体内の値の束縛を含む環境とペアになった単なる無環境関数であることに注意してください。 関数型 (&env, a) -> b において、記号 & は対応する関数の引数が参照で渡されていることを示しています。 つまり、この引数は左辺値であることが要求されていて、実行時に実際に渡されるものは左辺値のアドレスです。 参照渡し (call-by-reference) については別の章でより詳細に解説します。 次のコードは与えられた引数で呼び出されるクロージャ関数へのポインタを説明しています:

fun{ a:t@ype}{b:t@ype } cloptr_app {l:addr} ( pclo: !cloptr (a, b, l), x: a ) : b = let val p = pclo.1 (* // // taking out pf: ((&env, a) -> b, env) @ l // prval pf = pclo.0 // *) val res = !p.0 (!p.1, x) (* prval () = pclo.0 := pf // putting the proof pf back *) in res end // end of [cloptr]

(構文 !p で表わされた) p のデリファレンスが型検査を通すために、pclo 内の線形の証明がはじめに取り出されることに注意してください。 そして pclo の型が元の位置に復帰されて返ります。 このレコードからの線形証明の取り出しとレコードへの復帰は ATS の型検査器によって自動的に行なわれます。

クロージャ関数のような ATS プログラミングの機能を説明する能力は、ATS の型システムの表現力の説得力ある証拠です。