ATSプログラミング入門:
PrevChapter 14. 線形なデータ命題としてのデータ観 (dataview)Next

選言的な観

データ観 VOR は次のように宣言されています: 

dataview VOR (v0:view+, v1:view+, int) =
  | VORleft (v0, v1, 0) of (v0) | VORright (v0, v1, 1) of (v1)

この宣言はデータ観 VOR が1番目と2番目の引数について共変であることを示しています。 そして関連する2つの証明コンストラクタ VORleft と VORright があります。 観 V0 と V1 が与えられた時、 VOR(V0, V1, 0) の証明は V0 の証明になります。 また VOR(V0, V1, 1) の証明は V1 の証明になります。

なんらかの型 T を考えます。次の関数インターフェイスは getopt が未初期化のポインタを取り、ポインタが初期化されたかどうかを示す整数を返すことを表わしています: 

fun getopt{l:addr}
  (pf: T? @ l | ptr (l)): [i:int] (VOR (T? @ l, T @ l, i) | int (i))

次のコードは getopt の典型的な使用例を示しています: 

fun foo (): void = let
  var x: T?
  val (pfor | i) = getopt (view@(x) | addr@(x))
in
//
if i = 0
  then let
    prval VORleft (pf0) = pfor in view@(x) := pf0 // uninitialized
  end // end of [then]
  else let
    prval VORright (pf1) = pfor in view@(x) := pf1 // initialized
  end // end of [else]
// end of [if]
//
end // end of [foo]

ATS には、型 T とブール B を取り、opt 型 opt(T, B) を作るような型コンストラクタ opt があります。 このとき B が true ならば opt(T, B) は T に等しく、B が false ならそれは T? に等しくなります。 関数 getopt には次のような opt 型を使ったインターフェイスを与えることができます: 

fun getopt (x: &T? >> opt (T, b)): #[b:bool] bool(b)

これで getopt 呼び出しコードは次のように実装できます: 

fun foo (): void = let
  var x: T?
  val ans = getopt (x)
in
//
if (ans)
  then let
    prval () = opt_unsome(x) in (*initialized*)
  end // end of [then]
  else let
    prval () = opt_unnone(x) in (*uninitialized*)
  end // end of [else]
// end of [if]
//
end // end of [foo]

このとき、証明関数 opt_unsome と opt_unnone には次の型が割り当てられています: 

prfun opt_unsome{a:t@ype} (x: !opt (a, true) >> a): void
prfun opt_unnone{a:t@ype} (x: !opt (a, false) >> a?): void

VOR を使うバージョンと比較して、 opt 型を用いたこのバージョンはかなりすっきりしています。

PrevHomeNext
線形なデータ命題としてのデータ観 (dataview)Up線形配列のデータ観