ATS の線形型は 観型 (viewtype) という名前です。 これは線形型は2つの部分から構成されることを示しています: 一つは観 (view)でもう一つが型 (type) です。 例えば、観 V と型 T が与えられた時、タプル (V | T) は観型で、バー記号 (|) は観と型を (コンマのように) 分離しています。 少し意外かもしれませんが、反対に: それぞれの観型 VT について、VT が (V | T) と等しいような 観 V と型 T の存在を仮定できます。 形式上、ATS ではこの T は VT?! として参照されます。 この幾分意外な線形型の解釈は ATS の目立った新規性です。 それは観型の線形性は 完全に その中に存在する観部分に由来することを強調しています。
ビルトインの種 viewtype と viewt@ype は、型部分がそれぞれ種 type と t@ype であるような観型を表わす静的な項です。 別の言い方をすると、前者にはポインタのサイズに等しいサイズの線形値の観型が割り当てられ、そして後者には詳細不明のサイズの線形値の観型が割り当てられます。 例えば、型と、種 viewtype の観型を作るアドレスを取るような、tptr は次のように定義されます:
型 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]
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]
クロージャ関数のような ATS プログラミングの機能を説明する能力は、ATS の型システムの表現力の説得力ある証拠です。