日本ソフトウェア科学会第 41 回大会 (2024 年度) 講演論文集

パラメトリック多相関数の真偽値への単相化によるテスト
森畑 明昌
パラメトリック多相型をもつ関数をテストする際には、何らかの具体的な型で多相型を単相化する必要があるが、テストの有効性はどの型で単相化するかに依存しかねない。この問題に対し、いくつかの先行研究が多相型関数のテストのための適切な単相化手法を与えている。これらの手法は、多相型変数に対応する値がどのように得られたかを精緻に追跡するという着想に基づき、最終的には元の多相関数と等価な単相関数を構築する。そのため、テストにかかわらない部分についてまで実行トレースを全て覚えるような挙動になりやすい。本研究では、値が最終的にどのように観察され検証されるか、という観点から単相化の手法を与える。そして、多相型変数を真偽値に単相化したとしても意図せぬ挙動を必ず発見できるための十分条件を与える。さらに、この十分条件を満たさないプログラムに対し、条件をより満たしやすいプログラムへと変換するプログラム変換を与える。提案手法の有用性を確かめるため、
Haskell 98 の Prelude ライブラリに含まれる関数に対して網羅的な適用を試みた。真偽値型への単相化では十分なテストが本質的に不可能な場合を除いて、提案手法はほとんど全ての多相関数を「真偽値型への単相化で十分テストできる」と正しく判定できた。

し、ありうる型は有限種類ではなく、またプログラム

1 はじめに中で新たに定義されることもあるので、あらゆる型を

テストはプログラムの誤りを発見する最も基本的

試すのは原理的に不可能である。

で広く使われている手法である。にもかかわらず、著

もちろん、テストは明らかな間違いを見つけること

者の知る限り、多相関数のテストについての議論は多はできても、正しさを保証するようなものではない。

くない。例として、リストの要素を逆順に並び替える

そのため、すべての型を試すというのはテストの趣

関数 reverse を考える。

旨からしてそもそも必要ないという主張もありうる。

reverse :: ∀α. [α] → [α]
これはリストの要素がどんな型であっても動作する多そうだとしても、一定の標準的な指針があることが望ましい。

相関数である。ごく単純に考えると、この関数をテス

パラメトリック多相型を用いる関数型言語では、「適トするためには、リストの要素としてあらゆる型の当な型（例えば Int ）だけを試せば十分である」といものを試す、言い換えると型変数 α をあらゆる型でうような主張がしばしばなされる。例えば、Sannellar

単相化する必要がありそうに見える。例えば、リスト

らによる教科書 [19] には以下の記述がある。

の要素が Bool 型の場合にうまく動作したとしても、

You might think that polymorphic proper-

Int 型の場合はうまく動作しないかもしれない。しかties should be tested for values of many
diﬀerent types, in order to catch errors† TestingParametrically Polymorphic Functions via
Finite Monomorphization.
† This is an unrefereed paper. Copyrights belong to
the author.
Akimasa Morihata, 東 京 大 学 大 学 院 総 合 文 化 研 究 科,
Graduate School of Arts and Sciences, the University of Tokyo.

that might arise for one type but not another.

But since polymorphic functions

behave uniformly for all type instances,
there’s no need to test them on diﬀerent
types. It suﬃces to test polymorphic prop-

erties for Int or some other inﬁnite type.
しかし、このような主張にははっきりしないところがを用いるプログラムや、型クラスを用いるプログ
ラムでこのようなことが起こりやすい。

ある。まず、そもそもこの主張が正しいのかどうか、• 値が巨大ないし複雑になってしまった結果、テ

一見しては判じがたい。さらに、より少ない要素しかストが実質的に不可能、ないしは明らかに非効率

含まない型（例えば 2 つの要素をもつ Bool 型）ではとなってしまう例がある（詳細は 6. 1 節参照）。

何故だめなのか、またそうだとすれば本当に Int 型で本研究では既存研究とは異なる方針に基づき、多十分なのか、といったこともわからない。また、Int

相関数を単相化しテストする手法を与える。本研究型の要素なら何を使ってもよいのか、それともあらゆは特に、出力結果の正しさがどのように確認される

る Int 型の値をテストしなければならないのかもはっかに注目し、その確認に必要な情報をもつ入力を構成

きりしない。

することを目指す。例として再び reverse を考える。

この問題に対し、いくつかの研究 [3] [4] [8] [26] が、

reverse に長さ n のリストを入力し実行したとき、出パラメトリック多相性を持つ関数を完全にテストで力結果が正しくない場合は、以下の 2 通りに大別できる単相化の方法を論じている。これらの手法では、きる。

多相型に対応する値の具体的な内容の代わりに、そ• 出力結果のリストの長さが n でない。

の値がどのように得られたかを用いる。例えば、前述• 出力結果のリストの i 番目（0 ≤ i < n）の要素の reverse 関数にこの手法を適用すると次のようになが、入力リストの n − i − 1 番目の要素でない。

る。この関数の場合、α 型の値を得る方法は、入力リ

前者の場合、reverse 関数の動作はリストの要素によ

ストの中身を取り出すしかない。つまり、「入力リスらないため、どんな要素でも同様の誤りが生じるはず

トの何番目の要素から得られたか」に着目し、「リスである。つまり、() 型で試しても十分である。また、トの何番目の要素か」で単相化すればよい。よって、後者の場合、「その値が入力リストの n − i − 1 番目

reverse [0, 1, . . . , n − 1] = [n − 1, n − 2, . . . , 0]の要素と等しいか？」という点だけが問題となっていを確認すれば、長さ n のあらゆるリストに対して正る。つまり、n − i − 1 番目の要素が True 、それ以外

しく動作することが確かめられる。

が False のリストを入力したとして、出力の i 番目のこれらの手法は多相関数をテストする上での非常要素が True であることを確認すれば十分である。以

に良い指針を与える。しかし、これらの手法は、バグ上をふまえると、reverse 関数の誤りは Bool 型のリを発見するのに十分な情報をもてる値を使うことをストを十分テストすれば必ず発見できるはずである。

目指しており、時として複雑で巨大な値を用いて単相以上の例からもわかるとおり、本研究では、テスト化することになる。このことは、いくつかの問題をも結果の値が正しくないことを発見する観察を入力値たらしている。

へと伝播することで、入力としてどのような値を与• どのようなテストが行われるかを考慮していえれば十分にテストできるかを調べる。特に、多相型ないために冗長な情報を保持している可能性

変数を有限値域の型に単相化してテストすることで、がある。例えば、リストの長さを計算する関数

テスト対象の関数が所望の性質を満たすことを確認

length :: ∀α.[α] → Int であれば、入力リストのできる（本稿ではこれを有限単相化テストと呼ぶ）た

要素はテストに関係しないはずだが、この手法でめの十分条件を発見することを目指す。

は reverse と同様に自然数が順に並んだリストでのテストを求める。

本稿ではまず、上記の直感を定式化し、構造に関する性質が () 型への単相化で、要素に関する性質が• 実行トレースをほとんど完全に記憶するようなBool 型への単相化で、それぞれ有限単相化テストで結果になることも珍しくない。そのため、実行ト

きるための十分条件を与える（3 節）。次に、典型的レースが多少異なっても問題ないような例では、ないくつかの例を通して、提案手法の利用を実演する

うまくテストできないことがある。抽象データ型（4 節）。その中でも特に、提案手法が直接は適用でき

ない多相関数に対して、上記変換が適用できる形式へすために用いる。

と変換する前処理を与える（4. 2 節）。そして、提案

本稿の議論では圏論における関手の概念を援用す手法が実用的なプログラムに対してどの程度有用である。
（共変）関手 F とは、本稿においては、任意の型 Aるかの評価の第一歩として、関数型言語 Haskell [17]を型 FA に変換する型構成子であり、さらに任意の関の Prelude ライブラリの関数に対して網羅的に適用

数 f :: A → B に対し関数 Ff :: FA → FB を伴うもした結果を報告する（5 節）。6 節では提案手法を既のである。特に、関手のもたらす関数は Fid A = id FA

存手法と比較し、長短や今後の課題について論じる。

および Ff ◦ Fg = F(f ◦ g) を満たさなければならない。
関手の典型例はリスト型構成子 LX = [X] であり、

2 準備

map 関数が関手のもたらす関数となる。また、積・

本稿では関数型言語 Haskell [17]1 の記法を用い

和・定数・関数・関手の組合せで構成される型 T (α)

る。が、読みやすさのため、明らかに意図が理解できについて、α がその共変位置にのみ現れる場合、T はる範囲で、Haskell と多少異なる記号を用いる部分が関手である。関手を表すメタ変数としては F, G, H 等ある。例えば、ラムダ式には \x− > e ではなく λx. eを用いる。

を用いる。さらに、λx. λy. e は λx, y. e と略記する。

以降では、定式化を単純にするため、「関手 F およ

また、等値演算子は ≡ を、非等値演算子は ̸= を、大び G を用いて Fα → Gα と表せる型」は「関手 G を用

小比較演算子は ≤ 等を、それぞれ用いる。真偽値演

いて Gα と表せる型」を含むものとする。これは Gα

算には否定に ¬、論理積に ∧、論理和に ∨ を用いる。

型と 1 → Gα 型が同型であることに基づいている。

さらに、関数合成演算子としては ◦ を用いる。

本稿ではパラメトリック多相型に対するパラメトリ型についても、読みやすさのため、Haskell と多少

シティ原理 [18] [24] [23] に基づく “fast and loose but

異なる名称を用いる。要素を 1 つのみ含む型（Haskell

morally correct” [5] な議論を行う。具体的には、評の () 型）は 1 で表す。真偽値型（Haskell の Bool 型）

価戦略によらず、有限ステップでエラーなく終了するは 2 で表す。整数の集合に対応する方は Z で、自然ような実行のみを考え、その範囲ではパラメトリシ

数の集合に対応する型は N で表す。なお、N はゼロ

ティ原理が成り立つことを仮定する。例えば、リストと後者構成子からなる再帰データ型ではなく、Z の部の先頭要素を取り出す関数 head :: ∀α. [α] → α につ分集合とする。

いては、1 つ以上の要素を含むリストを入力した際の本稿では、α, β, γ は型変数を表すために用いる。また、型や型構成子を表すメタ変数としては A, B, T な
どの英大文字を用いる。プログラム中の変数名や関数名は f や x などの英小文字で表す。
本稿に現れる Haskell の関数のうち代表的なものの動作のみを議論の対象とする。そのため、Haskell の遅延評価や非正格性は議論に影響しない。
本稿の議論では以下の補題を用いる。この補題は多相型のパラメトリシティ [18] [24] [23] から容易に証明することができる。
補題 1. 多相関数 g :: ∀α.(F0 α → G0 α) → (F1 α →定義を図 1 に示す。
多相型をもつ式 e :: ∀α. T (α) に対し、型 A によるG1 α) → · · · → (Fn−1 α → Gn−1 α) → H(α) （た:: T (A) と表す。特に、どの型だ し 各 Fi , Gi （0 ≤ i ≤ n − 1）お よ び H は 関

変数に対する単相化であるかが文脈から明らかな場

手 ）、項 fi :: Fi A → Gi A と fi′ :: Fi B → Gi B合、e[α:=A] を単に eA と略記する。なお、この添字は（0 ≤ i ≤ n − 1）、および関数 h :: A → B について、文脈から明らかであれば省略することもある。また、以下の条件が満たされるとする。

e の単相化を e[α:=A]

e :: ∀α. T (α) に対し、「α 型の値」という言葉を「適当な型 A による単相化 eA における A 型の値」を表

条件 各 0 ≤ i ≤ n−1 について、Gi h◦fi = fi′ ◦Fi hが成り立つ。
このとき、次の等式が成り立つ。

1 特に明示しない限り Haskell 98 を考える。

id :: ∀α.α → α
id x = x(!!) :: ∀α.[α] → α(a : x) !! n = if n ≡ 0 then a else x !! (n − 1)

fst :: ∀α, β.(α, β) → α
fst (x, y) = x

snd :: ∀α, β.(α, β) → αsnd (x, y) = x

min :: ∀α.Ord α ⇒ α → α → α
min x y = if x ≤ y then x else y

max :: ∀α.Ord α ⇒ α → α → α
max x y = if x ≤ y then y else x(++) :: ∀α.[α] → [α] → [α]
[] +
+y
= y
(a : x) ++ y = a : (x ++ y)concat :: ∀α.[[α]] → [α]concat [ ]= []concat (x : xs) = x ++ concat xs

length :: ∀α.[α] → N
length [ ]= 0length (a : x) = 1 + length x

reverse :: ∀α.[α] → [α]reverse [ ]= 0reverse (a : x) = reverse x ++ [a]map :: ∀α, β.(α → β) → [α] → [β]map f [ ]= []map f (a : x) = f a : map f x

foldr :: ∀α, β.(α → β → β) → β → [α] → βfoldr f e [ ]= efoldr f e (a : x) = f a (foldr f e x)

図1

本稿で用いる代表的な Haskell 関数′
Hh (g A f0 · · · fn−1 ) = gB f0′ · · · fn−1

なく、平衡木の高さまで含めてテストしたい可能性もある。

3 有限単相化テスト可能条件

このように、T2 の型によって、またどのような性

いま、多相関数 g :: ∀α.T1 (α) → T2 (α) をテストす

質をテストしたいかによって、テストの実態は様々にることを考える。このためには、適当な型 A で単相変わる。この状況を統一的に扱おうとすると、等価性に対して適当な値 v :: T1 (A) を渡し、結果の確認まで含めた処理をテストするという方針が自v :: T2 (A) が所望の性質を満たす—典型的には意然に考えられる。例えば、上記 g であれば、これの

化し、g

g

A

A

図通りの値に等しい—ことを確認することになる。このようなテストのための一般的な理論の構築が本研究の目的である。しかし実際には、T2 がどのような型かによってテストの状況はずいぶん変わってくる。
このことを確認するため、「出力結果が特定の値と等しいかどうか」を調べることを考えよう。仮にT2 (X) = N → X であれば、出力結果が関数なので「特定の値と等しいかどうか」は調べられない 2 。また、平衡木によって集合を表している場合、平衡木の形はどうでも良く、要素集合として同じ物が含まれていれば「等価である」とするようなテストをしたい可能性もある。この場合、「特定の値に等しいかどうか」を調べる処理は構造に対する再帰を伴う複雑な処理となってしまう。しかも、平衡木に対する「等価性」

参照実装 g を用意し、
λv, eq. eq (g v) (g v):: ∀α.T1 (α) → (T2 (α) → T2 (α) → 2) → 2という式を考え、これに引数 v に加えて等価性確認
関数 (≡) を入力として渡すという方針である。この式であれば、結果が v によらず True であることを確認すれば良いため、「性質の確認方法」に悩むことはない。
しかし残念ながら、このようにテスト対象の型が変わってしまうと、十分なテストのために必要な単相化も変わってしまう。例として以下の型の関数を考える。

thd :: ∀α.(α, α, α) → α
実は、この関数が常に組の 3 つ目の要素を返すことを確認するには、2 型で単相化し、のテストはこれに限らない。例えば、要素集合だけで

thd 2 :: (2, 2, 2) → 2

2 このケースでは、出力結果の引数 N も g の引数だとみなし、この部分も含めてテストすれば良いと考えるかも知れない。しかし、このアプローチは T2 = [N → X]のような場合にスケールしない。

をテストすれば十分である。しかし上記方針に従い、

thd ′ :: ∀α.(α, α, α) → (α → α → 2) → 2という型の式を考えてしまうと、2 型への単相化では

バグを発見できない可能性が残ってしまう。具体的には、以下の式が表すような間違った実装 wrong thd′のテストをすることを考える。いま、参照実装（つまり入力リストを正しく逆順に並べ替える関数）をは、正しい実装を表していないにもかかわらず、2 型

reverse とすると、調べたい性質は、任意のリスト

への単相化では常に True を返してしまう。
wrong thd ′ (a, b, c) eq

x に対して=eq c (if ¬(eq a b) ∧ ¬(eq b c) ∧ ¬(eq c a)then aelse c)wrong thd ′ は、a、b、c の値が全て異なる場合には a
を返し、そうでなければ c を返すような実装を表している。入力が 2 型の組の場合、a、b、c の値が全て異なることはあり得ないので、常に c を返す。しかし、一般には a を返しうるために正しくない。

reverse x = reverse xが成り立つことである。これを確かめるためには、まず構造的性質としては、出力されるリストの「形」が等しいこと、すなわちlength (reverse x) = length (reverse x)を確認すればよい。また、要素的性質としては、出力される「要素」がそれぞれ等しいことを示せば良い。
つまり、0 ≤ i < length x なる任意の自然数 i に対し以上の事実は、値をどのように観察するかは可能なて以下が真となることを確認できれば良い。
p (acc (reverse x))

単相化を判断する上で本質的であることを示唆する。

where acc x = x !! ithd は α 型の値の等価性を確認するすべを持たなかった。一方、wrong thd ′ は α 型の値の等価性をプログ

p v = v ≡ (reverse x !! i)
出力が単純なリストでない場合でも同様にしてテス

ラム中で確認することができるようになってしまったトを行うことができる。例えば、計算結果がネストしたため、2 型への単相化では不十分となった。言い換え

リスト r :: [[A]] であり、参照実装の実行結果が r ∗ であると、テスト対象のプログラムの実行結果に対して調れば、構造的性質を map length r = map length r ∗べたい性質は、そのプログラムとは別個に決めなけれで確認し、要素的性質は、総要素数を n として、ばならない。

各 0 ≤ i < n について、acc x = concat x !! i とそこで本研究では、T (α) 型要素の性質を構造的性

p v = v ≡ (concat r∗ !! i) を用いて調べれば良い。

質と要素的性質に分けて考える。構造的性質は α 型

構造的性質・要素的性質は以下の性質を満たす。

の要素に依存しないものであり、要素的性質は原則と補題 4. 関手 H に対する構造的性質 sp :: ∀α. Hα → 2

して T に依存しない性質である。∀α. T (α) 型というについて以下の等式が成り立つ。ここで A は任意の多相型を持つ式をテストする上で、両者の区別は本質型、erase :: ∀α. α → 1 は erase a = () で定義され的である。構造的性質は α をどの型に単相化するかる関数である。

と無関係であり、どの型に単相化してテストすれば良いかには主に要素的性質が関わるはずである。
定義 2. 関手 H に対し、多相関数 sp :: ∀α. Hα → 2

sp A = sp 1 ◦ Herase
Proof. sp の多相型に対するパラメトリシティ原理[18] [24] [23] から直裁である。

を H に対する構造的性質と呼ぶ。
定 義 3. 関 手 H に 対 し 、acc :: ∀α.Hα → α と補題 5. 関手 H に対する (acc, p) による要素的性質

p :: A → 2 を用いて ep = p ◦ acc と定義される

ep :: HA → 2 について、以下の等式が成り立つ

関数 ep :: HA → 2 を H に対する (acc, p) による要素的性質と呼ぶ。
構造的性質の多相性は α 型の要素について関知し

ep = acc 2 ◦ Hp
Proof. acc の多相型に対するパラメトリシティ原理[18] [24] [23] から直裁である。

ないことを表している。また、要素的性質は、acc によって要素のみを取り出した上で性質を調べている。
構造的性質・要素的性質に基づいて reverse 関数

補題 4・5 を補題 1 と併せることで、以下の単相化

テスト手法が得られる。これらは、一定の条件の下で、構造的性質の確認には 1 型への単相化で、要素

ep (g A f0 · · · fn−1 )=的性質の確認には 2 型への単相化で十分であることを示している。

=

定理 6. 多相関数 g :: ∀α.(F0 α → G0 α) → (F1 α →G1 α) → · · · → (Fn−1 α → Gn−1 α) → H(α) （ただし各 Fi , Gi （0 ≤ i ≤ n − 1）および H は関手）につい{ 補題 5 }acc (Hp (g A f0 · · · fn−1 )){ 補題 1 }′acc (g 2 f0′ · · · fn−1)=

{ ep ′ を (acc, id ) による要素的性質とする }′ep ′ (g 2 f0′ · · · fn−1)て、以下の条件が満たされるとする。
条件 任意の fi :: Fi A → Gi A（0 ≤ i ≤ n − 1）について、Gi erase ◦ fi = fi′ ◦ Fi erase を満たす関数 fi′ :: Fi 1 → Gi 1 が存在する。

定理 7・定理 6 の利用にあたっての補足
定理 6・定理 7 は、関数 fi に対して適切な条件を満たす関数 fi′ の存在のみを要求している。この点はこのとき、H に対する構造的性質 sp が g A のあらゆ

極めて重要である。

る出力結果で満たされるかどうかの確認には、g の例として関数 length :: ∀α.[α] → N に定理 6 を適出力結果に対して構造的性質 sp 1 をテストすれば十用することを考える。仮に、length に対してある値分である。

v :: [A] を入力すればバグが見つかるとしよう。定理16 は、map erase v = v ′ となる値 v ′ :: [1]（この v ′Proof.
sp A (g A f0 · · · fn−1 )={ 補題 4 }1

sp (Herase (g=A

f0 · · · fn−1 )){ 補題 1 }′sp 1 (g 1 f0′ · · · fn−1)

はどんな v に対しても必ず存在する）を入力しても同様にバグが見つかることを示している。このとき、我々は具体的な v ′ の値を知る必要はない。[1] 型の値のどれかが v ′ であることは分かるので、[1] 型の値をテストしてゆけばそのうち v ′ に遭遇するからだ。
よって、定理 6・定理 7 を使うにあたっては、適切定理 7. 多相関数 g :: ∀α.(F0 α → G0 α) → (F1 α →な条件を満たす関数 fi′ の存在が型のみからわかると

G1 α) → · · · → (Fn−1 α → Gn−1 α) → H(α) （ただし非常に望ましい。以下にそのような場合を挙げる。

各 Fi , Gi （0 ≤ i ≤ n − 1）および H は関手）、およ• 関手 Fi (X) が定数関手、すなわち X の出現をび p :: A → 2 について、以下の条件が満たされるとする。
条件 任意の fi :: Fi A → Gi A（0 ≤ i ≤ n − 1）に 対 し 、Gi p ◦ fi = fi′ ◦ Fi p を 満 た す 関 数

fi′ :: Fi 2 → Gi 2 が存在する。

伴わない場合。この場合、任意の関数 h に対して、Fi h = id なので、fi′ = Gi h ◦ fi とすれば

Gi h ◦ fi = fi′ ◦ Fi h を満たす。特に典型的な場合
は、fi が定数関数（値と同一視できる関数）である場合である。

このとき、H に対する (acc, p) による要素的性質 ep• fi :: ∀β.Fi β → Gi β の場合。この場合には、任意が g A のあらゆる出力結果で満たされるかどうかの確の関数 h :: A → B に対して、Gi h◦fiA = fiB ◦Fi h

2

認には、g の出力結果に対して (acc, id ) による要素

であることが fi の多相型に関するパラメトリシ

的性質をテストすれば十分である。

ティ原理から直裁に導かれる。

Proof.

4 有限単相化テストの例
本節では、具体例を通して定理 6・定理 7 の有用性と利用方法を論じる。

4. 1 単純なリスト処理関数

れば十分であることを意味する。ﬁlter ′ 関数の型は

まず、1 節で議論した reverse 関数を再訪する。

ﬁlter ′ :: ∀α.[(α, 2)] → [α] なので、定理 6・定理 7 を

reverse 関数の型は ∀α.[α] → [α] であり、リスト型構

適用できる。

成子が関手であることをふまえると定理 6・定理 7 が以上の議論は、次の定理として定式化できる。

即座に適用できる。よって、構造的性質は 1 型へ単定理 8. 多相関数 g :: ∀α.T0 (α) → T1 (α) → · · · →相化、要素的性質は 2 型へ単相化した上でテストすTn−1 (α) → H(α)（ただし H は関手）について、以下れば十分である。

の条件が満たされるとする。

様々な関数のテストが同様に可能である。例えば、

条件 1 T0 (α) = α → F0 (α) → G0 （F0 と G0 はconcat :: ∀α.[[α]] → [α] や、リストの先頭から指定された個数の要素を取り出す関数 take :: ∀α.N → [α] →関手。特に G0 は α を含まない）である。
条件 2 各 1 ≤ i ≤ n−1 について、Ti (α) = Fi α →[α] についても、構造的性質は 1 型へ単相化、要素的Gi α（Fi と Gi は関手）である。

性質は 2 型へ単相化した上でテストすれば十分であ

このとき、g A に対するテストは、B = (A, F0 (A) →る。また、length :: ∀α.[α] → N や、リストが空であG0 ) および f0′ x y = snd x (F0 fst y) として、代わるかどうかを調べる関数 null :: ∀α.[α] → 2 であれ

りに
λf1 , . . . , fn−1 .Hfst (g B f0′ f1 · · · fn−1 )ば、結果が α 型の要素を含まないため、構造的性質しか必要ない。よって、1 型への単相化で十分である。

:: ∀α.T1 (B) → · · · → Tn−1 (B) → H(B)をテストすれば十分である。

4. 2 要素を消費する関数を伴う場合の前処理

Proof. 各 fi :: Ti (A)（0 ≤ i ≤ n − 1）が与えられたテストしたい関数の引数の型が（共変）関手であれ

とき、mkpair f0 a = (a, f0 a) とし、これを用いて各ば、定理 6・定理 7 を即座に適用できる。しかし、こfi′ （1 ≤ i ≤ n − 1）を以下で定義する。

の条件が成り立たないものも多い。例として、与えfi′ = Gi mkpair f0 ◦ fi ◦ Fi fst

られた述語を満たす要素のみをリストから抽出する

ﬁlter 関数を考える。
ﬁlter :: ∀α.(α → 2) → [α] → [α]このとき以下の性質が成り立つ。

• f0 x y = f0′ (mkpair f0 x) (F0 mkpair f0 y)• Gi mkpair f0 ◦ fi = fi′ ◦ Fi mkpair f0 （0 ≤ i ≤n − 1）

この関数は引数として α → 2 型の述語をとるが、T (X) = X → 2 とすると T は関手ではない。このよ

後者については fst ◦ mkpair f0 = id および関手の性

うに、多相型変数に対応する要素を消費・観察するよ質から簡単に導くことができる。前者については以下

うな関数を引数とする関数の場合、定理 6・定理 7 はのように証明できる。

f0′ (mkpair f0 x) (F0 mkpair f0 y)

そのままでは適用できない。
しかしよく見ると、第 1 引数の述語に対する入力=

として α 型の値を提供できるのは第 2 引数のリストしかない。このことをふまえると、ﬁlter p の代わり

snd (mkpair f0 x) (F0 fst (F0 mkpair f0 y))==

適用しておき、ﬁlter 関数はその結果を参照するものである。

λx.map fst (ﬁlter snd (map (λa.(a, p a)) x))
このことは、そもそも map (λa.(a, p a)) x が入力
リストであったとみなせば、ﬁlter 関数のテストは代わりに ﬁlter ′ = map fst ◦ ﬁlter snd をテストす{ F0 は関手 }snd (mkpair f0 x) (F0 (fst ◦ mkpair f0 ) y)に以下の関数をテストすれば十分であると思われる。
この関数は、まず最初にリストの全ての要素に p を{ f0′ の定義 }{ fst ◦ mkpair f0 = id および F0 id = id }snd (mkpair f0 x) y=

{ mkpair f0 と snd の定義 }f0 x y以上をふまえ、任意の fi :: Ti (A)（0 ≤ i ≤ n − 1）

4. 3 型クラス制約を伴う場合に対して、等式gA

f0 · · · fn−1 = Hfst (gB′f0′ f1′ · · · fn−1)が成り立つことを示す。

==

パラメトリック多相性は、型変数のあらゆる具体化に対して、その項が同じように動作することを要求す′
Hfst (g B f0′ f1′ · · · fn−1)

る。これは実用上は非常に強い制約となる。そこで、{ 補題 1 および上記の性質 }型変数を具体化できる型を一定範囲に制限するよう

Hfst (Hmkpair f0 (g A f0 f1 · · · fn−1 ))な枠組みが多く提案されている。その中でも型クラス{ fst ◦ mkpair f0 = id および関手 H の性質 }[16] [25] は特に広く用いられている。

gA

f0 f1 · · · fn−1

定理 8 の効果をまず ﬁlter :: ∀α.(α → 2) → [α] →[α] で確認する。T0 (α) = α → 2 なので、定理 8 から、ﬁlter の代わりに

λx. map fst (ﬁlter snd x) :: ∀α.[(α, 2)] → [α]を テ ス ト す れ ば 十 分 で あ る こ と が 導 か れ る 。これは、我々がまさに観察してきたとおりの結果である。全く同様にして、リストの全ての要素が与えられた条件を満たすかどうかを確認する関数

all :: ∀α.(α → 2) → [α] → 2 やリストの要素を先頭から与えられた条件を満たす要素まで取り出す
関数 takeWhile :: ∀α.(α → 2) → [α] → [α] なども扱うことができる。
次の例として、map :: ∀α, β.(α → β) → [α] → [β]を考える。これに対しては、α を多相型変数、β を定数とみなし、定理 8 を適用すると、代わりに

map snd :: ∀α, β.[(α, β)] → [β]をテストすれば良いことが分かる。この結果をよく見ると、返値には α が現れないため、α について注目するならば構造的性質のみを確認すれば良いことが分かる。よって、定理 6 より、さらに

map [α:=1] snd :: ∀β.[(1, β)] → [β]をテストすれば十分であるとわかる。(1, β) が β と型クラスを伴う典型的な関数として 2 要素のうち大きい方を返す関数 max を考える。

max :: ∀α. Ord α ⇒ α → α → α
この型において、Ord α は「α を具体化できるのは

Ord のインスタンスである型に限る」という制約を表している。Ord のインスタンスでは、大小比較を行う関数 (≤) :: α → α → 2 が定義されていなければならない 3 。
型クラスを伴う多相関数を提案手法で扱う場合、2通りの方針が考えられる。本小節では以降、そのうちの一つである、型クラスが要求する関数を追加の引数とする関数を考え 4 、これに対するテストを行うという方針について論じる。もう一つの方針については次小節で扱う。
例えば、max 関数であれば、(≤) :: α → α → 2 が追加の引数として与えられると考え、代わりに型クラス制約を伴わない関数

max 1 :: ∀α. (α → α → 2) → α → α → α
をテストすれば十分である。定理 8 を適用すると、

max 1 の代わりに
max 2 = λx, y. fst (max ′ (λv, w. snd v (fst w)) x y):: ∀α.(α, α → 2) → (α, α → 2) → α
をテストすれば良いことが分かる。さらに、カリー化
によって max 2 と等価な関数同型であることをふまえると、「map をテストするに

max 3 :: ∀α.α → (α → 2) → α → (α → 2) → α

は map id をテストすれば十分である」というよく知が得られるので、更に定理 8 を 2 度適用することで、
λx, y. fst (fst (max 3 x snd y (snd ◦ fst)))られた事実と等価な結果 [3] [8] を系統的に導出できた質であれば 1 型へ、要素的性質であれば 2 型へ単相:: ∀α.((α, 2), 2) → ((α, 2), 2) → α
をテストすれば良いことが分かる。これに対しては化してテストすれば十分である。

定理 7 が適用でき、2 型への単相化でテストが可能でことになる。なお、型変数 β については、構造的性

3 実際にはより多くの関数が定義されているが、本稿では一貫して必要最小限の定義を考える。
4 なお、これは型クラスの標準的な実装方法 [16] でも
ある。

ある。

することがほとんどである。この性質を活用すればよ

この方針は Ord クラス以外でも利用できる。例えば、第 1 引数の値から第 2 引数の値までを列挙したリり精緻なテストができるのではないか、と予想するのは自然である。

ストを得る関数 enumFromTo :: ∀α.Enum a ⇒ α →しかし、残念ながら、著者が調べた範囲では、提案

α → [α] であれば、型クラス Enum が要求する関数

手法でのテストに直接役立つような良い性質を伴う型

が fromEnum :: α → Z および toEnum :: Z → α な

クラスは見つかっていない。以下では、このようなアので、これらを引数とした
enumFromTo 1を取り上げる。

:: ∀α. (α → Z) → (Z → α) → α → α → [α]を考えることになる。定理 8 により、以下を代わりにテストすれば良いことが分かる。
λf, x, y. map fst (enumFromTo 1 snd f x y):: ∀α. (Z → (α, Z)) → (α, Z) → (α, Z) → [α]この式にも定理 6・定理 7 が適用できる。
また、Haskell 2010 [13] の length 関数は、リスト

プローチの可能性を示唆する例として、束（lattice）
集合 L の上の二項関係 ⪯ が任意の a, b, c ∈ L に対して以下の 3 つの演算性質を満たすとき、(L, ⪯) を
半順序集合とよぶ。

• 反射律：a ⪯ a• 推移律：a ⪯ b かつ b ⪯ c ならば a ⪯ c• 反対称律：a ⪯ b かつ b ⪯ a ならば a = b

だけでなく様々な構造の大きさを計算できるように、半順序集合 (L, ⪯) が、任意の a, b, c, d ∈ L に対して型クラスを用いて定義されている。

以下の 6 つの性質を満たす演算 ∨L （結び、join）とlength :: ∀α, τ. Foldable τ ⇒ τ α → N∧L （交わり、meet）を伴うとき、束と呼ぶ。

ここで、Foldable クラスは型コンストラクタを表す• a ∨L b = b ∨ L a

変数 τ への制約となっており、その構造に含まれる要• a ⪯ (a ∨L b)

素を 1 列に並べて処理できることを表している。よ• a ⪯ b かつ c ⪯ d ならば (a ∨L c) ⪯ (b ∨L d)

り具体的には、toList :: τ α → [α] の定義を要求して• a ∧L b = b ∧ L a

いる 5 。よって、これを追加の引数とすると、• (a ∧L b) ⪯ alength 1 :: ∀α, τ. (τ α → [α]) → τ α → N• a ⪯ b かつ c ⪯ d ならば (a ∧L c) ⪯ (b ∧L d)となる。この定義であれば τ α を新しい変数 β だとみ束の典型的な例としては、全順序集合に対して max

なしても問題ないため、これをふまえて定理 8 を適と min を演算とした場合や、べき集合に対して包含

用すると、関係を順序とし和集合と積集合を演算とした場合が

λx. length 1 snd :: ∀α, β. (β, [α]) → N

挙げられる。また、真偽値に対して論理和・論理積演をテストすれば良いことが分かる。型変数 α, β はど算を用いる場合も束になる。特に真偽値に対する論理

ちらも計算結果に表れないため、定理 6 から 1 型へ

和・論理積を明示的に表すため、本小節ではこれらをの単相化でテストできることが分かる。

∨2 , ∧2 で表す。
いま、束をなす 2 つの演算 (∨) :: α → α → α

4. 4 順序集合上の束を伴う場合と (∧) :: α → α → α によって定義される型クラス

4. 3 節では、型クラスが定義を要求する関数についLattice を考える。そして、この型クラスに基づき定ては、適切な型であればどんな関数でもよいとみなし義される関数 g :: ∀α. Lattice α ⇒ T (α) の要素的性ていた。しかし、特に型クラスが複数の関数を要求す

質をテストすることを考える。述語としては、「あるる場合、それらの間には一定の性質が成り立つと期待値以上」かどうかを調べるもの、すなわち λx.v ⪯ x

5 標準的な定義では、toList ではなく foldr の定義を要求する。toList の定義を与えるのは foldr を与えるのと等価であり、かつテストに関する分析には明らかに toList を与える定義の方が適しているため、本稿では toList を引数としている。

の形式のものを考える。このとき、以下の性質が束の性質から直裁に導かれる。

• v ⪯ (a ∨ b) = (v ⪯ a) ∨2 (v ⪯ b)
• v ⪯ (a ∧ b) = (v ⪯ a) ∧2 (v ⪯ b)

これは、任意の束について、∨ と ∧ が定理 7 の前提

かれる。そのため、完全な束ではなく、結び半束（束

条件を満たすことを表す。以上の観察から以下の系がから交わりを除いたもの）や交わり半束（束から結び導かれる。

を除いたもの）に対しても全く同様に成り立つ。

系 9. 多相関数 g :: ∀α.Lattice α ⇒ (F0 α → G0 α) →系 9 は古典的な Knuth の 0-1 原理 [9] を導く。Knuth(F1 α → G1 α) → · · · → (Fn−1 α → Gn−1 α) → H(α)

の 0-1 原理は、値の交換による整列手順の正しさは真（ただし各 Fi , Gi（0 ≤ i ≤ n − 1）および H は関手）、

偽値の整列のみによって確認できることを主張していおよび v :: A にによって p x = v ⪯ x と定義される

る。値の交換が min と max で実現できることをふま関数 p :: A → 2 について、以下の条件が満たされる

えれば、このような整列は

sort :: ∀α.Lattice α ⇒ [α] → [α]とする。
条件 任意の fi :: Fi A → Gi A（0 ≤ i ≤ n − 1）という型を持つ関数で表すことができる 6 。系 9 はに 対 し 、Gi p ◦ fi = fi′ ◦ Fi p を 満 た す 関 数

これが 2 型への単相化でテストできることを即座に

fi′ :: Fi 2 → Gi 2 が存在する。

示す。

このとき、H に対する (acc, p) による要素的性質 ep
が g A のあらゆる出力結果で満たされるかどうかの確

全く同様の観察は他の関数にも適用できる。例えば、リストから最大値を取り出す関数

maximum :: ∀α.Ord α ⇒ [α] → α

認には、g 2 をテストすれば十分である。
系 9 は、テストしたい実装の実行結果の各要素がを考える。この関数はしばしば条件分岐ではなく max

ある値以下であると確認するには、2 型への単相化でを用いて実装される。この場合、α は Ord ではなく十分であることを主張する。この際、束の演算子であLattice クラスのインスタンスでよい。そして、以下る ∨ と ∧ もそれに従って単相化され、∨2 と ∧2 が代の型の関数

わりに使われることに注意せよ。なお、これだけでmaximum 1 :: ∀α.Lattice α ⇒ [α] → α

は、要素がある値と一致することは確認できていなであれば、系 9 から 2 型への単相化でテストできるい。これについては、以下の 2 通りの方法がある。

ことがわかる。

• ⪯ が全順序（すなわち任意の a, b ∈ L に対して

また、Morihata [15] は、交換則・結合則・冪等則a ⪯ b または b ⪯ a）の場合、a ⪯ b かつ a ̸= b

を全て満たす二項演算子を引数とする接頭辞和であを ≺ で表すとすると、λx.v ≺ x が真でありかつれば、真偽値リストに対するテストのみで正しさがλx.v ⪯ x が偽であることを調べれば v との一致保証できることを示した。この証明は以下の 2 ステッを確認できる。しかも、λx.v ≺ x の形式の述語

プからなる。

に対しても、∨ と ∧ は定理 7 の前提条件を満た

1. 既存の単相化手法 [3] [4] [8] によって、この関数

す。このことは、結局のところ、2 型への単相化のテストが二項演算子として和集合演算のみをが十分であることを意味する。

考えれば良いことを示す。

• ⪯ が全順序でない場合、λx.v ⪯ x と λx.x ⪯ v
が共に真であることを調べれば v との一致を確

2. 和集合演算の代わりに論理和を使っても十分なテストができることを示す。

認できる。全ての順序を逆にし、結びと交わり

系 9 はこの証明に異なる道筋を与える。なぜなら、を逆にした構造もまた束をなすことから、後者「あらゆる結び半束演算（これは和集合演算を含む）の形式の述語も 2 型への単相化によってテストをテストすればよい」とわかれば即座に、2 型への単することができる。ただしこのテストでは ∨ と相化で十分であることが導かれるからである。

2∧ を入れ替えて使う必要があることに注意が必2要である。
系 9 は、型クラスが要求する関数（結びと交わり）が順序関係に対して適切な条件を満たすことから導6 Knuth の 0-1 原理が min-max ネットワークに拡張できることは folklore である。また、min-max ネッ
トワークは値の交換によるネットワークより真に高い
表現力を持つ。min-max ネットワークについての詳しい議論は Levi と Litman [10] を参照されたい。

Lattice クラスについての補足する関数が有限種類であり、可能性を静的に列挙

Lattice クラスは背景に半順序があることを前提とで き る こ と に 依 存 し て い る 。そ の た め 、例 え ば

していおり、従って同値関係も定義されている。よっ∀α.[α → 2] → [α] → 2 ような型をもつ関数にはて、Lattice クラスは Eq クラスのサブクラスでなけ

適用できない。このような型は、実用上はそれほど現ればならないように思えるかもしれない。しかし、本れないようにみえるかも知れない。しかし、しばしば稿ではそのように定義していない。これは本質的で定理 8 の適用によって得られてしまう。

ある。Haskell において、ある型が Eq クラスのイン例として、与えられた関数を等価関係としたとスタンスであることは、その型の上に同値関係が定きに定義される同値類の代表元のみを残す関数

義されることではなく、その型の値を ≡ で比較する

nubBy :: ∀α.(α → α → 2) → [α] → [α] を考えプログラムが書けることを表す。本研究で導入したる。これは第 1 引数が引数に型変数 α を含むために定Lattice クラスは、値を半順序や同値関係で比較する

理 6・定理 7 を直接適用できない。そこで定理 8 を適ことは許さない。むしろ、∨ と ∧ のみで値を計算す

用すると、代わりに nubBy ′ :: ∀α.[(α, α → 2)] → [α]るからこそ、定理 9 が成り立っている。

という型の関数をテストすれば良いと分かる。しかし、これは依然として定理 6・定理 7 が適用できず、

4. 5 有限単相化テストができない例

しかも定理 8 も適用できない。nubBy 関数について

提案手法は、必ずしも全ての多相関数に適用できる

言えば、これは本質的な限界である。仮に α を有限わけではない。

種類の値（仮に n 種類とする）しかない型に単相化

まず、定理 6・定理 7 は引数の各型に対して条件をしてテストすると、nubBy は長さ n 以下のリスト

課しており、特に引数の型に多相型変数を含む関数がしか返せない。これは、テストとしては不十分であ引数の場合には適用できない。さらに、定理 8 も多る。長さ n + 1 以上の時におかしな結果を返す、以相型の要素を消費・観察する関数が返値の型に多相型

下の wrong nubBy を定義できてしまう（nubBy は変数を含まないことを要求している。以上をふまえる

nubBy の正しい実装だとする）。
wrong nubBy :: ∀α.(α → α → 2) → [α] → [α]と、引数と返値の両方に多相型変数を持つような関数
を引数とする関数に対しては、原則として提案手法はwrong nubBy eq x

適用できない 7 。
典型的な例は、foldr :: ∀α, β.(α → β → β) → β →[α] → β や、所定の条件が満たされるまで指定された関数を繰り返し適用する until :: ∀α.(α → 2) →(α → α) → α → α などの、繰り返し構造を表すコ
ンビネータが挙げられる。これは本質的な限界である。これらは、引数として与えられた関数を何度も適用し、次々と新しい値を作り出してゆくため、有限個の値を持つ型ではテストができないのは自然である。
例えば、foldr は本質的にリストのチャーチ表現に対応するため、これをテストするにはリストと同程度の表現力をもつ型を用いる必要がある。
また、定理 8 では、多相型の要素を消費・観察= let r = nubBy eq x
in if length r ≥ n then [ ] else r
同 様 の 状 況 は し ば し ば 現 れ る 。例 え ば 、あ る
要素がリストに含まれるかどうかを調べる関数

elem :: ∀α. Eq α ⇒ α → [α] → 2 も、型クラス
Eq が同値関係をパラメタとしていることをふまえて
4. 3 節の方針を適用すると、elem ′ :: ∀α. (α → α →2) → α → [α] → 2 を考えることになる。しかし、この関数には nubBy と同じ理由で提案手法を適用できない。
しかし、その関数の意図を注意深く分析しインタ
フェースを修正すれば提案手法を適用できるようになるような関数も多い。例えば elem であれば、上記は任意の α 型の要素が比較できそうな型だった

7 4. 2 節で見たように、map 関数のように、引数と返値に異なる多相型変数を含む場合、片方を定数型とみなすことで扱える場合もある。

が、本来は入力リストの要素と与えられた要素を比較したいだけのはずである。つまり、上記の型は

過剰に一般的である。代わりに、ある条件を満たため、本質的は単相型だとみなすべきである。

す要素がリストに含まれるかどうかを調べる関数

これら 79 個の関数に対し、網羅的に提案手法の適

contain :: ∀α. (α → 2) → [α] → 2 を用意し、これ用を試みた。なお、IO モナドを伴う関数については、を用いて elem a x = contain (λb. a ≡ b) x と定義す

IO が関手であり、構造的性質を確認でき、かつ要素れば十分だったはずである。そして、contain であれ抽出のための関数 acc が適切に定義できることを仮ば提案手法でテストできる 8 。

定した。IO モナドの引き起こしうるあらゆる副作用

elem 関数の例は、効率的なテストのためには、プを考えるとこの仮定は成り立たない。しかし、テスト

ログラムの意図や挙動を適切に表したインタフェースをしたいという前提であれば、副作用としては画面や（すなわち型）が必要だということを示唆する。これ

ファイル等への出力のようなものを想定するのが自然

は自明な主張ではあるが、プログラミングの際にはしであり、そうであればこの仮定は成り立つ。

ばしば無視される。特にライブラリ関数はできる限りシンプルで一般的なインタフェースが良いとされがち

なお、以上をすべて手作業で行った。提案手法の実
装・自動化は今後の課題である。

である。本研究で示した理論は、テストを効率化する

結果を表 1・2 に示す。定理 6・定理 7 が適用可能

ためにはインタフェースをどのように制限すれば良いだった物には Yes、そうでないものは空欄を記載してか、に対する一定の指針を示唆していると解することいる。また「前処理なし」の列は定理 8 を用いない場もできる。しかし、より系統的・自動的な手法を与え合、「前処理あり」は定理 8 を適用した場合を表す。

るにはさらなる調査が必要であろう。

なお、− は前処理の必要が無かったことを表す。前
処理無しで適用可能だったのは 24 個であった。前処

5 評価

理を行うことでさらに 33 個の関数が適用可能となっ提案手法がどの程度の範囲の関数に対して適用可能

た。適用できなかったのは 22 個であった。

であるかを確認するため、Haskell 98 の Prelude ラ
イブラリの関数に対する評価実験を行った。
まず、全 196 個の関数（定数を含む）の中から以下に合致する物を除き、79 個の関数を抽出した。

• 型変数を含まず、本質的に単相である関数（25個）、例えば and :: [2] → 2。

提案手法が適用できなかった 22 個は、以下の 2 類型に分類することができる。
一つは、4. 5 節で議論したように、繰り返し構造を表す高階関数である。提案手法が適用できなかった
関数の大部分（17 個）はこちらの類型に属しており、特に型クラスを伴わない関数はすべて当てはまった。

• 型変数が全て Num 型などの数値に関する型ク

また、型クラスを伴う関数のうち、モナドクラスに関ラスのインスタンスである関数（66 個）、例えばする関数もこの類型だとみなすことができる。モナ(+) :: Num a ⇒ a → a → a。これらは数値の計

ドクラスは (>>=) :: ∀m, a, b.Monad m ⇒ m a →算を伴うため、2 型や 1 型への単相化は絶望的(a → m b) → m b をパラメタとしており、これを用だと考えるのが自然である。

いて計算を繰り返すことができる型となっている。

• その型をもつ定義が 1 通り（ないしは 0 通り）しもう一つは、Eq や Ord に関する一部の関数群であかないもの（15 個）、例えば fst :: ∀α, β.(α, β) →る。4. 5 節で議論したように、これらについては、リα。これらは型のみから正しさが示せるため、テスト等を引数に含むと定理 8 の適用が行き詰まってストは不要である。

しまう。この類型に属していたのは以下の 5 個の関数

• それが型クラスの最小限の定義に含まれる物（11だが、その全てについて、下記のようにインタフェー個）、例えば Eq クラスに対する (≡)。これらはスを修正することができれば提案手法が適用できる型クラスの各インスタンスで個別に定義されることも分かった。

8 なお、全く同じ状況は、lookup :: ∀α, β. Eq α ⇒α → [(α, β)] → Maybe β でも現れる。

• maximum と minimum ：これらは、4. 4 節で議論したように、比較演算子の代わりに max また

表1
関数名
catch
concatmaybe
zipWith
(!!)
(+
+)
all
any
asTypeOf
breakconcatMap
cycle
drop
dropWhile
ﬁlter
foldl
foldl1
foldr
foldr1head
init
iteratelast
lengthmap
null
readParen
repeatreplicatereversescanl
scanl1
scanr
scanr1span
splitAt
tail
take
takeWhile
until
unzip
unzip3zip
zip3
zipWith3

Prelude 関数への適用結果（型クラスを伴わないもの）

型
IO a → (IO Error → IO a) → IO a[[a]] → [a]b → (a → b) → Maybe a → b(a → b → c) → [a] → [b] → [c][a] → Int → a[a] → [a] → [a](a → 2) → [a] → 2(a → 2) → [a] → 2a→a→a(a → 2) → [a] → ([a], [a])(a → [b]) → [a] → [b][a] → [a]Int → [a] → [a](a → 2) → [a] → [a](a → 2) → [a] → [a](a → b → a) → a → [b] → a(a → a → a) → [a] → a(a → b → b) → b → [a] → b(a → a → a) → [a] → a[a] → a[a] → [a](a → a) → a → [a][a] → a[a] → Int(a → b) → [a] → [b][a] → 22 → ReadS a → ReadS aa → [a]
Int → a → [a][a] → [a](a → b → a) → a → [b] → [a](a → a → a) → [a] → [a](a → b → b) → b → [a] → [b](a → a → a) → [a] → [a](a → 2) → [a] → ([a], [a])Int → [a] → ([a], [a])[a] → [a]Int → [a] → [a](a → 2) → [a] → [a](a → 2) → (a → a) → a → a[(a, b)] → ([a], [b])[(a, b, c)] → ([a], [b], [c])[a] → [b] → [(a, b)][a] → [b] → [c] → [(a, b, c)](a → b → c → d) → [a] → [b] → [c] → [d]

前処理なし
Yes
Yes

Yes
Yes

Yes

Yes
Yes

前処理あり
−
−
Yes
Yes
−
−
Yes
Yes
−
Yes
Yes
−
−
Yes
Yes

Yes
Yes

−
−

Yes
Yes

−
−
Yes
−
−
−
−
−

Yes
Yes
Yes
Yes
Yes

Yes
Yes
Yes

Yes
−
−
−
Yes
Yes
Yes
Yes
Yes
Yes

は min 演算子を引数として与えればよい。

る関数群に関しては、提案手法はかなりの部分を扱う• elem 、lookup と notElem ：これらは、4. 5 節で能力を持っていた。また、適用できなかったものは、議論した通り、等価演算子の代わりに、見つけた繰り返しを表しており有限値域の型への単相化ではい要素を特定する単項述語（型 a → 2）を引数

本質的にテストが不十分となる関数群がほとんどでとして与えればよい。

あった。この結果は提案手法の可能性を示していると以上を見てきたとおり、Prelude ライブラリに現れ

言えよう。

表2
関数名
enumFrom
enumFromThen
enumFromThenTo
enumFromTo
pred
succ
(̸=)
elem
lookupnotElem(=<<)(>>)
applyM
sequence
sequence
mapM
mapM
(<)
(>)
(≥)
comparemax
maximumminminimum
read
readIO
readList
readLnreads
print
showListshows
showsPrec

Prelude 関数への適用結果（型クラスを伴うもの）
型
Enum a ⇒ a → [a]Enum a ⇒ a → a → [a]Enum a ⇒ a → a → a → [a]Enum a ⇒ a → a → [a]Enum a ⇒ a → a
Enum a ⇒ a → a
Eq a ⇒ a → a → 2
Eq a ⇒ a → [a] → 2
Eq a ⇒ a → [(a, b)] → Maybe b
Eq a ⇒ a → [a] → 2
Monad m ⇒ (a → m b) → m a → m b
Monad m ⇒ m a → m b → m b
Monad m ⇒ (a → m b) → m a → m b
Monad m ⇒ [m a] → m [a]Monad m ⇒ [m a] → m 1
Monad m ⇒ (a → m b) → [a] → m [b]Monad m ⇒ (a → m b) → [a] → m 1
Ord a ⇒ a → a → 2
Ord a ⇒ a → a → 2
Ord a ⇒ a → a → 2
Ord a ⇒ a → a → Ordering
Ord a ⇒ a → a → a
Ord a ⇒ [a] → a
Ord a ⇒ a → a → a
Ord a ⇒ [a] → a
Read a ⇒ String → a
Read a ⇒ String → IO a
Read a ⇒ ReadS [a]Read a ⇒ IO a
Read a ⇒ ReadS a
Show a ⇒ a → IO 1
Show a ⇒ [a] → ShowSShow a ⇒ a → ShowSShow a ⇒ Int → a → ShowS

前処理なし

前処理あり
Yes
Yes
Yes
Yes
Yes
Yes
Yes

Yes
Yes
Yes
Yes
Yes
Yes
Yes
Yes
Yes
Yes
Yes

−
−
−
−
−
Yes
Yes
Yes
Yes

リストに対してテストするならば、「入力リストの何6 議論番目の値か」を区別することで、つまり入力として6. 1 既存の単相化手法との比較[0, 1, . . . , n − 1] をテストすることを求める。

パラメトリック多相型関数の単相化によるテスト手

以降、これら既存手法と提案手法を比較する。な法は、既存の複数の研究が提案している。著者の知る

お、既存手法にはそれぞれ細部に技術的な差があるた限り、この問題を始めて取り扱ったのは Bernardy らめ、以降では原則として Hou と Wang による手法と[3] である。ほとんど同時期に、Christiansen と Seidel

比較する。

[4] は正格性の分析の文脈で非常によく似た議論を行っ

テストによって多相関数の正しさを完全に確かめている。Hou と Wang [8] はこれらの議論に型理論のようとした場合、多くの場合において、提案手法の方観点から精緻かつより一般的な定式化を与えている。

が「より小さなサイズのデータを、より多くの回数」

1 節で論じたとおり、これらの研究はいずれも「多テストすることを要求する。例えば先の reverse 関数

相型変数に対応する値がどう得られるか」に注目すであれば、既存手法は整数のリスト（n log n ビット）る。例えば、reverse :: ∀α.[α] → [α] 関数を長さ n のを 1 回テストすれば十分だと主張するのに対し、提案手法は真偽値のリスト（n ビット）を網羅的に（2nるので、このような問題は起こらない。

回 9 ）テストすることを求める。よって、この例に関手法の適用範囲は、原則として既存手法の方が広しては、既存手法の方が効率が良いと言える。なお、

い。例えば、既存手法であれば、提案手法では扱えな提案手法にも、インクリメンタルにテストができる、

い foldr :: ∀α, β.(α → β → β) → β → [α] → β 関数

テストの並列化ができる、等のメリットがないわけでに対しても、foldr (:) [ ] x = x が成り立つことを確認はない。

すれば十分である、ということを示すことができる。

しかし、「より少ない回数のテストで十分」という

ただし、このテストは実質的には foldr の実行トレー主張がどの程度実用上の意味を持つかは微妙ではあス（第 1 引数・第 2 引数をどのように使って計算結果る。reverse 関数であっても、正しさを完全に確かめを構築したか）を完全に覚えていることになるので、ようとした場合、任意の長さのリストについてテスト

効率的なテストだと言えるかどうかは微妙である。逆しなければならず、有限のテストでは完遂できない。

に提案手法は、単相化によってある程度効率的なテ

この状況は引数が増えるとたちまち悪化する。例えストが可能になるための条件を示していると解する

ば、take :: ∀α.N → [α] → [α] 関数であれば、リストこともできる。また、例えば整列に対する Knuth のに加えて自然数を与えてテストする必要があり、自然0-1 原理 [9] に関して言えば、既存手法 [3] よりも提案

数も有限種類ではない。

手法の方がより直接的な導出に成功している。

型がより複雑になると、効率の比較もさらに微妙

以上の状況をふまえると、既存手法と提案手法はどとなる。例として g1 :: ∀α.([2] → α) → N → α といちらが優れているともいえないと考えられる。上手くう型の関数を考える。既存手法であれば、第 1 引数組み合わせる方法があればより望ましいが、これは今の関数からどのように α 型の値を得たかに注目する後の課題である。

ので、引数である関数の引数の型、すなわち [2] 型で型変数 α を単相化する。より具体的には、第 1 引数

6. 2 値の観察への注目について[2]
を id 関数とした g1 id :: N → [2] のテストを要求す

前述の通り、既存手法は値が得られる手順に注目する。この場合、出力結果はリストとなるので、そのる。圏論の言葉を使うならば、既存手法は値が得られ要素的性質のテストを O(1) 時間で行うのは絶望的にる手順を表す始代数を構築し、その始代数で単相化を見える。一方で、提案手法であれば、この代わりに行う。これに対し、本研究では、「値をどのように観

g12 :: ([2] → 2) → N → 2 のテストを要求する。第 1

察するか」に注目して理論を構築した。

引数を id 関数に固定できていないというデメリット

Xia [26] は他の既存手法の圏論的双対として、終代はあるが、すくなくとも出力結果の確認は O(1) 時間

数で値が壊される手順を表すことで単相化を行う手法

で行うことができる。

を提案した。提案手法は一見すると Xia の手法と非さらに、g2 :: ∀α.((N → N) → α) → [α] という型

常に関連が深そうだが、現時点では両者の関係性はよの関数を考えると、既存手法では N → N 型の関数でく分かっていない。既存手法と Xia らの手法もどち型変数 α を単相化しようとする。しかし、これは望らも、最終的には多相関数と等価な単相関数を得る。

ましいことではない。この関数の実行結果を参照実装

よって両者の単相化結果は等価である。既に見てきたと比較しようとしても、「N → N 型の関数同士が等しとおり、本研究では、最終的にどのような述語等を用い」ことを確かめることはできない。提案手法であれ

いてテストを行うかを活用することで、単相化前の多ば、やはり 2 型への単相化が十分であることが分か

相関数とは本質的に等価でない関数をテストする。
本研究では、構造的性質と要素的性質の区別によっ9 実際には、入力が全て異なるリストをテストすれば十分であることが既存手法から分かるので、これをふまえれば、提案手法でも 1 つだけ True をふくむ n 通りの真偽値リストを試せば十分である。

て、どのような単相化が可能かを論じている。この方針は、Abbott らの container type [1] [2] の影響を受けている。Container type はデータを格納するような構造に対し、その「形（shape）」と「アクセス方

リズムについては 0-1 原理が成り立つことを示した。

法（positions）」によって捉えることで、一般的かつ

この 0-1 原理を本研究の枠組みで捉えることができる

理論的にシンプルな定式化を与えている。

かについても今後の課題である。

Container type に基づいていることは、実用上も多少のメリットがある。既存手法では、値の構成手法

6. 4 今後の課題を完全に追うために、多相型関数がデータ型に関する

本研究に残された直接的な課題は提案手法の自動化計算を行っていた場合、そのデータ型が代数的データである。特に、定理 8 を型同型（例えばカリー化・反型であること、そしてそのデータ型の完全な定義がカリー化）をふまえつつ繰り返し適用してテスト可能

手に入ることを要求している。しかし、この要求は、な式を導出するのは、原理的にはそれほど難しくない

そのデータ型が（特にライブラリ等で定義された）抽が実際にはかなり煩雑である。これを自動化するシス

象データである場合や、型クラスで抽象化されている

テムは、より大規模な実験等には不可欠だと考える。

場合などには満たされない。提案手法では、そのデー本研究では、構造的性質と要素的性質についてのタ型が関手であること、およびそのデータ型の要素が議論を行った。しかし、プログラムの仕様の中には、アクセスできることを求めるにとどめており、データ

これらどちらとも言えないようなものも少なからず型の詳しい定義を要求せずに済んでいる。

ある。例えば整列アルゴリズムについて考えると「値が小さい順に並ぶ」「入力に含まれる値と出力に含ま6. 3 Knuth の 0-1 原理とその亜種

れる値は集合としては一致する」といったことが最も

本研究の動機の一つは、Knuth の 0-1 原理 [9] のよ

自然な仕様だが、これらはどちらも構造的性質・要素

うなテスト手法を与える一般的な方法を構築するこ的性質ではないように見える。これに対し、本研究でとである。

は「結果の i 番目の要素が参照実装の i 番目の要素と著者の知る限り、Knuth の 0-1 原理と多相型パラ一致する」というような形で要素的性質に翻訳し、間メトリシティとの関係を初めて示したのは Day ら [6]

接的に正しさを確認している。このような翻訳は多くである。Day らは整列に特化した議論を行っていたの場合可能だと思われるが、翻訳方法自体が非自明なが、本研究では 4. 4 節においてこの議論を束に一般化場合もあるかも知れない。より系統的な方法を模索すした。また、Knuth の 0-1 原理の亜種としては、ソーる余地は残っている。

ト済み列の併合 [14]、上位と下位の分離 [11]、二分割評価実験 5 からも見て取れるように、実用性の観[7] などが提案されている。本研究の成果はこれらを点からは型クラスの扱いは不可欠である。型パラメト

ほとんど即座に導出できる。

リシティの観点から型クラスを扱う研究はいくつかあVoigtländer [21] は、結合的二項演算子を用いた接る [22] [20] ので、これらも参照しつつ、より広い範囲

頭辞和計算において、真偽値（2 種類の値）ではなくの型クラスを扱う方法や、テストに適した型クラス・3 種類の値でテストすれば十分であるという、「0-1-2

適さない型クラスを判別する手法などを与えること原理」を示した。Morihata [15] はこの結果をふまえ、も今後の課題である。

二項演算子が結合的・交換的であるだけでは真偽値のテストは不十分であり、結合的・交換的・冪等的であ

謝辞 本研究は JSPS 科研費 23K11044 の助成を受けている。

れば十分となることを示した。本研究では、4. 4 節において、Morihata の結果と Knuth の 0-1 原理との

参 考 文 献関係を示した。Voigtländer の 0-1-2 原理についても[ 1 ] Michael Gordon Abbott, Thorsten Altenkirch,
and Neil Ghani. Categories of containers. In
Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6thInternational Conference, FOSSACS 2003 Held as同様に理解できるかは、今後の課題である。

Maric ら [12] は分散合意形成アルゴリズムを記述するための言語を設計し、この言語で記述できるアルゴ

Part of the Joint European Conference on Theory
and Practice of Software, ETAPS 2003, Warsaw,
Poland, April 7-11, 2003, Proceedings, volume 2620
of Lecture Notes in Computer Science, pages 23–38.
Springer, 2003.
[ 2 ] Michael Gordon Abbott, Thorsten Altenkirch,
and Neil Ghani. Containers: Constructing strictly
positive types. Theor. Comput. Sci., 342(1):3–27,
2005.
[ 3 ] Jean-Philippe Bernardy, Patrik Jansson, andKoen Claessen. Testing polymorphic properties.
In Andrew D. Gordon, editor, Programming Languages and Systems, 19th European Symposium on
Programming, ESOP 2010, Held as Part of the
Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus,
March 20-28, 2010. Proceedings, volume 6012 of
Lecture Notes in Computer Science, pages 125–144,
Berlin, Germany, 2010. Springer.
[ 4 ] Jan Christiansen and Daniel Seidel. Minimallystrict polymorphic functions. In Peter SchneiderKamp and Michael Hanus, editors, Proceedings ofthe 13th International ACM SIGPLAN Conference
on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark, pages
53–64. ACM, 2011.
[ 5 ] Nils Anders Danielsson, John Hughes, Patrik
Jansson, and Jeremy Gibbons. Fast and loose reasoning is morally correct. In J. Gregory Morrisettand Simon L. Peyton Jones, editors, Proceedingsof the 33rd ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL
2006, Charleston, South Carolina, USA, January
11-13, 2006, pages 206–217. ACM, 2006.
[ 6 ] Nancy A. Day, John Launchbury, and Jeﬀ Lewis.
Logical abstractions in Haskell. In Proceedings ofthe 1999 Haskell Workshop, Utrecht, Netherlands,
October 1999. Utrecht University Department ofComputer Science, Technical Report UU-CS-199928.
[ 7 ] Guy Even, Tamir Levi, and Ami Litman. Optimal conclusive sets for comparator networks. Theor.
Comput. Sci., 410(14):1369–1376, 2009.
[ 8 ] Kuen-Bang Hou and Zhuyang Wang. Logarithm
and program testing. Proc. ACM Program. Lang.,
6(POPL):1–26, 2022.
[ 9 ] Donald Knuth. The Art of Computer Programming, volume 3. Addison Wesley Longman, Boston,
MA, USA, second edition, 1998.
[10] Tamir Levi and Ami Litman. The strongest
model of computation obeying 0-1 principles. Theory Comput. Syst., 48(2):374–388, 2011.
[11] Shuo-Yen Robert Li. Uniﬁed algebraic theoryof sorting, routing, multicasting, and concentration
networks. IEEE Trans. Commun., 58(1):247–256,
2010.
[12] Ognjen Maric, Christoph Sprenger, and David A.
Basin. Cutoﬀ bounds for consensus algorithms.

In Rupak Majumdar and Viktor Kuncak, editors,
Computer Aided Veriﬁcation - 29th International
Conference, CAV 2017, Heidelberg, Germany, July
24-28, 2017, Proceedings, Part II, volume 10427 of
Lecture Notes in Computer Science, pages 217–237.
Springer, 2017.
[13] Simon Marlow.
Haskell 2010 language report. Available from https://www.haskell.org/
onlinereport/haskell2010/, 2009.
[14] Peter Bro Miltersen, Mike Paterson, and Jun
Tarui. The asymptotic complexity of merging networks. J. ACM, 43(1):147–165, 1996.
[15] Akimasa Morihata. When does 0-1 principle
hold for preﬁx sums?
New Gener. Comput.,41(3):523–531, 2023.
[16] John Peterson and Mark P. Jones. Implementing type classes. In Robert Cartwright, editor, Proceedings of the ACM SIGPLAN’93 Conference on
Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June
23-25, 1993, pages 227–236. ACM, 1993.
[17] Simon Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge, UK, 2003.
[18] John C. Reynolds. Types, abstraction andparametric polymorphism. Information Processing,
83:513–523, 1983.
[19] Donald Sannella, Michael Fourman, Haoran
Peng, and Philip Wadler. Introduction to Computation - Haskell, Logic and Automata. Undergraduate
Topics in Computer Science. Springer, 2021.
[20] Daniel Seidel and Janis Voigtländer. Proving
properties about functions on lists involving element
tests. In Till Mossakowski and Hans-Jörg Kreowski,
editors, Recent Trends in Algebraic Development
Techniques - 20th International Workshop, WADT
2010, Etelsen, Germany, July 1-4, 2010, Revised
Selected Papers, volume 7137 of Lecture Notes in
Computer Science, pages 270–286. Springer, 2010.
[21] Janis Voigtländer. Much ado about two (pearl):a pearl on parallel preﬁx computation. In George C.
Necula and Philip Wadler, editors, Proceedingsof the 35th ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL
2008, San Francisco, California, USA, January 712, 2008, pages 29–35, New York, NY, USA, 2008.
ACM.
[22] Janis Voigtländer. Free theorems involving type
constructor classes: functional pearl. In Graham
Hutton and Andrew P. Tolmach, editors, Proceedingof the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2,
2009, pages 173–184. ACM, 2009.
[23] Janis Voigtländer. Free theorems simply, via dinaturality. In Petra Hofstedt, Salvador Abreu, Ulrich John, Herbert Kuchen, and Dietmar Seipel,
editors, Declarative Programming and Knowledge

Management - Conference on Declarative Programming, DECLARE 2019, Unifying INAP, WLP,
and WFLP, Cottbus, Germany, September 9-12,
2019, Revised Selected Papers, volume 12057 of Lecture Notes in Computer Science, pages 247–267.
Springer, 2019.
[24] Philip Wadler. Theorems for free! In FPCA’89
Conference on Functional Programming Languages
and Computer Architecture. Imperial College, London, England, 11-13 September 1989, pages 347–
359. ACM, New York, 1989.

[25] Philip Wadler and Stephen Blott. How to makead-hoc polymorphism less ad-hoc. In Conference
Record of the Sixteenth Annual ACM Symposiumon Principles of Programming Languages, Austin,
Texas, USA, January 11-13, 1989, pages 60–76.
ACM Press, 1989.
[26] Li-yao Xia. A terminal view of testing polymorphic functions. Blog post，https://blog.poisson.
chat/posts/2017-06-29-terminal-monomorphization.
html, 2017.