章一覧

リスト・ジェネリクス・型クラス

同じアルゴリズムを、複数の型に使います。

6.1 リストは二つの形を持つ

標準の List(A) は、空のリスト Nil と、先頭と残りを持つ Cons(head, tail) でできています。

ch06-list.taut
let numbers := Cons(1, Cons(2, Cons(3, Nil)))

fn list_sum(xs: List(i64)): i64 ! {Div} {
  match xs {
    Nil => 0
    Cons(first, rest) => first + list_sum(rest)
  }
}

perform show("sum", list_sum(numbers))
実行結果
・ list_sum

sum = 6
sum = 6

List(i64) を値の形に従って分解するので、空の場合とそうでない場合の両方が自然に扱えます。Cons の rest に対する再帰は、リストの構造に沿った再帰です。

6.2 型に依存しない関数

ch06-identity.taut
fn identity<A>(x: A): A {
  x
}

let n := identity(42)
let t := identity("Tauto")
perform show("n", n)
perform show("t", t)
実行結果
✓ def identity : ∀ A: Type. (A) -> A

n = 42
t = "Tauto"
n = 42
t = "Tauto"

<A> は型パラメータを宣言します。引数の型から A が決まるので、呼ぶときに書かなくて構いません。型として使うときは、前章の Option(i64) のように丸括弧で適用します。

6.3 where Ord(A) が示すもの

任意の型で大小を比べるには、比較の方法が必要です。Tauto の型クラス Ord(A) は、比較関数があるだけではなく、順序として守るべき法則も含みます。関数が Ord(A) を要求することは、where で書きます。

挿入ソートを書いてみます。証明で使う定義を import std::Base で読み込み、プログラムで使う順序を import std::prelude::Ord で明示的に読み込みます。

tauto init sorter
src/sort.taut
import std::Base
import std::prelude::Ord

pub fn insert<A>(x: A, l: List(A)): List(A) where Ord(A) {
  match l: List(A) {
    Nil => Cons(x, Nil)
    Cons(y, tail) => match Ord::compare(x, y): List(A) {
      Less => Cons(x, Cons(y, tail))
      Equal => Cons(x, Cons(y, tail))
      Greater => Cons(y, insert(x, tail))
    }
  }
}

pub fn sort<A>(l: List(A)): List(A) where Ord(A) {
  match l: List(A) {
    Nil => Nil
    Cons(x, rest) => insert(x, sort(rest))
  }
}
✓ 検査を通過
✓ def insert : ∀ A: Type. (Ord(A)) -> (A) -> (List(A)) -> List(A)
✓ def sort : ∀ A: Type. (Ord(A)) -> (List(A)) -> List(A)
src/main.taut
import "sort.taut"

perform show("ints", sort(Cons(3, Cons(1, Cons(2, Nil)))))
perform show("words", sort(Cons("pear", Cons("apple", Cons("fig", Nil)))))
実行結果
ints = Cons(1, Cons(2, Cons(3, Nil)))
words = Cons("apple", Cons("fig", Cons("pear", Nil)))
tauto run --tote sorter
ints = Cons(1, Cons(2, Cons(3, Nil)))
words = Cons("apple", Cons("fig", Cons("pear", Nil)))

比較が Less か Equal なら先頭に挿入し、Greater なら次の要素を調べます。同じ sort が、数にも文字列にも使えます。Ord::compare(x, y) が唯一の比較で、match で Less・Equal・Greater に分けています。

法則を証明できるようにクラスを定義してあるので、特定の数値型に依存しない、ソートの性質を主張できます(第 18 章)。

演習 6.1:identity と、リストを一段ずつ分解する関数の共通点を説明してください。