ATSプログラミング入門:
Prev	Chapter 10. データ型の改良	Next

例: リストに対する関数テンプレート (再)

コンストラクタ list0_nil と list0_cons で作られるリストに対する関数テンプレートを使った一般的な実装を以前紹介しました。ここでは、コンストラクタ list_nil と list_cons で作られるリストに対する関数テンプレートを次のように実装します。この実装によってこれらのテンプレートにより正確な型を割り当てることができます。

この章のコード全体とテストのための追加コードはオンラインから入手できます。

連結: list_append

型 T と整数 I1 と I2 があり、2つのリスト xs と ys が型 list(T, I1) と list(T, I2) で与えられた時、list_append(xs, ys) は xs と ys を連結した型 list(T,I1+I2) のリストを返します:

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

list_append のこの実装が末尾再帰でないことは明確です。

逆順連結: list_reverse_append

型 T と整数 I1 と I2 があり、2つのリスト xs と ys が型 list(T, I1) と list(T, I2) で与えられた時、list_reverse_append(xs, ys) は xs と ys を逆順にして連結した型 list(T, I1+I2) のリストを返します:

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

list_reverse_append のこの実装が末尾再帰であることは明確です。

逆順: list_reverse

リスト xs が与えられた時、list_reverse(xs) は xs の逆順を返します。この返値は xs と同じ長さになります:

fun{a:t@ype}
list_reverse{n:nat} .<>. // defined non-recursively
  (xs: list (a, n)): list (a, n) = list_reverse_append (xs, list_nil)
// end of [list_reverse]

マップ: list_map

型 T1, T2 と整数 I があり、型 list(T1, I) のリスト xs と型 T1 -<cloref1> T2 のクロージャ関数 f が与えられた時、list_map(xs) は型 list(T2, I) のリスト ys を返します:

fun{
a:t@ype}
{b:t@ype
} list_map
  {n:nat} .<n>.
(
  xs: list (a, n), f: a -<cloref1> b
) : list (b, n) =
(
  case+ xs of
  | list_nil() => list_nil()
  | list_cons(x, xs) => list_cons(f x, list_map<a>(xs, f))
) (* end of [list_map] *)

ys のそれぞれの要素 y は、xs の対応する要素を x とすれば f(x) に等しいことになります。 list_map のこの実装が末尾再帰でないことは明確です。

zip関数: list_zip

型 T1, T2 と整数 I があり、型 list(T1, I) と list(T2, I) のリスト xs と ys がそれぞれ与えられた時、list_zip(xs, ys) は型 list((T1,T2), I) のリスト zs を返します。

fun{
a,b:t@ype
} list_zip
  {n:nat} .<n>.
(
  xs: list (a, n), ys: list (b, n)
) : list ((a, b), n) =
(
  case+ (xs, ys) of
  | (
      list_nil()
    , list_nil()
    ) => list_nil((*void*))
  | (
      list_cons (x, xs)
    , list_cons (y, ys)
    ) => list_cons((x, y), list_zip<a,b>(xs, ys))
) (* end of [list_zip] *)

zs のそれぞれの要素 z は、xs と ys の対応する要素をそれぞれ x と y とすれば、ペア (x, y) に等しいことになります。list_zip のこの実装が末尾再帰でないことは明確です。

zip with関数: list_zipwith

型 T1, T2, T3 と整数 I があり、2つのリスト xs と ys がそれぞれ型 list(T1, I) と list(T2, I) で、クロージャ関数 f が型 (T1, T2) -<cloref1> T3 で与えられた時、list_zipwith(xs, ys, f) は型 list(T3, I) のリスト zs を返します:

fun{
a,b:t@ype
}{c:t@ype
} list_zipwith
  {n:nat} .<n>.
(
  xs: list (a, n)
, ys: list (b, n)
, f: (a, b) -<cloref1> c
) : list (c, n) =
(
  case+ (xs, ys) of
  | (
      list_nil()
    , list_nil()
    ) => list_nil((*void*))
  | (
      list_cons(x, xs)
    , list_cons(y, ys)
    ) =>
      list_cons(f(x, y), list_zipwith<a,b><c>(xs, ys, f))
     // end of (list_cons, list_cons)
) (* end of [list_zipwith] *)

zs のそれぞれの要素 z は、xs と ys の対応する要素をそれぞれ x と y とすれば、f(x, y) に等しいことになります。 list_zipwith のこの実装が末尾再帰でないことは明確です。

Prev	Home	Next
データ型の改良	Up	例: リストのマージソート (再)