リスト・ジェネリクス・型クラス
同じアルゴリズムを、複数の型に使います。
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 と、リストを一段ずつ分解する関数の共通点を説明してください。