ATSプログラミング入門:
PrevChapter 15. 線形データ型としてのデータ観型 (dataviewtype)Next

線形リスト

線形リストはデータ観 slist_v で表現された片方向リストと本質的に同じです。 けれども、以前の実装ではできなかったリストノードのメモリ確保と解放が可能になります。 次の宣言は線形データ型 list_vt を導入しています。 これは型と整数に適用されると、(viewtype である) ボックス型を作ります: 

datavtype
list_vt (a:t@ype+, int) =
  | list_vt_nil (a, 0) of ()
  | {n:nat}
    list_vt_cons (a, n+1) of (a, list_vt (a, n))
// end of [list_vt]

型 T と整数 I が与えられた時、list_vt(T, I) は、それぞれの要素が型 T である長さ I の線形リストを表わします。

あるデータ観型に関連する foo という名前のデータコンストラクタあると仮定しましょう。 すると、n が foo のアリティのとき、n+1 個のアドレスを取り観型 (viewtype) を作るような、一致する foo_unfold という名前の観型コンストラクタがあります。 例えば、観型コンストラクタ list_vt_cons_unfold は3つのアドレス L0, L1, L2 を取り、観型 list_vt_cons_unfold(L0, L1, L2) を作ります。 この観型は、リストノードが L0 に配置されていて、list_vt_cons の2つの引数が L1 と L2 に配置されているような、list_vt_cons を呼び出して作られたリストノードを表わします。 このとき L1 と L2 に関連する駐観の証明は現在有効な証明として保管されます。

次の関数テンプレート length は与えられた線形のリストの長さを計算します: 

fn{
a:t@ype
} length{n:nat}
  (xs: !list_vt (a, n)): int n = let
  fun loop
    {i,j:nat | i+j==n} .<i>.
    (xs: !list_vt (a, i), j: int j): int (n) =
    case+ xs of
    | list_vt_cons (_, xs1) => loop (xs1, j+1) | list_vt_nil () => j
  // end of [loop]
in
  loop (xs, 0)
end // end of [length]

length インターフェイスは、型 list_vt(T, I) のリストに適用されると、length<T> が I に等しい整数を返すことを示しています。 このとき T と I はそれぞれ型と整数です。 関数引数の型の前にある記号 ! は、その引数が値渡しで関数呼び出しが完了した後も保持されることに注意してください。 length の本体内の関数 loop は末尾再帰です。 線形のリストと整数が与えられた時、loop はそのリストの長さとその整数の和を返します。 loop の本体において、もし xs が パターン list_vt_cons(_, xs1) にマッチするなら、名前 xs1 は xs の tail に束縛されます。 xs1 は (変数ではなく) 値であり、xs1 を違う型の別の値に変更することはできないことに注意してください。

リストノードに保管された中身を修正したくなったとしましょう。 例えば、線形の整数リストに保管されているそれぞれの整数の値を2倍したいかもしれません。 次のコードは、このようなことを行なう list_vt_2x という名前の関数を実装しています: 

fun
list_vt_2x{n:nat}
  (xs: !list_vt (int, n) >> _): void =
(
  case+ xs of
  | @list_vt_cons
      (x, xs1) => let
      val () = x := 2 * x
      val () = list_vt_2x (xs1)
      prval () = fold@ (xs)
    in
      // nothing
    end // end of [list_vt_cons]
  | list_vt_nil () => ()
) (* end of [list_vt_2x] *)

型 T が与えられた時、(!T >> _) という記法は (!T >> T) の略です。 パターン list_vt_cons(x, xs1) の前にある特殊記号 @ は unfolding を意味することに注意してください。 もし xs がこのパターンにマッチした場合、 x と xs1 は、それぞれ xs の head と tail が格納された場所 L1 と L2 を指すポインタに束縛されます。 そして xs が参照するリストノードの位置を L0 とするために、xs の型は list_vt_cons_unfold(L0, L1, L2) に変化します。 パターン list_vt_cons(x, xs1) によるガード節の本体において、x と xs1 は (左辺値の) 変数として扱われます。 特別な証明関数 fold@ は xs に対して呼び出され、それを畳み込むと同時に L1 と L2 に付属した駐観の証明を線形リストにします。

線形リストのノードが正確に解放される例を見てみましょう: 

fun{
a:t@ype
} list_vt_free
  {n:nat} .<n>.
  (xs: list_vt (a, n)): void =
(
  case+ xs of
  | ~list_vt_cons
      (x, xs1) => list_vt_free (xs1)
  | ~list_vt_nil ((*void*)) => ()
) (* end of [list_vt_free] *)

線形リストが与えられた時、関数 list_vt_free はそのリスト中の全てのノードを解放します。 list_vt_free の本体を注意深く調べてみましょう。 xs がパターン list_vt_cons(x, xs1) にマッチするなら、 名前 x と xs1 はそれぞれ xs の head と tail に束縛されます; パターンの前にある特殊記号 ~ は、xs がパターンにマッチした後、xs で参照されるリストノードが即座に解放されることを意味しています。 もし xs がパターン list_vt_nil() にマッチするなら、束縛は生成されません; パターンの前にある特殊記号 ~ は xs で参照されるリストノードが解放されることを示しています; この場合 list_vt_nil は NULL ポインタにマップされているので、実際に実行時には何も解放されません。

変数がデータ観型に関連するコンストラクタで作られたパターンにマッチした後に、線形変数はそのまま残して (またはスケルトンとも呼ばれます) ノードを明示的に解放するために特殊関数 free@ を使うことも可能です。 例えば、次のコードは list_vt_free の別の実装です: 

fun{
a:t@ype
} list_vt_free
  {n:nat} .<n>. (xs: list_vt (a, n)): void =
  case+ xs of
  | @list_vt_cons
      (x, xs1) => let
      val xs1_ = xs1 // [xs1_] is the value stored in [xs1]
      val ((*void*)) = free@{a}{0}(xs) in list_vt_free (xs1_)
    end // end of [list_vt_cons]
  | @list_vt_nil () => free@{a} (xs)
// end of [list_vt_free]

実際の場面における free@ の少し巧妙な使い方として、次に詳しく解説します。 はじめに list_vt に関連するコンストラクタ list_vt_nil と list_vt_cons には次のような型が割り当てられています: 

list_vt_nil : // one quantifier
  {a:t@ype} () -> list_vt (a, 0)
list_vt_cons : // two quantifiers
  {a:t@ype}{n:nat} (a, list_vt (a, n)) -> list_vt (a, n+1)

もし free@ が型 list_vt_nil() ノードに適用されたら、コンストラクタ list_vt_nil の型に量化子をインスタンス化するために、型としての静的引数を1つ必要とします。 もし free@ が型 list_vt_cons_unfold(L0, L1, L2) ノードに適用されたら、コンストラクタ list_vt_cons の型に2つの量化子をインスタンス化するために、2つの型と整数の静的引数を必要とします。 xs の型が list_vt_cons_unfold(L0, L1, L2) である場合、 free@{a}{0}(xs) 呼び出しを型検査すると駐観 a?@L1 と駐観 list_vt(a, 0)?@L2 の証明を暗黙的に消費します。 どのような T と I においても、list_vt(T, 0)? と list_vt(T, I)? の間に違いがないので、静的引数 0 をこのコードでは使っています。 実際のところ、どのような自然数も free@ の第二静的引数として0の代わりに使うことができます。

線形リストの逆順

次のコードは、与えられた線形リストを逆順にする関数 reverse を実装しています: 

fn{
a:t@ype
} reverse{n:nat}
(
  xs: list_vt (a, n)
) : list_vt (a, n) = let
  fun revapp
    {i,j:nat | i+j==n} .<i>.
  (
    xs: list_vt (a, i), ys: list_vt (a, j)
  ) : list_vt (a, n) =
    case+ xs of
    | @list_vt_cons
        (_, xs1) => let
        val xs1_ = xs1
        val () = xs1 := ys
        prval () = fold@ (xs)
      in
        revapp (xs1_, xs)
      end // end of [list_vt_cons]
    | ~list_vt_nil ((*void*)) => ys
  // end of [revapp]
in
  revapp (xs, list_vt_nil)
end // end of [reverse]

reverse に割り当てられた型は、この関数が線形リストを消費してそれと同じ長さの線形リストを返すことを示しています。 内部の関数 revapp は末尾再帰であることに注意してください。 線形リストの逆順のこの実装は、以前示したデータ観 slseg_v (これは片方向リストでした) を使った実装に直接対応しています。 これら2つの実装を比較すると、データ観型を使った実装は型レベルで著しく単純化されています。 例えば、関数 reverse と revapp に割り当てられた型において、ポインタに関して明示的な言及をしていません。

線形リストの連結

次のコードは、与えられた2つの線形リストを1つに連結する関数 append を実装しています: 

fn{
a:t@ype
} append{m,n:nat}
(
  xs: list_vt (a, m)
, ys: list_vt (a, n)
) : list_vt (a, m+n) = let
  fun loop {m,n:nat} .<m>. // [loop] is tail-recursive
  (
    xs: &list_vt (a, m) >> list_vt (a, m+n), ys: list_vt (a, n)
  ) : void =
    case+ xs of
    | @list_vt_cons
        (_, xs1) => let
        val () = loop (xs1, ys) in fold@ (xs)
      end // end of [list_vt_cons]
    | ~list_vt_nil ((*void*)) => xs := ys
  // end of [loop]
  var xs: List_vt (a) = xs // creating a left-value for [xs]
  val () = loop (xs, ys)
in
  xs
end // end of [append]

関数 loop の本体にある fold@(xs) 呼び出しは型検査後に消去されるので、loop は末尾再帰関数です。 したがって、スタックオーバーフローの可能性を気にせず、どのような長さのリストに対しても append を呼び出すことができます。 loop の最初の引数の型は記号 & ではじまっています。 これはこの引数が参照渡しであることを示しています。 loop の型は、1番目の引数が長さ m のリストから長さ m+n のリストに変化することを単に意味しています。 この時、2番目の引数は消費されます。

リスト連結のこの実装は、以前紹介したデータ観 slseg_v を用いた実装と本質的に一致しています。 これら2つの比較すると、上記の実装がはるかに単純できれいで、データ観に対するデータ観型の利点を具体的に立証していることがわかるでしょう。

これはまた、関数的なリスト連結と末尾再帰に関連する問題について言及する良い機会です。 次は関数的なリスト連結の典型的な実装です: 

fun{
a:t@ype
} append1{m,n:nat}
(
  xs: list (a, m), ys: list (a, n)
) : list (a, m+n) =
  case+ xs of
  | list_cons (x, xs) => list_cons (x, append1 (xs, ys))
  | list_nil () => ys
// end of [append1]

明確に append1 は末尾再帰ではありません。 つまり、もし1番目の引数がとても長かった (例: 百万個の要素を含むような) 場合には実行時にスタックオーバーフローを引き起こす可能性があります。 けれども、関数的なリスト連結を末尾再帰的に実装するために、ATS では直接的かつ化安全な方法があります。 スタックオーバーフローの可能性を取り除くことができます。 例えば、 次のような append2 の実装は与えられた関数的な2つのリストを、末尾再帰的に連結して返します: 

fun{
a:t@ype
} append2{m,n:nat}
(
  xs: list (a, m), ys: list (a, n)
) : list (a, m+n) = let
//
fun loop
  {m,n:nat} .<m>.
(
  xs: list (a, m), ys: list (a, n)
, res: &(List a)? >> list (a, m+n)
) : void =
(
  case+ xs of
  | list_cons
      (x, xs) => let
      val () = 
      res := list_cons{a}{0}(x, _)
      val+ list_cons (_, res1) = res
      val () = loop (xs, ys, res1)
      prval ((*void*)) = fold@ (res)
    in
      // nothing
    end // end of [list_cons]
  | list_nil () => (res := ys)
) (* end of [loop] *)
//
var res: List(a)
val () = loop (xs, ys, res)
//
in
  res
end // end of [append2]

型検査の間では、アドレス L0, L1, L2 について、式 list_cons{a}{0}(x, _) には線形型 list_cons(L0, L1, L2) が割り当てられています。 このとき、駐観 a@L1 と駐観 list(a, 0)?@L2 の証明が現在有効な証明として保存されます。 特殊記号 _ は単に、新しくコンストラクトされたリストの tail が未初期化であることを示すことに注意してください。 型 list_cons(L0, L1, L2) の部分的に初期化されたリストはパターン list_cons(_, res1) にマッチすることが保証されます。 この時、res1 と当該リストの (未初期化の可能性がある) tail を格納した L2 を指すポインタの間に束縛ができます。 T と N がそれぞれ型と整数であるとき、型 list_cons(L0, L1, L2) の変数に fold@ が呼び出されると、それは list(T, N+1) 型に変化します。 この時、at-view T@L1 と at-view list(T, N)@L2 の証明が消費されます。

要約

データ型に関連付けれられているパターンマッチの利便性を、データ観型を用いて明示的なメモリ管理をサポートする際にも享受することができました。 データ観と比較するとデータ観型は一般的ではありません。 けれども、もしデータ観型を用いて問題を解決できれば、 その解決策はデータ観を用いた時よりしばしばきわめて単純できれいになります。

PrevHomeNext
線形データ型としてのデータ観型 (dataviewtype)Up例: 線形リストのマージソート