型 T とアドレス L が与えられた時、 最初の段階で観 T@L の証明はどのように得られるのでしょうか？ 実際にそのような証明を得る方法は様々です。 次のようにローカルの値としてスタックに確保する方法を紹介します。
次の関数 foo の本体では、 いくつかのスタックに確保されたローカルな値が宣言されています:
fn foo (): void = let var x0: int // view@(x0): int? @ x0 val () = x0 := 0 // view@(x0): int(0) @ x0 var x1: int = 1 // view@(x1): int(1) @ x1 // // [with] is a keyword in ATS // var y: int with pfy // pfy is an alias of view@(y): int? @ y val () = y := 2 // pfy = view@(y): int(2) @ y var z: int with pfz = 3 // pfz is an alias of view@(z): int(3) @ z in // nothing end // end of [foo]
キーワード var はローカルな値の宣言です。 値は宣言された時、その型またはその初期値を与える必要があります。 もし値が型をともなわずに宣言されたら、その初期値の型がその型であると見なされます。 値 x が型 T で宣言されていたと仮定しましょう。 するとその値の位置を指すポインタは addr@(x) で表わされ、関連した (駐観の) 線形の証明は view@(x) で表わされます。 このとき addr@ と view@ はキーワードです。 値は ATS における左辺値のもう一つの形です。 foo の本体では、x0 が型 int の値として宣言されて整数0で初期化されます; x1 が型 int の値として宣言されて初期値1が与えられます; pfy が view@(y) の別名として導入されているとき、 y が型 int の値として宣言されて整数2で初期化されます; pfz が view@(z) の別名として導入されているとき、 z が型 int の値として宣言されて初期値3が与えられます。
次のコードは階乗関数の実装です:
fn fact{n:nat} (n: int (n)): int = let fun loop{n:nat}{l:addr} .<n>. (pf: !int @ l | n: int n, res: ptr l): void = if n > 0 then let val () = !res := n * !res in loop (pf | n-1, res) end // end of [if] // end of [loop] var res: int with pf = 1 val () = loop (pf | n, addr@res) // addr@res: the pointer to res in res end // end of [fact]
loop を実行している間、res の値は中間結果を保持していることに注意してください。 res はスタックに確保されるので、 fact 呼び出しが評価された後にゴミが生成されることはありません。 C言語でこのスタイルのプログラミングをする時、fact 呼び出しが返った後に res を指すポインタがデリファレンスされてしまう不安がしばしばあります。 これは一般に、宙ぶらりんなポインタのデリファレンス (derefencing a dangling pointer) と呼ばれます。 ATS ではこの不安は完全に取り除かれています。 変数 res に関連する駐観の線形証明は、res のスコープが終わるまで存在することが ATS の型システムによって要求されます。 より具体的には、もし型 T の変数 x が宣言されていたら、L がアドレス x のとき観 T?@L の線形証明は、x のスコープの終わりに型検査が到達するまで有効でなければなりません。 この要求は、確保されたスタックの割り当てが終わった後、もはや変数にアクセスできないことを保証します。 その変数に関連した駐観の線形証明がその時点では無効なのです。
ATS の配列もまたスタックに確保できます。 例えば、次のコードは関数 main0 のスタックフレームに double の2つの配列を確保します。 それからそれらを dotprod に渡してドット積を計算します:
implement main0 () = { // var A = @[double][3](1.0) // initialized with 1.0, 1.0, 1.0 var B = @[double](1.0, 2.0, 3.0) // initialized with 1.0, 2.0, 3.0 // val () = println! ("A * B = ", dotprod (A, B)) // A * B = 6.0 // } (* end of [main0] *)
関数の呼び出しフレーム中に大きな配列確保するのは良い慣習とは言えないことに注意してください。 実行時にスタックオーバーフローが非常に発生しやすくなります。
ATS では、関数の呼び出しフレーム内にクロージャを確保することもできます。 例えば、次のコードは bar という名前でスタックに確保された変数にフラットなクロージャ関数を置く foo という名前の関数を実装しています:
fun foo ( x: int, y: int ) : int = let // var bar = lam@ (): int => x * y // in bar () end // end of [foo]
fun foo2 ( x: int, y: int ) : int = let // var bar2 = fix@ f (x: int): int => if x > 0 then y + f(x-1) else 0 // in bar2 (x) end // end of [foo]
動的なメモリ確保が使えない状況下では、スタックに確保されたクロージャは高階関数を使ったプログラミングをサポートする極めて重要な存在です。