Executive Summary
忙しくて本文をお読みになれない方のために、本稿の内容をここにまとめます。
本文だけをお読みになる方は、この節を読み飛ばしても差し支えございません。
本文は、この節を読んでいなくても理解できるように書いてあります。
本稿の問い
初回記事では、Haskell のコンパイラ GHC が、圏論の法則を書き換え規則として使い、プログラムを速くしていることを見ました。
本稿の問いは、初回記事で扱った最適化手法を、Haskell 以外の関数型言語でも使えるのか という点にあります。
本連載の4つの分類軸で、11の関数型言語を整理する
本連載は、関数型言語と定理証明言語を、型理論、評価戦略、論理体系、言語機能の4つの軸で整理 します。
この4軸は、研究者のあいだで確立された分類ではなく、本連載が独自に組み立てたものです。
個々の軸は教科書に載っている標準的なもので、独自なのは4つを並べて使う点だけ です。
詳しくは第2章でご説明します。
言語名の前の記号は、グループを示します。
- $A$ は 静的型付け で 非正格評価 の言語
- $B$ は 静的型付け で 正格評価 の言語
- $C$ は 動的型付け の言語
Haskell は初回記事で扱った言語で、比較のために 載せています。
関数型言語の分類表:4つの分類軸
| 言語 | 型理論 | 評価戦略 | 論理体系 | 言語機能 |
|---|---|---|---|---|
| 【A】Haskell(参考) | 静的型付け。多相型(rank-N polymorphism、higher-kinded type) | 非正格 | 特に制約はない | 型クラス、RULES プラグマ(書き換え規則)、seq
|
| 【A】Clean | 静的型付け。多相型(rank-2 までの型、type constructor class)、一意型 | 非正格(! による正格性の注釈が可能) |
特に制約はない | 型クラス、一意型、コンパイラによる融合変換 |
| 【A】Miranda | 静的型付け。多相型(Hindley-Milner 型。rank-1 のみ) | 非正格 | 特に制約はない | 型クラスなし、seq
|
| 【B】PureScript | 静的型付け。多相型(rank-N polymorphism、higher-kinded type)、row polymorphism | 正格 | 特に制約はない | 型クラス、Partial 型クラス、Effect 型 |
| 【B】OCaml | 静的型付け。多相型(rank-1。polymorphic record field で rank-2 type を表す) | 正格(評価順序は仕様上未規定。lazy による遅延評価が可能) |
特に制約はない | モジュールとファンクタ、Flambda、代数的エフェクト(OCaml 5) |
| 【B】Standard ML | 静的型付け。多相型(rank-1 のみ) | 正格 | 特に制約はない | モジュールとファンクタ、形式仕様、MLton の whole-program optimization |
| 【B】Scala | 静的型付け。多相型(higher-kinded type。polymorphic method で rank-2 type を表す) | 正格(by-name parameter と view による遅延評価が可能) |
特に制約はない | implicit による型クラス(Cats)、view
|
| 【B】F# | 静的型付け。多相型(higher-kinded type なし。generic method で rank-2 type を表す) | 正格(Seq と lazy 式による遅延評価が可能) |
特に制約はない |
inline 関数、Seq、型クラスなし |
| 【C】Clojure | 動的型付け | 正格(lazy sequence による遅延評価が可能) | 特に制約はない | transducers、マクロ |
| 【C】Erlang | 動的型付け | 正格(部分式を先に評価することが仕様で定められている) | 特に制約はない | パターンマッチとガード、型情報にもとづく JIT(OTP 25) |
| 【C】Common Lisp | 動的型付け | 正格(引数を左から右へ評価してから関数を呼ぶことが仕様で定められている) | 特に制約はない | マクロ、コンパイラマクロ、型宣言 |
| 【C】Lisp | 動的型付け | 方言によって異なる(Racket には遅延評価を既定とする Lazy Racket がある) | 特に制約はない | Common Lisp、Scheme、Racket、Clojure などを方言とする言語族。歴史的な言及にとどめる |
言語比較: 8つの最適化手法は各言語で使えるか
連載初回の記事 で取り上げた (圏論知見から導かれる)8つの最適化手法 について、それぞれの関数型言語で利用可能かどうか を 表 にまとめました。
8つの最適化手法 の詳細については、この Executive Summary の後の 「本稿(連載第2回)で扱う最適化手法の一覧」 をご参照ください。
| 最適化手法 | 使える | 条件付きで使える | 使えない |
|---|---|---|---|
第3章 map の書き換え規則(Functor 則。2回の map を1回にまとめる。map f (map g xs) を map (f . g) xs に書き換える) |
Haskell(参考)、Clean、Miranda、PureScript | OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | ── |
| 第4章 foldr/build の書き換え規則(始代数。中間リストを作らない。rank-2 type を要する) | Haskell(参考)、Clean、PureScript | OCaml、Scala、F# | Miranda、Standard ML、Clojure、Erlang、Common Lisp |
| 10-1 foldMap(Monoid 準同型) | Haskell(参考)、Clean、Miranda、PureScript | OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | ── |
10-2 Traversable(自然性。2回の走査を1回にまとめる。traverse を2回呼び出すコードを、traverse を1回だけ呼び出すコードに書き換える。higher-kinded type を要する) |
Haskell(参考)、Clean、PureScript | OCaml、Standard ML、Scala | Miranda、F#、Clojure、Erlang、Common Lisp |
| 10-3 bind の再結合(Monad 則の結合律) | Haskell(参考)、Clean、Miranda、PureScript、OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | ── | ── |
| 10-4 Difference List(自己準同型のモノイド。計算量が変わる) | Haskell(参考)、Clean、Miranda、PureScript、OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | ── | ── |
| 10-5 Codensity(Kan 拡張。higher-kinded type と rank-2 type を要する) | Haskell(参考)、Clean、PureScript | OCaml、Scala、F# | Miranda、Standard ML、Clojure、Erlang、Common Lisp |
| 10-6 Applicative による全エラー集約(積構造) | Haskell(参考)、Clean、PureScript、OCaml、Standard ML、Scala | Miranda、F#、Clojure、Erlang、Common Lisp | ── |
最適化手法を使えるかの表の3つの列は、次の基準で分けました。
| 列 | 基準 |
|---|---|
| 使える | その手法の正しさを支える条件が、言語の性質によって満たされる。標準の言語機能で書ける。書き方が Haskell と異なる場合を含む |
| 条件付きで使える | 書けるが、言語が保証しない条件を、プログラマが自分で満たす必要がある |
| 使えない | その手法の正しさを支える型の保証を、言語の中で表現できない |
なお、上の表の 「使えない」の列 は、
- その言語では途中のデータを作らずに計算できない
- 計算量を減らせない
という意味ではありません。
次の2つのいずれかにあたるという意味 です。
- 初回記事で扱った形のままでは、その言語で書けない
- 書けるが、その書き換えが正しいことを、言語が検査してくれない
筆者は、このことを実機で確かめました。
Clojure、Erlang、Common Lisp で、foldr/build、Traversable、Codensity の規則を満たさない関数 をあえて書いても、どの言語もエラーを出さず、書き換えの前後で結果が変わりました。
Haskell、OCaml、PureScript は、コンパイルの段階で拒否されることを確認** しました。
言語によって結果が大きく分かれるという観察結果が得られました。
結果を分けたのは、型による保証の有無 です。
静的型付け の言語では、rank-2 type と パラメトリシティ によって、規則を満たさない関数をそもそもコードに記述することが許されません。
rank-2 type とは、forall(どんな型についても、という宣言)を、関数の引数の型の中に置くことができる型 のことです。この形で書くと、受け取った関数は、その中身の型を調べることができなくなります。
パラメトリシティ とは、そのようにして型の中身を調べられない関数は、どの型に対しても同じ形の処理しかできない、という性質です。中身を見られない以上、型ごとに処理を変えることができない からです。
ここで、初回記事で扱った foldr/build の規則 を思い出して下さい。
その規則とは、foldr c n (build g) = g c n。リストを作ってから畳み込む代わりに、リストを作らずに直接畳み込んでよい、という規則でした。
この規則が成り立つのは、build に渡す関数 g が、リストを組み立てる部品の中身を調べずに、どの部品に対しても同じ形で組み立てる場合だけ です。
g が 部品の中身を見て処理を変えると、リストを作った場合と作らなかった場合とで、結果が変わってしまいます。
rank-2 type は、まさにその「中身を調べる」ことを型の段階で禁じます。
その結果、規則を満たさない g は、そもそも build に渡せる型を持つことが許されないため、コンパイルが拒絶してくれるのです。
つまり、rank-2 type で型の中身を隠せば、パラメトリシティによって「どの型でも同じ処理をする」ことが保証され、規則の成立に必要な条件が満たされます。 規則を満たさない関数は、そもそもこの型を持てないため、コンパイルを通らないのです。
それに対して、動的型付け の言語では、規則を満たさない関数をコードに記述することが許されてしまう ため、誤った書き換えが紛れていることには、コードが実行されるまで気づくことができない のです。
恒等律の破れは、Haskell だけの問題ではない
初回記事 では、*Haskell の seq と底によって、恒等律が成り立たなくなること を見ました。
上記は、Haskが厳密には圏ではない理由 として、初回記事で注目しました。
この点は、Hask圏 について論じている多くの解説記事でも取り上げられている論点です。
実務上の慣行として、Haskが厳密には圏ではない ことを認識した上で、Hask圏 という言葉が使われています。
本稿では、seq に底を渡す式と、その底に id を合成した式を、Haskell の前身にあたる Miranda という言語 で評価してみました。
| 言語 | seq bottomfn 1 |
seq (bottomfn . id) 1 |
|---|---|---|
| Haskell(GHC 9.4.7) | 例外 | 1 を返した |
| Miranda(2.066) | 例外 | 1 を返した |
bottomfn は、評価すると例外を投げる関数です。
恒等律 によれば、bottomfn と bottomfn . id は等しいはずです。
しかし、どちらの言語でも、上記の2つは 区別されてしまいました。
Miranda は1985年に登場した、Haskell の前身にあたる言語 です。
同じ現象が2つの言語で起きたことから、恒等律の破れは Haskell 固有の問題ではないことが分かります。
非正格評価であることと、seq を持つことの2つがそろえば、同じ問題が生じてしまいます。
Haskell も Miranda も、この2つの条件が揃った ことで、bottomfn と bottomfn . id が等しい結果にならず、互いに異なるものとして判断 されてしまい、恒等律が破れてしまった のです。
| 観点 | 内容 |
|---|---|
| 事実関係 |
seq bottomfn 1 と seq (bottomfn . id) 1 は、同じ結果を生まなかった。前者は例外を発生させ、後者は 1 を返した。この違いが、Haskell と Miranda の両方で観測された |
| 論理 | 恒等律は「f . id = f」が成り立つことを要求している。したがって、bottomfn と bottomfn . id が等しいのであれば、その2つを seq に渡したときの結果も、同じでなければならない。しかし、異なる結果になった。このことは、seq がこの2つを区別していることを示しており、恒等律が成り立っていないことになる |
| 原因の特定 | 「非正格評価であること」と「seq を持つこと」の2つが原因である。正格評価の言語であれば、bottomfn . id という式を作った時点で評価が行われるため、この差は生じない。また、seq を持たない言語であれば、底を強制的に評価する手段そのものがないため、2つの式を区別できない |
| 用語 | 恒等律が破れたとは、圏の公理である「どの射 f についても f . id = f かつ id . f = f が成り立つ」という要請が満たされないことを指す |
なお、Miranda は型クラスを持ちません。
それでも同じ問題が起きたことから、型クラスの有無は、この現象と無関係である ことも分かります。
本連載の4軸でいえば、この問題は評価戦略の軸 に属します。
PureScript は、Haskell とほぼ同じ型システムを持ちながら、正格評価の言語 です。
PureScript では、関数が使わない引数に、評価すると例外を投げる式を渡しただけで、例外が発生しました。
正格評価の言語 は、関数を呼ぶ前に引数をすべて評価するため、使われない引数であっても、引数を評価するため、漏れなく例外を発生してくれるのです。
Haskell では、同じ形の式が 例外を発生させませんでした。
Haskellのように非正格評価の言語 は、引数が実際に必要になるまで評価しません。
この関数は渡された引数を一度も参照しないため、例外を投げる式が評価されることはなかったのです。
| 言語 |
(\_ -> 1) に底を渡す |
結果 |
|---|---|---|
| Haskell | (\_ -> 1) (error "bottom") |
1 を返した |
| PureScript | (\_ -> 1) (crash unit) |
例外を投げた |
型システムがほぼ同じでも、評価戦略だけが違うことで、まったく異なる結果を生み出す のです。
評価戦略の違いが、この違いをもたらすことが観測できました。
詳しくは第4章でご説明します。
本記事の結論
- 本稿は、Haskell 以外の11の関数型言語 を、型理論、評価戦略、論理体系、言語機能の4軸で整理 しました。そのうえで、初回記事で扱った8 つの最適化手法が、各言語で使えるかどうかを判定 しました。
- 11の関数型言語のうち、歴史的な言及にとどめた Lisp を除く10の言語と、比較のための Haskell を、筆者が実機で検証しました。Clean は、Wine の上で Windows 版を動かして検証しました
-
Difference List は、評価戦略も型付けも問わず、検証した10の関数型言語すべてで桁違いに速くなりました。 計算量そのものが変わる手法だから です
- 2回の map を1回にまとめる最適化(
map f (map g xs)をmap (f . g) xsに書き換える最適化)がどれだけ効くかは、評価戦略で決まりました。
正格評価の言語 では、プログラマが自らコードを記述して書き換えると 1.56 倍から 4.09 倍速くなりました。
遅延評価 の Miranda では、1.05 倍にとどまりました
-
Haskell 以外の言語のコンパイラ は、
map f (map g xs)をmap (f . g) xsに 自動では書き換えてくれませんでした。
GHC が自動で行う書き換えを、他の言語では、プログラマ自身、ライブラリの作者、言語の設計者が担っています
- 初回記事で見た 恒等律の破れは、Haskell 固有の問題ではありませんでした。
1985年に登場した Miranda でも、まったく同じ形で再現 しました
- 型システムがほぼ同じで評価戦略だけが違う Haskell と PureScript では、同じ形の式が違う結果になりました。評価戦略の違いが、上記の異なる結果につながる事実を観察されました
- Standard ML の MLton では、関数をモジュールやファンクタで包んでも、性能は変わりませんでした(差は3パーセント未満)
-
動的型付けの Erlang でも、処理系の内部では型が推論されていました。
型が分かる加算では、JIT が生成する命令が14から5に減りました
- 初回記事で見た Codensity、Traversable の2回の走査を1回にまとめる書き換え、foldr/build の効果は、Haskell の外でも成り立ちました。
OCaml、Scala、PureScript などで、rank-2 type を各言語の仕組みで表して書くと、同じように速く なりました
- 副作用を許す7つの言語では、2回の map を1回にまとめる(
map f (map g xs)をmap (f . g) xsに 書き換える)と、返す値は同じでも副作用の起きる順序が変わりました。
これらの言語で書き換えを使うには、関数に副作用がないことをプログラマが保証する必要があります
- OCaml の最適化の仕組み Flambda を有効にしても、
map f (map g xs)はmap (f . g) xsに書き換えられませんでした。一方、Scala の Cats のライブラリ cats-free は、左結合に重なった bind を内部で組み替えていました。圏論の知識を使う主体は、処理系の最適化の仕組みではなく、ライブラリの作者である場合もあります
-
動的型付け の Clojure、Erlang、Common Lisp では、foldr/build、Traversable、Codensity の規則を満たさない関数を書いてもエラーにならず、書き換えの前後で結果が変わりました。
静的型の言語 では、同じ関数が コンパイルで拒否 されました。
型が守っているのは、書き換えの正しさ です
本稿で実機検証した最適化とその効果を、言語ごとに表にまとめ結果が、以下の表です。
言語ごとの、実機検証した最適化手法とその効果の表
| 言語 | 実行した最適化手法 | 最適化の効果 |
|---|---|---|
| Haskell(参考) | GHC の書き換え規則(map f (map g xs) を map (f . g) xs に書き換える)map f (map g xs) を、プログラマが自ら map (f . g) xs と記述する(書き換え規則を無効にした場合)Difference List Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すfoldr/build(書き換え規則の有無) |
map f (map g xs) と記述したコードが 49.5 ms から 10.7 ms になった(4.6 倍)1.76 倍速くなった 15,107.8 ms が 0.2 ms になった 0.8968 s が 0.000074 s になった 1.74 倍速くなった 規則を無効にすると 19.8 ms が 26.9 ms になった |
| Miranda |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するDifference List foldMap、bind の再結合、エラーを集める検証を特定の型で書く |
1.05 倍にとどまった 27,219 ms が 23 ms になった(起動時間を含む) いずれも実行に成功した |
| PureScript |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するDifference List Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すfoldr c 0 (build g) を、プログラマが自ら g c 0 と記述する(要素数 10,000) |
2.29 倍速くなった 18,396.5 ms が 9.5 ms になった 1.8351 s が 0.0072 s になった 1.69 倍速くなった 4.3 倍速くなった |
| OCaml |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するDifference List リストの連結を右結合に変える Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すfoldr c 0 (build g) を、プログラマが自ら g c 0 と記述するFlambda を有効にして、 map f (map g xs) と map (f . g) xs を測り直す |
2.03 倍速くなった。確保したメモリは半分になった 23,390.6 ms が 0.8 ms になった 1,307 倍速くなった 0.2297 s が 0.000571 s になった 1.99 倍速くなった 24.5 倍速くなった map (f . g) xs と記述したコードとの差は 2.10 倍で、Flambda なし(2.05 倍)とほぼ同じ。Flambda は map (f . g) xs に書き換えなかった |
| Standard ML |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するDifference List 関数をモジュールやファンクタで包む traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すTraversable をファンクタとして書く |
1.75 倍速くなった 11,989.0 ms が 0.3 ms になった 性能は変わらなかった(差は3パーセント未満) 1.83 倍速くなった コンパイルと実行に成功した |
| Scala |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するview を挟むDifference List リストの連結を右結合に変える Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すfoldr c 0 (build g) を、プログラマが自ら g c 0 と記述するCats の Traverse(Scala 3.3.6) Cats の Chain(Scala 3.3.6) cats-free の Free(左結合の flatMap、Scala 3.3.6) |
4.09 倍速くなった 17.7 倍速くなった 4,024.3 ms が 9.2 ms になった 930 倍速くなった 0.3182 s が 0.000353 s になった 4.89 倍速くなった 6.82 倍速くなった 2.98 倍速くなった 3,350.7 ms が 4.97 ms になった n が倍になってもおよそ 1.5 倍から 1.9 倍の伸びにとどまった |
| F# |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するSeq を使うinline 関数にするDifference List foldr c 0 (build g) を、プログラマが自ら g c 0 と記述する |
1.94 倍速くなった 5.3 倍速くなった 差は出なかった(1.04 倍) 31,680.7 ms が 1.3 ms になった 28.8 倍速くなった |
| Clojure |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するtransducers を使う Difference List JVM 上の通常の Clojure で同じ測定を行う |
1.23 倍速くなった 1.63 倍速くなった 45,795.6 ms が 8.8 ms になった 絶対値はおよそ10分の1になったが、倍率の傾向は変わらなかった(プログラマが自ら map (f . g) xs と記述したコードで 1.19 倍、transducers で 1.85 倍) |
| Erlang |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するリスト内包表記を使う Difference List 型が推論される形で加算を書く |
1.83 倍速くなった 2.02 倍速くなった 3,503.4 ms が 2.2 ms になった 加算の命令が14から5に減り、1.07 倍速くなった |
| Common Lisp |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するloop を使うDifference List 型を宣言する |
1.56 倍速くなった 約14倍速くなった(測定の分解能は4ミリ秒) 3,504 ms が4ミリ秒未満になった 10.8 倍速くなった |
| Clean | Clean のコンパイラの融合変換(同じモジュールで定義した map、要素数 10,000,000) Clean のコンパイラの融合変換(標準ライブラリの map) foldr/build と Clean のコンパイラの融合変換 Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すDifference List 一意型 による配列の破壊的更新(10 万回) |
199 ms が 99 ms になった(2.0 倍) 効かなかった 70 ms が 18 ms になった 1,060 ms が 1 ms 未満になった 1.12 倍速くなった 12,459 ms が 1 ms 未満になった 1 ms 未満(コピーを伴う書き換えは 614 ms) (Clean は Wine の上の Windows 版で測った。Wine の起動時間を差し引いた値) |
2回の map を1回にまとめる測定は要素数 2,000,000、Difference List は要素数 40,000、Codensity は bind を左結合に重ねる回数 n、Traversable と foldr/build は要素数 1,000,000(PureScript の foldr/build のみ 10,000)で測りました。
倍率は、いずれも最適化しない書き方と比べたものです。
実機検証の結果の表では、各言語のコードを、Haskell の記法で代表させて示しています。各言語での実際のコードは、第4章から第8章に示します。
測定環境と測定の条件は、末尾の「実機検証について」の節に記載しました。
測定は複数の時期にわたって行いました。時期が違うと、同じ処理系、同じコードでも値が変わります。Flambda 版の OCaml と Cats の測定は別の時期に行ったため、同じ時期に測った値どうしでのみ比べています。
用語について(簡易的な説明) ※詳細は本稿の本文をご参照ください
Executive Summary では、専門用語に簡単な説明だけを添えます。
詳しい説明は、右の列に示した本文の章でいたします。
| 用語 | 簡単な説明 | 詳しい説明 |
|---|---|---|
| 圏論の法則 | Functor 則や Monad 則のように、圏論で「〇〇則」と呼ばれる等式を、本連載ではまとめて「圏論の法則」と呼びます | 第1章 |
| 書き換え規則 | コンパイラが、プログラムの意味を変えずに、速く動く形へ書き換えるための規則です。GHC では RULES プラグマとして書かれています | 第1章 |
| 正格(strict)と非正格(non-strict) | 正格は、関数の本体を評価する前に引数を評価する性質です。非正格は、引数を必要になるまで評価しない性質です | 第2章 |
| rank-2 type | 関数の引数の型の中に、「任意の型について」を意味する forall を置ける型です。日本語の定訳を確認できなかったため、英語のまま記します |
第3章 |
| higher-kinded type |
List や Maybe のように、型を受け取って型を返すものを、型変数として扱える機能です。日本語の定訳を確認できなかったため、英語のまま記します |
第3章 |
底(bottom)と seq
|
底は、評価しても値を返さない式(例外や無限ループ)です。seq は、1つ目の引数を強制的に評価してから、2つ目の引数を返す関数です |
第4章 |
| 恒等律 | 何もしない関数 id と合成しても、元の関数と変わらない、という圏論の法則です |
第4章 |
| 副作用 | 画面への出力のように、値を返す以外に、プログラムの外へ影響を与えることです | 第6章 |
| Flambda | OCaml のコンパイラに備わった、一連の最適化の処理の名前です。関数のインライン展開(関数の呼び出しを、その関数の中身で置き換えること)などを、標準より積極的に行います。使うには、コンパイラを作る段階で有効にしておく必要があります | 第5章 |
| 融合変換(fusion、deforestation) | 複数の関数や繰り返しを1つにまとめて、途中で作られる中間のデータを取り除くプログラム変換です。関数型言語の研究者が使う定訳です | 第1章 |
本稿では、融合変換という用語を使います。
融合変換(英語では fusion、あるいは deforestation)は、日本の関数型言語の研究者のあいだで確立された訳語です。複数の関数や繰り返しを1つにまとめて、途中で作られる中間のデータを取り除くプログラム変換を指します。
たとえば、map f (map g xs) と記述したコードは、g を適用した中間のリストをいったん作り、そのリストに f を適用します。map (f . g) xs と記述したコードは、g と f を続けて適用するので、中間のリストを作りません。2つのコードは同じ結果を返します。
map f (map g xs) を map (f . g) xs に書き換えることは、融合変換の一例です。本稿では、この書き換えを「2回の map を1回にまとめる」とも表します。
融合変換という用語の成り立ちにも触れておきます。英語の deforestation は、直訳すると「森林伐採」です。この用語は、Philip Wadler が1990年の論文で作ったもので、論文の題名は「Deforestation: transforming programs to eliminate trees」(木を取り除くプログラム変換)です。ここでの「木」は、プログラムの途中で作られるリストや木構造などの中間のデータ構造を指します。英語では、同じ変換を fusion とも呼びます。
本稿で「融合」を単独では用いない理由は、この Executive Summary の後の「本稿の用語と訳語について」に記しました。
融合変換を、コンパイラが自動で行う言語もあれば、プログラマが自らコードを記述して行う必要がある言語もあります。詳しくは第1章でご説明します。
本連載の位置付け
この 連載シリーズ は、関数型言語 と 定理証明言語 について、それぞれの 言語の特徴(圏論構造、型システム、論理体系、言語機能)に照らして、圏論知見から導き出される最適化手法のうち、どの手法が各言語で使えるのか、使う場合はコードの書き方はどう変わるのか、最適化するとどの評価指標がどれくらい改善するのか(実機検証) を考察します。
それぞれの言語で、この記事で取り上げる最適化手法が、使える理由、使えるが条件が付く理由、使えない理由はなにかを、言語と最適化手法の組み合わせごとに考察 します。
連載2回目となる 本稿 では、11個の関数型言語 を取り上げます。
連載3回目となる 次回の記事 では、複数の定理証明言語 を取り上げます。
今回取り上げる 関数型言語では、分類軸軸のうち「論理体系」には、大きな違いは認められませんでした。
次回とりあげる 定理証明言語では、各言語の「論理体系」は大きく異なります。
なお、本連載シリーズの各回の記事は、各言語について、上記の論点について全体を概観します。
個々の言語や、個々の産業領域に特化した単体記事を、この連載記事からの派生記事として書く予定 です。
この連載シリーズ記事は、これら単発記事への入口という位置付け です。
本稿の位置づけ
本稿は、本連載の第2回の記事です。
初回記事は、次の記事です。
初回記事では、Haskellを題材 に、圏論の法則が GHC の中で最適化の書き換え規則として働いている様子を、実機で確かめました。
第2回目となる本稿 では、Haskell 以外の関数型言語 を取り上げます。
初回記事で扱った最適化手法が、それぞれの言語で使えるのか、使うとすれば書き方がどう変わるのか、使えないとすればなぜなのかを、言語の特徴に照らして整理し、実機で確かめます。
初回記事の見取り図では、第2回で扱う言語として次を挙げました。
OCaml・Scala・Clean・Erlang・Clojure・F#・Lisp・Common Lisp・Miranda
本稿では、ここに Standard ML と PureScript を加えます。
Standard ML は、言語仕様が数学的に形式化されている点で、他と性格が異なります。
ほとんどの言語は、仕様が自然言語の文書で書かれています。
それに対して、Standard ML は、型付け規則と意味論を数式で記述した『The Definition of Standard ML』を持ち、言語の振る舞いが数学の対象として定義 されています。
この形式仕様があるため、コンパイラが仕様どおりに動いているかを、数学的に検証することが可能 です。
| 言語 | 仕様の形 |
|---|---|
| Standard ML | 『The Definition of Standard ML (Revised)』が、型付け規則と操作的意味論を数式で記述している |
| Haskell | 『Haskell 2010 Language Report』が、構文の定義と、意味についての非形式的な記述を与えている。報告書自身が「informal abstract semantics(非形式的な抽象意味論)」と述べている |
| OCaml、Scala、F# など | 公式マニュアルによる自然言語の記述 |
なお、Haskell についても、静的意味論や動的意味論を形式化しようとする研究は行われてきましたが、それらは言語仕様そのものではありません。
出典:
S. Marlow (editor), Haskell 2010 Language Report, 2010, Chapter 1 "Introduction"
https://www.haskell.org/onlinereport/haskell2010/haskellch1.html
全文(PDF):https://www.haskell.org/definition/haskell2010.pdf
R. Milner, M. Tofte, R. Harper, D. MacQueen, The Definition of Standard ML (Revised), 2nd edition, MIT Press, 1997
ISBN: 0-262-63181-4
全文(PDF):https://smlfamily.github.io/sml97-defn.pdf
出版社のページ:https://mitpress.mit.edu/9780262631815/the-definition-of-standard-ml/
著者は Robin Milner、Mads Tofte、Robert Harper、David MacQueen の4名で、MIT Press から1997年に出ています。128ページから132ページの小冊子です。
初版は1990年に出ており、改訂版では新しい機能が加わり、使われていない機能が削られ、定義の誤りが修正されています。
構成は、第1部が核の構文、第2部がモジュールの構文、第3部が核の静的意味論、第4部がモジュールの静的意味論、と続きます。型付け規則が、推論規則の形で書かれています。
序文には、言語を厳密に定義するにはプログラミング言語以外の記法が必要であり、厳密さを求めるなら数学の記法が自然な選択である、という趣旨が述べられています。
PureScript は、Haskellとほぼ同じ型システムを持ちながら、評価戦略だけが異なります。
Standard ML と PureScript を加えることで、本連載の4軸が何を分けているのかを、より鮮明に示せると考えました。
| 対にする言語 | そろえた性質 | 動かした軸 | この対で測ったこと |
|---|---|---|---|
| Standard ML と OCaml | どちらも ML 系の言語であり、正格評価で、型クラスを持たない | 言語機能の軸(コンパイラの方針)。OCaml は分割コンパイル、Standard ML の MLton はプログラム全体を一度に見る | モジュールで二重に包んでも、実行時の速さが変わらないこと(第5章 5-4) |
| PureScript と Haskell | 型システムがほぼ同じであり、rank-2 type と higher-kinded type を書け、型クラスを持つ | 評価戦略の軸。Haskell は非正格評価、PureScript は正格評価 | 中間データの作られ方と、底の扱いが変わること(第4章) |
想定読者
- 関数型言語(Haskell、OCaml、Scala、F#、Clojure など、いずれか1つ)を書いたことがある方。初級者でも差し支えございません
- 初回記事を読んだ方、あるいは読んでいなくても、圏論を学び始めたばかりの方
- 自分の使う言語で、初回記事の最適化手法が使えるかを知りたい方
- 言語の設計や処理系の違いに関心のある、上級の実務家や研究者の方
前提とする知識
- いずれかの関数型言語の基本的な文法
前提としない知識
- 圏論。本文で必要な範囲を説明いたします
- 初回記事の内容。本文で必要な範囲を振り返ります
- 正格と非正格の違い、rank-2 type、higher-kinded type、自由定理とパラメトリシティ
- 各言語の処理系の内部の仕組み
本稿の用語と訳語について
本稿では、専門用語の日本語の訳語を、日本の研究者や実務家のあいだで確立された訳語(定訳)があるものに限って用います。定訳を用いる場合は、英語の原語を添えます。
定訳を確認できなかった専門用語は、英語のまま記します。定訳がない用語を、筆者が独自に訳すことはいたしません。
この方針は、初回記事と同じです。初回記事の第4章では、catamorphism、anamorphism、hylomorphism には定着した日本語訳がなく、日本の研究論文でも原語のまま用いられていることを示し、本連載もそれに従うと述べました。
訳語が定訳かどうかは、日本の学会論文や大学の講義資料での用例で確かめました。確かめた用語と典拠の一覧は、末尾の「用語の解説」に載せています。
たとえば、本稿で扱う次の用語は、定訳を確認できなかったため、英語のまま記します。
| 英語のまま記す用語 | 意味(詳しくは本文でご説明します) |
|---|---|
| rank-2 type | 関数の引数の型の中に、「任意の型について」を意味する forall を置ける型 |
| higher-kinded type |
List や Maybe のように、型を受け取って型を返すものを、型変数として扱える機能 |
一方、Clean が持つ uniqueness type は、「一意型」と訳され、日本の実務家のブログ、勉強会の発表資料、技術記事で、2005年ごろから一貫して用いられています。競合する別の訳語は見つかりませんでした。本稿は、「一意型(uniqueness type)」と記します。一意型は、値が共有されていないことを型で表す仕組みです。詳しくは第7章でご説明します。
「一意型」について参照した文章(出典):
- lethevert「Concurrent Clean : 副作用と一意型」、2006年
https://lethevert.hatenadiary.org/entry/20060202/p1 - tanakh「関数プログラミング入門」、2010年
https://www.slideshare.net/tanakh/ss-3580292 - oskimura「Clean」、関数型言語勉強会発表資料、2012年
https://www.slideshare.net/oskimura/clean-8554799 - shigemk2「Cleanの一意型」、2015年
https://www.shigemk2.com/entry/clean_one
学会論文や大学の講義資料での「一意型」の用例は、筆者は確かめられていません。
「融合変換」、fusion、deforestation
本稿で最も多く登場する専門用語の1つが、融合変換 です。
融合変換 は、複数の関数や繰り返しを1つにまとめて、途中で作られる中間のデータを取り除くプログラム変換 を指します。
英語では、同じ変換を fusion とも deforestation とも呼びます。
「融合変換」 は、日本の関数型言語の研究者のあいだで確立された訳語です。
日本ソフトウェア科学会の論文誌や大会論文集、京都大学数理解析研究所の講究録、情報処理学会の研究会の発表で、プログラム変換を指す語として 「融合変換」 が用いられています。
【 「融合変換」 という訳語が定まった訳語かを判断する際に参照した文章(出典)】
- 尾上能之、胡振江、岩崎英哉、武市正人「プログラム融合変換の実用的有効性の検証」、コンピュータソフトウェア、17巻3号、pp. 273–277、2000年、日本ソフトウェア科学会. doi: 10.11309/jssst.17.273
https://doi.org/10.11309/jssst.17.273 - 「書き換え帰納法に基づくプログラム融合変換」、日本ソフトウェア科学会第21回大会(2004年度)論文集
https://www.jstage.jst.go.jp/article/jssstconference/21/0/21_0_21/_pdf/-char/ja - 酒井政裕「非正格関数の融合変換における始代数の存在について」
https://researchmap.jp/msakai/published_papers/115381 - 「変数の出現条件を用いた融合変換とその反復適用について」、京都大学数理解析研究所講究録 1125
https://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/1125-16.pdf - 「boost::proto を用いた融合変換機能付きライブラリの作成」、情報処理学会プログラミング研究会発表資料、2013年2月28日
https://www.univ-orleans.fr/lifo/traclifo/PaPDAS/raw-attachment/wiki/WikiStart/ipsj-pro2013.pdf
これらの典拠は、いずれも関数型言語のプログラム変換の研究です。圏論の研究者のあいだでの「融合変換」の用例は、筆者は確かめていません。
fusion を直訳すると「融合」ですが、本稿では「融合」を単独では用いません。「融合」は日常の言葉でもあり、何と何が融合するのかが伝わりにくいためです。プログラム変換を指す場合は、定訳の「融合変換」を用います。
ただし、Clean のコンパイラの設定項目の名前(Fusion)や、論文の題名に含まれる fusion と deforestation は、固有の名前なので英語のまま記します。
本稿から得られること
- 11の関数型言語を、本連載の4つの分類軸で整理した表(言語の分類表)を得られます
- 初回記事の8つの最適化手法が、ご自身の使う言語で使えるか、条件付きで使えるか、使えないかが分かります(最適化手法を使えるかの表)
- 最適化手法を使えるかの表の「使えない」が何を意味するのかを、書き換えの規則が崩れる実例と、コンパイラが誤りを拒否する実例で確かめられます
- Lisp を除く10の関数型言語と Haskell で測った実測値を、そろえた条件で比べられます(実機検証の結果の表)
- 初回記事で見た恒等律の破れが、Haskell だけの問題ではないことを確かめられます
- ご自身の使う言語では、圏論の知識を誰が使っているのか(コンパイラの作者か、ライブラリの作者か、プログラマ自身か)が分かります
言語別の読み方
本稿は11の関数型言語を扱うため、分量が多くなりました。
ご自身の使う言語についてだけ知りたい方は、次の表の箇所をお読みいただければ十分です。言語の分類表、最適化手法を使えるかの表、実機検証の結果の表は、どの言語の方にも共通してお読みいただきたい表です。
| 言語 | とくにお読みいただきたい箇所 | その言語で注目していただきたい結果 |
|---|---|---|
| OCaml | 最適化手法を使えるかの表の条件の表、OCaml の実機検証、本稿の限界 | コンパイラは map f (map g xs) を map (f . g) xs に自動では書き換えない。プログラマが自らコードを記述して書き換えると 2.03 倍速く、確保したメモリは半分になった。Flambda を有効にしても、map (f . g) xs に書き換えなかった |
| Standard ML | 最適化手法を使えるかの表の「使えない」の理由の表、Standard ML の実機検証 | rank-2 type を書けない。MLton では、モジュールやファンクタで包んでも性能が変わらなかった |
| Scala | 最適化手法を使えるかの表の条件の表、Scala の実機検証、「誰が圏論の知識を使うのか」 |
view を挟むと 17.7 倍速くなった。Cats を使った測定はしていない |
| F# | 最適化手法を使えるかの表の条件の表、F# の実機検証 | higher-kinded type を持たないため、任意のモナドについての Codensity は書けない。Seq を使うと 5.3 倍速くなった |
| PureScript | 本稿の中心となる Haskell との比較、PureScript の実機検証 | Haskell とほぼ同じ型システムで、評価戦略だけが違う。同じ形の式が違う結果になった |
| Clean | 言語の分類表、最適化手法を使えるかの表、Clean の実機検証 | Wine の上で Windows 版を動かして検証した。同じモジュールで定義した map は、Clean のコンパイラの融合変換で 2.0 倍速くなった |
| Miranda | 恒等律の破れの節、Miranda の実機検証 | 初回記事で見た恒等律の破れが、Haskell と同じ形で再現した |
| Clojure | 最適化手法を使えるかの表の「使えない」の意味と、その実機検証、Clojure の実機検証 | transducers で 1.63 倍速くなった。JVM 上の通常の Clojure でも、倍率の傾向は変わらなかった。副作用の順序は入力の型によっても変わる |
| Erlang | Erlang の実機検証(JIT の命令数) | 型が分かる加算では、JIT が生成する命令が14から5に減った |
| Common Lisp | Common Lisp の実機検証 |
loop で約14倍、型の宣言で 10.8 倍速くなった |
| Lisp | 言語の分類表 | 歴史的な言及にとどめた |
本稿(連載第2回)で扱う最適化手法の一覧
本稿では、初回記事で扱った8つの最適化手法を、各言語で確かめます。
| 初回記事の節 | 手法 | 何をするか | 使う数学 |
|---|---|---|---|
| 第3章 | map の書き換え規則 | 2回の map を1回にまとめる(map f (map g xs) を map (f . g) xs に書き換える) |
Functor 則 |
| 第4章 | foldr/build の書き換え規則 | 中間のリストを作らずに畳み込む | 始代数、catamorphism |
| 10-1 | foldMap | 変換と畳み込みを1回の走査にまとめる(fold op 0 (map f xs) を、1回の走査で済む foldMap の形に書き換える) |
Monoid 準同型 |
| 10-2 | Traversable | 失敗しうる処理を2回かける走査を、1回にまとめる(traverse を2回呼び出すコードを、traverse を1回だけ呼び出すコードに書き換える) |
自然性 |
| 10-3 | bind の再結合 | 左に偏った bind の連鎖を組み替える | Monad 則の結合律 |
| 10-4 | Difference List | リストの連結を関数の合成に置き換え、計算量を変える | 自己準同型のモノイド |
| 10-5 | Codensity | bind の連鎖を関数の合成に置き換え、計算量を変える | Kan 拡張 |
| 10-6 | Applicative による全エラー集約 | 複数の検証のエラーを、すべて集める | 積構造 |
それぞれの手法の中身は、初回記事の各節でご説明しました。本稿では、第1章で要点を振り返ります。
第1章 初回記事の振り返りと、本稿の問い
本章では、本稿を読むために必要な範囲で、初回記事の内容を振り返ります。
初回記事をお読みになった方は、1-5 の「本稿の問い」まで読み飛ばしても差し支えございません。
1-1 圏論の法則が、コンパイラの書き換え規則になっている
本連載では、Functor 則や Monad 則のように、圏論で「〇〇則」と呼ばれる等式を、まとめて「圏論の法則」と呼びます。
正確を期すならば、Functor 則や Monad 則は、圏論の用語というよりも、Haskell の型クラスに課される法則として語られることが多いものです。圏論の側では、関手(functor)の公理、モナドの公理と呼ばれます。
たとえば Functor 則の1つは、次の等式です。
map f . map g = map (f . g)
左辺は、リストに g を適用して中間のリストを作り、そのリストに f を適用します。右辺は、g と f を続けて適用する関数を、リストに1回だけ適用します。
2つの式は同じ結果を返します。しかし、右辺は中間のリストを作らないため、速く動きます。
この書き換えのように、複数の関数や繰り返しを1つにまとめて、途中で作られる中間のデータを取り除くプログラム変換を、融合変換と呼びます。英語では fusion、あるいは deforestation と呼ばれます。関数型言語の研究者が使う、日本語の定訳が定まった専門用語です。
出典:
「boost::proto を用いた融合変換機能付きライブラリの作成」、情報処理学会プログラミング研究会発表資料、2013年2月28日
https://www.univ-orleans.fr/lifo/traclifo/PaPDAS/raw-attachment/wiki/WikiStart/ipsj-pro2013.pdf
引用
融合変換は、複数の関数や繰り返しを1つにまとめることにより中間データを除去するプログラム変換である。
deforestation という用語は、Philip Wadler が1990年の論文で作ったものです。直訳すると「森林伐採」で、論文の題名のとおり、プログラムの途中で作られる「木」(リストや木構造などの中間のデータ構造)を取り除く変換を指します。英語では、同じ変換を fusion とも呼びます。
出典:
P. Wadler, "Deforestation: transforming programs to eliminate trees", Theoretical Computer Science, 73(2), pp. 231–248, 1990. doi: 10.1016/0304-3975(90)90147-A
https://doi.org/10.1016/0304-3975(90)90147-A
出典:
Wikipedia「Deforestation (computer science)」
https://en.wikipedia.org/wiki/Deforestation_(computer_science)
引用
deforestation (also known as fusion) is a program transformation to eliminate intermediate lists or tree structures
筆者による日本語訳:
deforestation(fusion とも呼ばれる)は、中間のリストや木構造を取り除くプログラム変換である。
fusion を直訳すると「融合」ですが、本稿では、プログラム変換を指す専門用語として「融合変換」を用い、「融合」を単独では用いません。「融合」は日常の言葉でもあり、何と何が融合するのかが伝わりにくいためです。Clean のコンパイラの設定項目の名前(Fusion)や、論文の題名に含まれる fusion は、固有の名前なので英語のまま記します。
本稿では、map f (map g xs) を map (f . g) xs に書き換えることを、「2回の map を1回にまとめる」とも表します。
Haskell のコンパイラ GHC は、この等式を、プログラムを右辺の形へ書き換える規則として使っています。規則は、GHC の標準ライブラリの中に、RULES プラグマという記法で書かれています。
出典:
GHC 9.4.7、libraries/base/GHC/Base.hs、1357〜1362行目
https://github.com/ghc/ghc
{-# RULES
"map" [~1] forall f xs. map f xs = build (\c n -> foldr (mapFB c f) n xs)
"mapList" [1] forall f. foldr (mapFB (:) f) [] = map f
"mapFB" forall c f g. mapFB (mapFB c f) g = mapFB c (f.g)
"mapFB/id" forall c. mapFB c (\x -> x) = c
#-}
タロウくん:
先生、RULES プラグマに書かれている規則は、コンパイラが勝手に使うのですか?
専任講師:
そうです。
プログラマが map f (map g xs) と書いても、GHC は、規則に従って map (f . g) xs にあたる形へ書き換えます。
3番目の mapFB の規則が、2回の map を1回にまとめる役目を担っています。
タロウくん:
書き換えても結果が変わらないこと は、誰が保証しているのでしょうか?
専任講師:
圏論の法則
です。
Functor則が成り立つので、左辺と右辺は同じ結果を返します。
GHCの作者は、その法則を知っていたから、この規則を書けたのです。
本稿では、この書き換えを「map の書き換え規則」と呼びます。
1-2 圏論が出すのは「書き換えてよい」という許可である
初回記事の第4章では、もう1つの書き換え規則を扱いました。foldr/build の書き換え規則です。
foldr c n (build g) = g c n
build g は、g にリストの構築子((:) と [])を渡してリストを作る関数です。foldr c n は、そのリストを c と n で畳み込みます。
規則の右辺は、リストを作らずに、g に c と n を直接渡します。中間のリストが消えます。
出典:
A. Gill, J. Launchbury, S. L. Peyton Jones, "A Short Cut to Deforestation", FPCA 1993, pp. 223–232. doi: 10.1145/165180.165214
https://doi.org/10.1145/165180.165214
タロウくん:
この規則は、どんな g についても成り立つのですか?
専任講師:
よい質問です。
成り立つのは、g の型が次の形のときだけです。
build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
内側の forall b. によって、g は、「どんな型 b についても使える」関数でなければなりません。
そういう関数は、b の中身を調べることができません。
渡された c と n を組み合わせることしかできないのです。
タロウくん:
中身を調べられないから、リストを作ってから畳み込んでも、直接 c と n を渡しても、同じ結果になる、ということですか?
専任講師:
そのとおりです。
関数の型だけから、その関数が満たす等式を導けることを、自由定理(free theorem)と呼びます。
その土台にある性質を、パラメトリシティ(parametricity)と呼びます。
初回記事で詳しく説明しました。
出典:
P. Wadler, "Theorems for free!", FPCA 1989, pp. 347–359. doi: 10.1145/99370.99404
https://doi.org/10.1145/99370.99404
初回記事で強調したのは、圏論の法則や自由定理が出すのは「この書き換えをしてよい」という許可である、という点です。
書き換えた方が速いかどうかは、処理系の実装で決まります。許可を出すのが数学で、速さを決めるのが処理系です。
1-3 Hask は、厳密には圏ではない
Haskell の型を対象、関数を射とみなしたものを、Hask 圏と呼びます。
しかし、Hask は厳密には圏ではありません。初回記事の第7章で、そのことを実機で確かめました。
原因は、底(bottom)と seq です。
底は、評価しても値を返さない式です。例外を投げる undefined や、無限ループがこれにあたります。
タロウくん:
先生、底という言葉は初回記事にも出てきましたね。値が返ってこない式を指す、ということでしたね。
専任講師:
はい。そのとおりです。
計算が終わらないか、例外で止まるか、どちらにしても、値が得られません。その「値がない」という状態を、1つの式として扱うための言葉です。
タロウくん:
値がないのに、式として扱うのですね。
専任講師:
そこが要点です。底を式として扱うからこそ、「この関数は底を受け取ったらどうなるか」を論じられます。
本章と第4章で、この問いが中心になります。
seq は、1つ目の引数を強制的に評価してから、2つ目の引数を返す関数です。Haskell は、引数を必要になるまで評価しない言語です。seq は、その評価を強制するために用意されています。
出典:
A. Bauer, "Hask is not a category", 2016年
https://math.andrej.com/2016/08/06/hask-is-not-a-category/
引用
It is then immediately noticed that there is a problem because the supposed identity morphisms do not actually work correctly:
seq undefined () = undefinedandseq (undefined . id) () = (), therefore we do not haveundefined . id = undefined.
筆者による日本語訳:
ここで直ちに問題が見つかる。恒等射であるはずのものが、実際には正しく働かないのである。seq undefined () = undefined であるのに対し seq (undefined . id) () = () であるから、undefined . id = undefined が成り立たない。
恒等律によれば、undefined . id と undefined は等しいはずです。しかし seq は、この2つを区別します。
それでも GHC が圏論の法則を使って最適化できるのは、「底を含まない範囲で考える」という約束のうえに立っているから です。
この約束が一定の条件のもとで正当化されることは、POPL 2006 の論文で示されています。
出典:
N. A. Danielsson, J. Hughes, P. Jansson, J. Gibbons, "Fast and Loose Reasoning is Morally Correct", POPL 2006, pp. 206–217. doi: 10.1145/1111037.1111056
https://doi.org/10.1145/1111037.1111056
本稿の第4章では、同じ現象を、Haskell 以外の言語で確かめます。
1-4 コンパイラが行う最適化と、プログラマが行う最適化
初回記事では、8つの最適化手法を扱いました。
| 初回記事の節 | 手法 | 使う数学 | 誰が行うか |
|---|---|---|---|
| 第3章 | map の書き換え規則 | Functor 則 | GHC が自動で行う |
| 第4章 | foldr/build の書き換え規則 | 始代数、catamorphism | GHC が自動で行う |
| 10-1 | foldMap | Monoid 準同型 | GHC が自動で行う |
| 10-2 | Traversable。2回の走査を1回にまとめる | 自然性 | プログラマが行う |
| 10-3 | bind の再結合 | Monad 則の結合律 | プログラマが行う |
| 10-4 | Difference List | 自己準同型のモノイド | プログラマが行う |
| 10-5 | Codensity | Kan 拡張 | プログラマが行う |
| 10-6 | Applicative による全エラー集約 | 積構造 | プログラマが行う |
GHC が自動で行う最適化は、圏論を知らないプログラマでも恩恵を受けられます。
一方、プログラマが行う最適化は、圏論の知識がなければ、そもそも思いつくことができません。
とくに Difference List と Codensity は、定数倍の改善ではありません。計算量そのものが変わります。初回記事では、Codensity で約3,300倍の高速化を実測しました。
出典:
J. Voigtländer, "Asymptotic Improvement of Computations over Free Monads", MPC 2008, LNCS 5133, pp. 388–403. doi: 10.1007/978-3-540-70594-9_20
https://doi.org/10.1007/978-3-540-70594-9_20
1-5 本稿の問い
本稿は、次の2つの問いに答えます。
1つ目の問いは、Haskell 以外の関数型言語を、本連載の4つの分類軸(型理論、評価戦略、論理体系、言語機能)で見たとき、各言語をどのようにグループ分けできるか、というものです。第2章で答えます。
2つ目の問いは、各グループの言語で、初回記事の8つの手法のうち、どれが使え、どれが条件付きで使え、どれが使えないのか、というものです。条件が付く理由と使えない理由を、初回記事のロジックと整合させて説明します。第3章から第8章で答えます。
手法を使えるための条件は、4つの軸のすべてに○が付くことです。
本稿は、Haskell から出発して、軸を1つずつ動かしながら、何がどの軸に依存しているのかを確かめます。
| 何を変えるか | 比較する言語 | 章 |
|---|---|---|
| 評価戦略だけを変える | Haskell と PureScript、Miranda | 第4章 |
| 言語機能を変える | OCaml、Standard ML、Scala、F# | 第5章 |
| 型付けを変える | Clojure、Erlang、Common Lisp | 第6章 |
| 非正格のまま、別の言語機能を見る | Clean | 第7章 |
第2章 本連載が採用する分類軸
本章では、本連載が各言語を整理するために使う4つの軸を説明し、11の関数型言語を言語の分類表にまとめます。
本稿の4つの軸と、それぞれが何を決めるのかを、図に示します。
2-1 4つの分類軸と、その位置づけ
本連載が採用する分類軸について
本連載は、関数型言語と定理証明言語を、次の4つの軸で整理します。
| 軸 | 何を見るか |
|---|---|
| 型理論 | 静的型付けか動的型付けか。静的なら、多相型か依存型か |
| 評価戦略 | 正格か非正格か |
| 論理体系 | 古典論理か直観主義論理か |
| 言語機能 | 型パラメータ、型クラスまたはモジュール、higher-kinded type ほか |
higher-kinded type は、日本語の定訳を確認できなかったため、英語のまま記します。
タロウくん:
先生、表を読む前に、言葉の意味を確認しておきたいのですが。
静的型付けはコンパイルのときに型を検査するもの、動的型付け は実行時に検査するもの。この区別で合っていますか?
専任講師:
はい、そのとおりです。
静的型付けの言語では、型が合わないコードはコンパイルが通りません。
動的型付けの言語では、実行してみて初めて分かります。
本稿で扱う11の関数型言語のうち、Clojure、Erlang、Common Lisp の3つが動的型付けです。
タロウくん:
それから多相型。
これは、どの型にも使える関数を書ける仕組みのことだと記憶しています。
専任講師:
はい。リストの長さを数える関数は、中身が整数でも文字列でも同じように働きます。
この「どの型でも同じ」を型で表す仕組みが、多相型 です。
タロウくん:
すると依存型は、何が違うのですか?
専任講師:
依存型は、値に依存する型 です。
たとえば「長さ3のリスト」という型を書けます。3という値が、型の中に現れています。多相型では、こうは書けません。
タロウくん:
型の中に、数字が入るのですか。
専任講師:
そうです。
「長さの違うリストどうしを連結してはいけない」といった規則を、型で表せます。
依存型を持つのは、第3回で扱う定理証明言語です。本稿の11の関数型言語には、依存型を持つものはありません。
この4つの軸は、いずれも研究者のあいだで標準的に使われているものです。
独自なのは、この4つを同時に並べて、1つの表にまとめる点です。
4つをこの形で組み合わせた分類は、筆者が調べたかぎり、既存の文献に見当たりませんでした。
なぜこの組み合わせにしたのか、そしてこの組み合わせにどのような限界があるのかを、以下に述べます。
個々の軸は、いずれも標準的なものです
まず、4つの軸のそれぞれが、教科書や論文で使われている標準的な区別であることを確かめます。
「多相型か依存型か」という区別は、ヘンク・バレンドレヒト(Henk Barendregt)が示したラムダ・キューブ(lambda cube、λ-cube)に対応します。
ラムダ・キューブは、型付きラムダ計算の体系を、3つの方向への拡張の組み合わせとして、8個の体系からなる立方体に整理したものです。バレンドレヒトが1991年の論文で示しました。
出典:
H. P. Barendregt, "Introduction to generalized type systems", Journal of Functional Programming, 1(2), pp. 125–154, 1991
doi: 10.1017/S0956796800020025
https://doi.org/10.1017/S0956796800020025
出典:
H. P. Barendregt, "Lambda calculi with types", in S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (eds.), Handbook of Logic in Computer Science, Volume 2, Oxford University Press, pp. 117–309, 1992
Benjamin C. Pierce の教科書『Types and Programming Languages』では、型システムが次の順に位置づけられています。
| 体系 | 何を抽象化できるか |
|---|---|
| 単純型付きラムダ計算 | 項において項を抽象化する |
| System F | 項において型を抽象化する(多相型) |
| System Fω | 型において型を抽象化する(型演算子、higher-kinded type) |
| 依存型 | 型において項を抽象化する |
出典:
B. C. Pierce, Types and Programming Languages, MIT Press, 2002
https://www.cis.upenn.edu/~bcpierce/tapl/
「正格か非正格か」という区別も、評価戦略の標準的な分類です。
Pierce の同じ教科書が、call-by-value と call-by-name の区別として扱っています。
タロウくん:
先生、ここも確認させてください。
正格評価は、関数を呼ぶ前に引数を計算してしまう、非正格評価は、必要になるまで計算しない、ということでしたよね。
専任講師:
そのとおりです。よく覚えていました。
f (1 + 2) と書いたとき、正格評価の言語は、まず 1 + 2 を計算して3にしてから f に渡します。非正格評価の言語は、3 を計算せずに f に渡し、f の中で実際に必要になったときに初めて計算します。
タロウくん:
遅延評価 という言葉も出てきますが、非正格評価と同じものですか?
専任講師:
厳密には違います。
非正格評価は「必要になるまで計算しない」という 性質 の名前です。
遅延評価は、その性質を実現する方式の1つです。一度計算した結果を覚えておき、二度目からは使い回します。
タロウくん:
覚えておく、というところが違うのですね。
専任講師:
はい。本稿で扱う Haskell、Miranda、Clean は、いずれも遅延評価です。
この区別が、第4章の結論に直結します。
正格評価では、中間のリストが全要素いっぺんにメモリに作られます。遅延評価では、1つずつ作られて、すぐ消費されます。
「古典論理か直観主義論理か」も、Curry-Howard 対応(Curry-Howard correspondence)を論じる文脈で、繰り返し用いられてきた区別です。この対応を体系的に扱った文献として、次が挙げられます。
出典:
M. H. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, Volume 149, Elsevier, 2006
https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/149
「型クラスか、モジュールか」という区別も、両者を比較した研究があります。
第5章で、この論文を引用します。
出典:
S. Wehr, M. M. T. Chakravarty, "ML Modules and Haskell Type Classes: A Constructive Comparison", APLAS 2008, LNCS 5356, Springer, pp. 188–204
doi: 10.1007/978-3-540-89330-1_14
https://link.springer.com/chapter/10.1007/978-3-540-89330-1_14
タロウくん:
先生、型クラスというのは、同じ名前の関数を、型ごとに違う中身で用意しておく仕組みだと習いました。
そう捉えて差し支えありませんか?
専任講師:
はい、それで結構です。
Haskell の show は、整数に使えば整数を文字にし、リストに使えばリストを文字にします。名前は1つですが、型ごとに中身が違います。この仕組みが型クラスです。
タロウくん:
それなら、rank-2 type は何でしょうか?
この言葉は、初回記事にも出てきましたが、いまひとつ掴めていません。
専任講師:
forall を、どこに置けるかの違いです。
forall a. a -> a と書くと、「どの型 a についても」が式の外側にあります。これが rank-1 です。
(forall a. a -> a) -> Int と書くと、forall が関数の引数の型の中に入っています。
これが rank-2 です。
タロウくん:
位置が変わると、何が変わるのですか?
専任講師:
呼び出す側と呼ばれる側の、どちらが型を決めるか が変わります。
rank-1 では、呼び出す側が 型を決めます。
それに対して、rank-2 では、受け取った関数を関数の中で好きな型に使えます。
初回記事の foldr/build の書き換えは、この性質に依存していました。第3章と第8章で、もう一度扱います。
タロウくん:
higher-kinded type も、同じような話でしょうか。
専任講師:
似ていますが、別のものです。
List や Maybe は、それ自体では型ではありません。List Int のように、型を受け取って初めて型になります。
この「型を受け取って型を返すもの」を、型変数として扱える機能が higher-kinded type です。
タロウくん:
「どの List でも Maybe でも使える関数」を書ける、ということですか。
専任講師:
そのとおりです。よい言い換えです。
Traversable のような、どの入れ物にも使える仕組みは、これがないと書けません。F# にはこれがないので、第8章で特定の型に固定して測ることになります。
では、なぜ4つを組み合わせるのか
個々の軸は標準的でも、既存の分類は、それぞれ別々の目的で作られています。ラムダ・キューブは型システムを整理するため、評価戦略の分類は計算の順序を整理するためのものです。
本連載が答えたいのは、それらとは別の問いです。
圏論の知見から導かれた最適化手法のうち、どれがこの言語で使えるのか。
この問いに答えるには、4つすべてに○が付く必要があります。
初回記事で扱った foldr/build の書き換え規則を例にします。
| 軸 | Haskellの場合 | 何が決まるか |
|---|---|---|
| 型理論 | 静的型付け。多相型を持つ | パラメトリシティが成り立つ |
| 評価戦略 | 非正格。底と seq がある |
保証が崩れる場合がある |
| 論理体系 | ── | Haskellでは問題にならない |
| 言語機能 |
forall b. と書ける |
規則を実際に記述できる |
1つでも欠ければ、その手法は使えません。
既存の分類は、いずれか1つの軸を深く掘り下げるもので、この4つを同時に見る形になっていません。
そこで本連載は、標準的な4つの軸を、この問いに答えるための1つの表にまとめました。
この組み合わせの限界
ただし、4つをこの形で並べることには、3つの限界があります。
1つ目。4つの軸は、互いに独立ではありません。
論理体系と型理論は、Curry-Howard対応を通じてつながっています。
独立した座標軸のように扱うのは、便宜上の整理です。
2つ目。「言語機能」だけが、理論ではなく実装の話です。
他の3つと並べるのは、厳密には層が違います。
しかし、その手法を実際に書けるかどうかは、言語機能で決まります。
実務の観点から、あえて並べました。
3つ目。この4軸で、すべての最適化手法を説明できるわけではありません。
初回記事の 10-3 では、bind の再結合という手法を扱いました。
あの手法に必要だったのは、処理系がどう評価するかという実装の知識です。
4軸のどれにも、うまく収まりません。
そうした手法が出てきた場合は、4軸では説明できないことを、その都度書き添えます。
🔬 上級者向けコラム:「二階」と rank-2 は別のものである
System F は、「多相ラムダ計算(polymorphic λ-calculus)」とも「二階ラムダ計算(second-order lambda calculus)」とも呼ばれます。ここでの「二階」は、second-order の訳です。
一方、本稿の第3章で扱う rank-2 type の rank は、forall が型の中でどれだけ深い位置に置かれるかを表す尺度です。forall が型の一番外側にしかない型を rank-1、関数の引数の型の中に forall を置ける型を rank-2 と呼びます。
2つは別の概念です。rank-2 type を「二階の多相型」と訳すと、System F の「二階」と混同されます。本稿が rank-2 type を英語のまま記すのは、日本語の定訳を確認できなかったことに加え、この混同を避けるためでもあります。
出典:
五十嵐淳「工学部専門科目『計算と論理』配布資料 多相ラムダ計算(System F)」京都大学
https://io.kuis.kyoto-u.ac.jp/~igarashi/class/cal/systemF.pdf
2-2 評価戦略:正格と非正格
4つの軸のうち、本稿で最も大きな役割を果たすのが評価戦略です。
タロウくん:
先生、正格と非正格の違いを、あらためて教えていただけますか。
専任講師:
関数を呼ぶときに、引数をいつ評価するか、の違いです。
正格な言語は、関数の本体を評価する前に、引数をすべて評価します。
非正格な言語は、引数が本当に必要になるまで評価しません。
タロウくん:
それで、何が変わるのでしょうか。
専任講師:
たとえば、使わない引数に、評価すると例外を投げる式を渡したとします。
正格な言語では、関数の本体に入る前にその引数を評価するので、例外が起きます。
非正格な言語では、その引数を使わないかぎり評価しないので、例外は起きません。
タロウくん:
Haskell は非正格でしたね。
専任講師:
そうです。
そして、非正格であるからこそ、評価を強制する seq が用意されていて、第1章で見た恒等律の破れが生じます。
第4章で、この違いを実機で確かめます。
非正格な評価を実現する方式の1つが、遅延評価(lazy evaluation)です。
出典:
五十嵐淳「SICP 第4章(その3)」京都大学、2012年
https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/pl12s/chap4-3.pdf
2-3 言語の分類表:11の関数型言語を4軸で整理する
言語名の前の記号は、グループを示します。A は静的型付けで非正格評価の言語、B は静的型付けで正格評価の言語、C は動的型付けの言語です。
Haskell は、初回記事で扱った言語です。比較のために載せています。
4つの分類軸による言語の分類表
| 言語 | 型理論 | 評価戦略 | 論理体系 | 言語機能 |
|---|---|---|---|---|
| 【A】Haskell(参考) | 静的型付け。多相型(rank-N polymorphism、higher-kinded type) | 非正格 | 特に制約はない | 型クラス、RULES プラグマ(書き換え規則)、seq
|
| 【A】Clean | 静的型付け。多相型(rank-2 までの型、type constructor class)、一意型 | 非正格(! による正格性の注釈が可能) |
特に制約はない | 型クラス、一意型、コンパイラによる融合変換 |
| 【A】Miranda | 静的型付け。多相型(Hindley-Milner 型。rank-1 のみ) | 非正格 | 特に制約はない | 型クラスなし、seq
|
| 【B】PureScript | 静的型付け。多相型(rank-N polymorphism、higher-kinded type)、row polymorphism | 正格 | 特に制約はない | 型クラス、Partial 型クラス、Effect 型 |
| 【B】OCaml | 静的型付け。多相型(rank-1。polymorphic record field で rank-2 type を表す) | 正格(評価順序は仕様上未規定。lazy による遅延評価が可能) |
特に制約はない | モジュールとファンクタ、Flambda、代数的エフェクト(OCaml 5) |
| 【B】Standard ML | 静的型付け。多相型(rank-1 のみ) | 正格 | 特に制約はない | モジュールとファンクタ、形式仕様、MLton の whole-program optimization |
| 【B】Scala | 静的型付け。多相型(higher-kinded type。polymorphic method で rank-2 type を表す) | 正格(by-name parameter と view による遅延評価が可能) |
特に制約はない | implicit による型クラス(Cats)、view
|
| 【B】F# | 静的型付け。多相型(higher-kinded type なし。generic method で rank-2 type を表す) | 正格(Seq と lazy 式による遅延評価が可能) |
特に制約はない |
inline 関数、Seq、型クラスなし |
| 【C】Clojure | 動的型付け | 正格(lazy sequence による遅延評価が可能) | 特に制約はない | transducers、マクロ |
| 【C】Erlang | 動的型付け | 正格(部分式を先に評価することが仕様で定められている) | 特に制約はない | パターンマッチとガード、型情報にもとづく JIT(OTP 25) |
| 【C】Common Lisp | 動的型付け | 正格(引数を左から右へ評価してから関数を呼ぶことが仕様で定められている) | 特に制約はない | マクロ、コンパイラマクロ、型宣言 |
| 【C】Lisp | 動的型付け | 方言によって異なる(Racket には遅延評価を既定とする Lazy Racket がある) | 特に制約はない | Common Lisp、Scheme、Racket、Clojure などを方言とする言語族。歴史的な言及にとどめる |
論理体系の列は、すべての言語で「特に制約はない」となりました。
本稿で扱う言語は、いずれも定理証明を目的とした言語ではないためです。
論理体系の軸が効いてくるのは、第3回で扱う定理証明言語です。
初回記事の Applicative の節でも、Haskell、OCaml、Scala の論理体系の列は「特に制約はない」としていました。
2-4 言語の分類表の記述の典拠
言語の分類表の評価戦略と、純粋かどうかについての記述は、次の文献で確かめました。
| 言語 | 確かめた内容 | 典拠 |
|---|---|---|
| 11の関数型言語のうち10言語 | 純粋(Pure)かどうか、遅延評価の機能を持つかどうか | Wikipedia「Comparison of functional programming languages」 https://en.wikipedia.org/wiki/Comparison_of_functional_programming_languages |
| PureScript | 正格評価であること。値が既定では副作用を持たず、副作用は Effect 型で表すこと |
PureScript 公式ドキュメント「Differences from Haskell」、purescript-effect(Pursuit) https://pursuit.purescript.org/packages/purescript-effect |
| Clojure | 遅延評価の言語ではないが、lazy sequence を持つこと | Clojure Guides「Language: Laziness」 https://clojure-doc.org/articles/language/laziness |
| Common Lisp | 関数の引数を左から右へ評価してから関数を呼ぶこと | Common Lisp HyperSpec, Section 3.1.2.1.2.3 https://www.lispworks.com/documentation/HyperSpec/Body/03_ababc.htm |
| Erlang | すべての部分式を、式そのものより先に評価すること | Erlang Reference Manual, "Expressions" https://erlang.org/documentation/doc-10.3/doc/reference_manual/expressions.html |
| F# |
Seq の要素が必要になったときにだけ計算されること。遅延式が直ちには評価されないこと |
Microsoft Learn「Sequences」「Lazy Expressions」 https://learn.microsoft.com/en-us/dotnet/fsharp/language-reference/sequences |
| Scala | by-name parameter が、使われるたびに評価され、使われなければ評価されないこと | Scala 公式ドキュメント「By-name Parameters」 https://docs.scala-lang.org/tour/by-name-parameters.html |
| Lisp | Common Lisp、Scheme、Racket、Clojure などを方言とする言語族であること | Wikipedia「Lisp (programming language)」 https://en.wikipedia.org/wiki/Lisp_(programming_language) |
第3章 初回記事の8手法は、各言語で使えるか
本章では、初回記事の8つの手法が各言語で使えるかどうかを、最適化手法を使えるかの表にまとめます。
その前に、最適化手法を使えるかの表の判定を左右する2つの型の機能を説明します。
3-1 2つの型の機能:rank-2 type と higher-kinded type
タロウくん:
先生、Executive Summary に rank-2 type と higher-kinded type という言葉が出てきました。どういうものでしょうか。
専任講師:
第1章で見た build の型を、もう一度見てください。
build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
引数の型の中に forall b. があります。
このように、関数の引数の型の中に「どんな型についても」を置ける型を、rank-2 type と呼びます。
foldr/build の規則が正しいことは、この forall b. に支えられていました。
タロウくん:
では、forall を内側に置けない言語では、build を書けないのですか。
専任講師:
build という関数を書くことはできます。
しかし、引数の g が「どんな型についても使える」ことを、型で強制できません。
そうなると、規則が正しいことを、型が保証してくれなくなります。
タロウくん:
higher-kinded type のほうは、どういうものでしょうか。
専任講師:
List や Maybe は、それだけでは型ではありません。
List Int や Maybe String のように、型を1つ受け取って、初めて型になります。
この「型を受け取って型を返すもの」を、型変数として扱える機能を、higher-kinded type と呼びます。
タロウくん:
どんな場面で必要になるのでしょうか。
専任講師:
Traversable や Codensity は、「任意の Applicative について」「任意のモナドについて」書く手法です。
Applicative やモナドの型は、Maybe や List のような「型を受け取って型を返すもの」です。
それを型変数として扱えないと、汎用の形で書けません。
タロウくん:
Codensity は、どちらも必要なのですか。
専任講師:
そうです。
Codensity の型は forall b. (a -> m b) -> m b という形をしています。
forall b. が rank-2 type に、m が higher-kinded type にあたります。
rank-2 type と higher-kinded type は、いずれも日本語の定訳を確認できなかったため、英語のまま記します。「高カインド型」「高階型」といった表記も見られますが、定訳として確かめられませんでした。
3-2 各言語で、rank-2 type と higher-kinded type を書けるか
筆者は、各言語で build(rank-2 type を要する)と Codensity(rank-2 type と higher-kinded type を要する)を実際に書き、コンパイルして確かめました。
| 言語 | rank-2 type | higher-kinded type | 確かめた方法 |
|---|---|---|---|
| PureScript | 直接書ける | 書ける |
build と Codensity のコンパイルに成功した |
| OCaml | polymorphic record field で表せる | ファンクタで表せる |
build と Codensity のコンパイルに成功した |
| Scala | polymorphic method を持つ trait で表せる | 書ける |
build と Codensity のコンパイルに成功した |
| F# | generic method を持つインターフェースで表せる | 書けない |
build はコンパイルに成功した。任意のモナドについての Codensity では、コンパイラが FS0712(Type parameter cannot be used as type constructor)を出した |
| Standard ML | 書けない | ファンクタで表せる | 引数の関数を2つの異なる型で使う関数が、型エラーになった |
| Miranda | 書けない | 書けない | 引数の関数を2つの異なる型で使う関数が、型エラーになった |
| Clean |
A. による全称量化で書ける(rank-2 まで) |
type constructor class で書ける | Wine の上の Clean 3.1 で、build と Codensity のコンパイルと実行に成功した |
ここで、polymorphic record field、polymorphic method、generic method は、それぞれ OCaml、Scala、F# で、型パラメータを持つレコードのフィールド、メソッドのことです。いずれも日本語の定訳を確認できなかったため、英語のまま記します。
OCaml と Standard ML の「ファンクタ」は、モジュールを受け取ってモジュールを返す、モジュール上の関数です。圏論の関手(functor)とは別物です。本稿では、両者を「ファンクタ」と「関手」で書き分けます。
出典:
MLton, "First-Class Polymorphism"
https://mlton.sourceforge.io/FirstClassPolymorphism
引用
Although Standard ML does have polymorphic functions, it does not support first-class polymorphism.
筆者による日本語訳:
Standard ML は多相関数を持つが、第一級の多相性は持たない。
出典:
University of Cambridge, L28: Advanced Functional Programming, Chapter 7 "Parametricity"
https://www.cl.cam.ac.uk/teaching/1617/L28/parametricity.pdf
引用
universal types in OCaml are provided through record types
筆者による日本語訳:
OCaml では、全称型はレコード型を通じて提供される。
「rank-2 type、higher-kinded type、ファンクタ」について参照した文章(出典):
- PureScript 公式ドキュメント "Types"(Rank N Types の節)
https://github.com/purescript/documentation/blob/master/language/Types.md - Clean Language Report Version 2.2
https://ftp.cs.ru.nl/Clean/html_report/CleanRep.2.2_1.htm - OCaml 公式チュートリアル「Functors」
https://github.com/ocaml/ocaml.org/blob/02b11348501cef1699c405c6c97fa61e5c529d2c/data/tutorials/language/1ms_01_functors.md
3-3 最適化手法を使えるかの表:初回記事の8手法を、各言語で使えるか
初回記事の8つの最適化手法を、各言語で使えるかの表
| 最適化手法 | 使える | 条件付きで使える | 使えない |
|---|---|---|---|
第3章 map の書き換え規則(Functor 則。2回の map を1回にまとめる。map f (map g xs) を map (f . g) xs に書き換える) |
Haskell(参考)、Clean、Miranda、PureScript | OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | ── |
| 第4章 foldr/build の書き換え規則(始代数。中間リストを作らない。rank-2 type を要する) | Haskell(参考)、Clean、PureScript | OCaml、Scala、F# | Miranda、Standard ML、Clojure、Erlang、Common Lisp |
| 10-1 foldMap(Monoid 準同型) | Haskell(参考)、Clean、Miranda、PureScript | OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | ── |
10-2 Traversable(自然性。2回の走査を1回にまとめる。traverse を2回呼び出すコードを、traverse を1回だけ呼び出すコードに書き換える。higher-kinded type を要する) |
Haskell(参考)、Clean、PureScript | OCaml、Standard ML、Scala | Miranda、F#、Clojure、Erlang、Common Lisp |
| 10-3 bind の再結合(Monad 則の結合律) | Haskell(参考)、Clean、Miranda、PureScript、OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | ── | ── |
| 10-4 Difference List(自己準同型のモノイド。計算量が変わる) | Haskell(参考)、Clean、Miranda、PureScript、OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | ── | ── |
| 10-5 Codensity(Kan 拡張。higher-kinded type と rank-2 type を要する) | Haskell(参考)、Clean、PureScript | OCaml、Scala、F# | Miranda、Standard ML、Clojure、Erlang、Common Lisp |
| 10-6 Applicative による全エラー集約(積構造) | Haskell(参考)、Clean、PureScript、OCaml、Standard ML、Scala | Miranda、F#、Clojure、Erlang、Common Lisp | ── |
Lisp は歴史的な言及にとどめるため、最適化手法を使えるかの表には含めていません。
10-3 の bind の再結合は、どの言語でも、そのモナドが結合律を満たすことをプログラマが保証する必要があります。結合律は、Haskell を含めどの言語の型検査でも確かめられません。
この条件はすべての言語に共通するため、最適化手法を使えるかの表では「使える」に含めました。
なお、bind を左結合から右結合に組み替えても、関数を呼ぶ順序は変わりません。筆者は、OCaml、Clojure、Erlang、Common Lisp で、このことを実機で確かめました。
3-4 3つの列の基準と、条件の内訳
最適化手法を使えるかの表の3つの列は、次の基準で分けました。
| 列 | 基準 |
|---|---|
| 使える | その手法の正しさを支える条件が、言語の性質によって満たされる。標準の言語機能で書ける。書き方が Haskell と異なる場合を含む |
| 条件付きで使える | 書けるが、言語が保証しない条件を、プログラマが自分で満たす必要がある |
| 使えない | その手法の正しさを支える型の保証を、言語の中で表現できない |
「条件付きで使える」の条件は、手法と言語によって異なります。
| 手法 | 言語 | 条件 |
|---|---|---|
| 第3章、10-1 | OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | 書き換えの前後で、関数を適用する順序が変わる。これらの言語は副作用を禁じていないため、関数に副作用がないことをプログラマが保証する必要がある |
| 第3章 | OCaml | 上記に加え、OCaml は評価順序を仕様で定めていない |
| 第3章 | Clojure | transducers を使えば、中間コレクションを作らずに同じ目的を達成できる |
| 第4章、10-5 | OCaml | rank-2 type を、polymorphic record field で表す。Codensity は、さらにファンクタで表す。加えて、副作用がないこと |
| 第4章、10-5 | Scala | rank-2 type を、polymorphic method を持つ trait で表す。加えて、副作用がないこと |
| 第4章 | F# | rank-2 type を、generic method を持つインターフェースで表す。加えて、副作用がないこと |
| 10-5 | F# | F# は higher-kinded type を持たない。任意のモナドについての Codensity は書けず、特定のモナドに固定すれば書ける |
| 10-2 | OCaml、Standard ML | Traversable をファンクタで表す。加えて、副作用がないこと |
| 10-2 | Scala | Cats の Traverse を使う。加えて、副作用がないこと |
| 10-6 | Miranda、F# | 型クラスまたは higher-kinded type がないため、特定の型に固定して書く |
| 10-6 | Clojure、Erlang、Common Lisp | 型の保証がないまま、エラーを集める関数を自分で書く |
「使えない」の理由は、次の2つに分かれます。
| 手法 | 言語 | 使えない理由 |
|---|---|---|
| 第4章、10-5 | Miranda、Standard ML | rank-2 type を書けない。forall b. にあたる型を関数の引数に置けない |
| 10-2 | Miranda | 型クラスも higher-kinded type もなく、Traversable を表現できない |
| 10-2 | F# | higher-kinded type を持たず、Traversable を表現できない |
| 第4章、10-2、10-5 | Clojure、Erlang、Common Lisp | 静的な型を持たない。手法の正しさを支える型の保証(自由定理、自然性、rank-2 type)が得られない |
3-5 「使えない」の意味
ただし、「使えない」は、同じ目的を達成する手段がまったくないという意味ではありません。
たとえば Clojure は、transducers によって、foldr/build と同じく中間コレクションを作らない処理を書けます。
最適化手法を使えるかの表が示しているのは、初回記事で扱った手法を、その正しさの保証とともに使えるかどうかです。
筆者は、このことを実機で確かめました。
Clojure、Erlang、Common Lisp で、foldr/build、Traversable、Codensity の規則を満たさない関数をあえて書くと、どの言語もエラーを出さず、書き換えの前後で結果が変わりました。
たとえば foldr/build では、n の型を調べる g を書くと、foldr c 0 (build g) が 6、g c 0 が 100 になりました。
同じ関数を Haskell、OCaml、PureScript で書こうとすると、コンパイルの段階で拒否されました。型の中身を調べる手段が、型によって封じられているためです。
タロウくん:
先生、「使えない」と書かれていると、その言語ではもう手の打ちようがない、という意味に読めてしまいます。
専任講師:
そう読まれないように、最適化手法を使えるかの表の直後に、意味を書き添えました。
たとえば Clojure の transducers は、foldr/build と同じく、中間のコレクションを作りません。
手段はあるのです。
タロウくん:
では、何が「使えない」のですか。
専任講師:
初回記事の手法を、正しさの保証とともに使うことです。
foldr/build の規則は、g が forall b. の型を持つから正しいのでした。
型を持たない言語では、g が規則を満たしているかどうかを、プログラマが自ら確かめるしかありません。
第6章で、規則を満たさない g を書くと、書き換えの前後で結果が本当に変わることを確かめます。
3-6 最適化手法を使えるかの表の判定の根拠
最適化手法を使えるかの表の各判定の根拠を、種類ごとに示します。判定のうち、推論にもとづくものはありません。
| 根拠の種類 | 該当する判定 | 確認した内容 |
|---|---|---|
| 実測 | 10-4 の8言語(Standard ML、OCaml、F#、Erlang、PureScript、Scala、Miranda、Common Lisp) | 本稿の実測。いずれも結果が一致し、劇的に速くなった |
| 実測 | 第3章の8言語(Standard ML、OCaml、Common Lisp、Erlang、Scala、F#、PureScript、Miranda)で、プログラマが自らコードを記述して書き換えた結果が一致すること | 本稿の実測 |
| コンパイル確認 | 第4章、10-5 の PureScript、OCaml、Scala |
build と Codensity のコンパイルに成功した |
| コンパイル確認 | 第4章 の F# |
build のコンパイルに成功した |
| コンパイル確認 | 10-5 の F# が条件付きであること | 任意のモナドについての Codensity で、コンパイラが FS0712(Type parameter cannot be used as type constructor)を出した |
| コンパイル確認 | 第4章、10-5 の Standard ML、Miranda が使えないこと | 引数の関数を2つの異なる型で使う関数が、いずれも型エラーになった |
| ソース確認 | 10-2、10-6 の PureScript | purescript-foldable-traversable に Traversable、purescript-validation に Validation が存在する |
| ソース確認 | 10-2、10-6 の Scala | Cats に Traverse と Validated が存在する |
| 実機確認と文献 | Clean のすべての判定 | Wine の上で Windows 版の Clean 3.1 を動かし、すべての手法を書いて動かした。rank-2 type と type constructor class も書けた。Clean のコンパイラの融合変換の効果も測った。文献は Clean 言語報告書 2.2(rank-2 までの universally quantified type と type constructor class)、Alimarine & Smetsers(IFL 2002) |
| 文献 | 10-6 の OCaml、Scala | 初回記事の Applicative の表と同じ判定 |
| 文献 | 10-6 の Standard ML | Wehr & Chakravarty(APLAS 2008)の翻訳元の言語が、Standard ML のサブセットである |
| 文献 | 第3章、10-1 の「使える」「条件付き」の線引き | 各言語が純粋かどうかは、Wikipedia の関数型言語の比較表の Pure の列で確認した(Haskell、Clean、Miranda、PureScript は Yes、他は No)。PureScript は公式パッケージの文書で、値が既定では副作用を持たないことを確認した。純粋でない言語では評価の順序を考慮する必要があることは、Wikipedia の Purely functional programming の記述で確認した |
| 実機確認 | 第3章、10-1 の「条件付き」の条件(副作用がないこと)と、10-3 の判定の訂正 | 純粋でない7言語で、副作用を持つ関数で map f (map g xs) を map (f . g) xs に書き換えると、返す値は同じでも副作用の順序が変わることを確かめた。純粋な Haskell と PureScript では、Int -> Int の関数に副作用を書くとコンパイルが通らないことを確かめた。10-3 は、bind の再結合で関数を呼ぶ順序が変わらないことを確かめ、「使える」に改めた |
| 実測 | 10-5 の PureScript(使える)、OCaml と Scala(条件付き) | Free モナドの左結合の bind で、Codensity を経由すると大幅に速くなることを測った |
| 実測 | 10-2 の PureScript(使える)、OCaml、Standard ML、Scala(条件付き) |
traverse を2回呼び出すコードを1回だけ呼び出すコードに書き換えると、1.69 倍から 4.89 倍速くなることを測った |
| 実測 | 第4章の PureScript(使える)、OCaml、Scala、F#(条件付き) |
foldr c 0 (build g) を、プログラマが自ら g c 0 と記述すると、4.3 倍から 28.8 倍速くなることを測った |
| 実機確認 | Clojure、Erlang、Common Lisp の「使えない」「条件付き」 | 規則を満たさない関数でも言語が止めず、書き換えの前後で結果が変わることを確かめた。静的型の言語では同じ関数がコンパイルで拒否された。10-6 は3言語で書いて動かした |
| コンパイル確認 | 10-2 の Standard ML | Traversable を Applicative を受け取るファンクタとして書き、コンパイルと実行に成功した |
| 実機確認 | 10-1、10-3、10-6 の Miranda | foldMap、bind の再結合、エラーを集める検証を特定の型に固定して書き、実行に成功した |
| 実測 | 10-4 の Clojure | babashka と JVM の両方で測定した |
🔬 上級者向けコラム:foldr/build の規則は、なぜ rank-2 type から導かれるのか
build の引数 g の型は forall b. (a -> b -> b) -> b -> b です。
パラメトリシティによれば、この型を持つ関数は、型 b の値の中身を調べることができません。g にできるのは、受け取った c :: a -> b -> b と n :: b を組み合わせて、型 b の値を作ることだけです。
したがって、g が作る値は、必ず c x1 (c x2 (... (c xk n))) という形になります。
g に (:) と [] を渡すと、リスト [x1, x2, ..., xk] ができます。そのリストを foldr c n で畳み込むと、c x1 (c x2 (... (c xk n))) になります。
g に c と n を直接渡しても、同じ c x1 (c x2 (... (c xk n))) になります。
これが、foldr c n (build g) = g c n が成り立つ理由です。Wadler の自由定理の一例にあたります。
逆に、g が型 b の中身を調べられる言語では、g は b が何であるかによって振る舞いを変えられます。その場合、(:) と [] を渡したときと、c と n を渡したときとで、g が別の振る舞いをしうるため、規則は成り立ちません。第6章で、このことを実機で確かめます。
ただし、Haskell では、1-3 で見た底と seq によって、この議論は厳密には成り立ちません。HaskellWiki の「Correctness of short cut fusion」は、底と seq がある場合に、この規則が成り立たなくなる例を論じています。GHC は、POPL 2006 の論文が正当化した「底を含まない範囲で考える」という約束のうえで、この規則を使っています。
出典:
HaskellWiki, "Correctness of short cut fusion"
https://wiki.haskell.org/Correctness_of_short_cut_fusion
第4章 評価戦略だけを変える:Haskell と PureScript、Miranda
第3章までで、11の関数型言語を4つの軸で整理し、初回記事の8つの最適化手法が各言語で使えるかを表にしました。
第4章からは、その表の根拠を、言語ごとに見ていきます。
本章では、4つの軸のうち 評価戦略の軸だけを動かします。ほかの3つの軸(型付け、型システムの表現力、型クラスの有無)は、できるだけそろえます。
軸を1本だけ動かすと、その軸が結果に何をもたらすのかが、はっきり見えます。
4-1 なぜ Haskell、PureScript、Miranda を並べるのか
この3つの言語は、次の関係にあります。
| 言語 | 評価戦略 | 型システム | 型クラス |
|---|---|---|---|
| Haskell | 非正格 | Hindley-Milner に拡張を加えたもの。rank-2 type と higher-kinded type を書ける | ある |
| PureScript | 正格 | Haskell とほぼ同じ。rank-2 type と higher-kinded type を書ける | ある |
| Miranda | 非正格 | Hindley-Milner の多相型 | ない |
Haskell と PureScript は、型システムと型クラスがほぼ同じで、評価戦略だけが違います。
Haskell と Miranda は、評価戦略が同じ非正格で、型クラスの有無が違います。
この2つの対を並べることで、「評価戦略の違いが何をもたらすか」と、「型クラスの有無が何をもたらすか」を、別々に観測できます。
PureScript が正格評価である理由は、公式の文書に書かれています。
Unlike Haskell, PureScript is strictly evaluated. As the evaluation strategy matches JavaScript, interoperability with existing code is trivial.
筆者による日本語訳:
Haskell とは異なり、PureScript は正格評価である。評価戦略が JavaScript と一致するため、既存コードとの相互運用が容易である。
出典:
PureScript 公式ドキュメント「Differences from Haskell」
https://github.com/purescript/documentation/blob/master/language/Differences-from-Haskell.md
PureScript は JavaScript にコンパイルされる言語です。JavaScript は正格評価なので、それに合わせたということです。
Miranda は、David Turner が1985年に公開した言語です。Haskell に直接影響を与えました。Turner 自身が、Haskell にない Miranda の利点として「より小さい言語、より単純な型システム、より単純な算術」を挙げています。型クラスがないのは、この「より単純な型システム」の一部です。
出典:
D. Turner, "An Overview of Miranda"
https://www.cs.kent.ac.uk/people/staff/dat/miranda/Overview.html
出典:
Wikipedia「Miranda (programming language)」
https://en.wikipedia.org/wiki/Miranda_(programming_language)
4-2 PureScript で map の融合を測る
初回記事で扱った map f (map g xs) = map (f . g) xs の書き換えを、PureScript で測りました。
要素数は2,000,000です。5回測定した中央値を示します。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
lfoldl (+) 0 (lmap f1 (lmap g1 xs)) |
1,042.6 ms | 915.9 ms | 1,198.5 ms |
lfoldl (+) 0 (lmap (f1 <<< g1) xs) |
454.5 ms | 343.4 ms | 460.3 ms |
両者の結果は一致しました。2.29倍の差が出ました。
PureScript は正格評価です。lmap g1 xs の結果である中間リストは、次の lmap f1 が始まる前に、全要素が作られます。
手で融合すれば、その中間リストが消えます。だから2.29倍の差が出ます。
リスト型は自前で定義しました。purescript-lists に依存すると、取得すべきライブラリが増えるためです。
4-3 同じ測定を Miranda で行うと、結果が変わる
同じ map の融合を、Miranda で測りました。
要素数は500,000です。Miranda には時間を測る組み込み関数がないため、プログラム全体の実行時間を外部から測りました。5回測定した中央値を示します。起動のみを行うプログラムの実行時間は2 msでした。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
sum (map f (map g [0..499999])) |
228 ms | 225 ms | 235 ms |
sum (map (f . g) [0..499999]) |
219 ms | 218 ms | 220 ms |
両者の結果は一致しました。起動時間を差し引くと、1.04倍の差でした。
Miranda では、手で融合しても、ほとんど速くなりませんでした。
タロウくん:
先生、同じ書き換えなのに、PureScript では2.29倍で、Miranda では1.04倍です。なぜ、こんなに違うのですか?
専任講師:
評価戦略が違うからです。
PureScript は正格評価です。map g xs を計算すると、その時点で、要素数と同じ長さの中間リストがメモリに作られます。次の map f は、そのリストを先頭から読み直します。
Miranda は非正格評価、つまり遅延評価です。map g [0..499999] の結果は、全要素が一度に作られるわけではありません。sum が要素を1つ要求するたびに、1つずつ作られ、すぐに消費されます。
タロウくん:
中間リストの全体が、メモリに存在する瞬間がない、ということですか?
専任講師:
そのとおりです。
だから、融合によって削減できるものが少ないのです。すでに、ほとんど融合されたのと同じように動いています。
タロウくん:
遅延評価のほうが、いつも速いということでしょうか。
専任講師:
そうとは言えません。
遅延評価には、評価を遅らせるための仕組みを保持する費用がかかります。Miranda の1回の測定で、要素数が PureScript の4分の1なのに、実行時間が短いのは、比較の条件がそろっていないからです。
ここで比べているのは、言語どうしの速さではありません。同じ言語の中で、手で融合したときと、しなかったときの差です。その差の大きさが、評価戦略によって変わる、という話です。
4-4 PureScript の測定で判明した注意点
PureScript の Int は32ビットです。JavaScript へのコンパイル時に、加算の結果に |0 が付加されるためです。
要素数2,000,000の総和は32ビットの範囲を超えるため、結果は桁あふれして折り返された値になります。
ただし、両方の書き方で同じように折り返されるため、結果が一致するかどうかの比較は有効です。
ここで、第5章と第6章の測定を先取りして述べておきます。同じ桁あふれが、MLton と F# では例外になりました。PureScript では例外にならず、黙って折り返します。
同じ「整数の桁あふれ」でも、言語によって起きることが違います。測定の結果を読むときは、この違いに注意してください。
4-5 Difference List は、どちらの言語でも効く
初回記事で扱った Difference List を、両方の言語で測りました。
PureScript(要素数20,000)
| 書き方 | 中央値 |
|---|---|
| 左結合の連結の繰り返し | 3,500.5 ms |
| Difference List | 3.6 ms |
両者の結果は一致しました。972倍の差が出ました。
Miranda(要素数8,000。左結合の連結は3回、Difference List は5回測定した中央値)
| 書き方 | 中央値 |
|---|---|
acc ++ [1] の繰り返し |
1,053 ms |
| Difference List | 6 ms |
両者の結果は一致しました。起動時間を差し引くと、263倍の差でした。
タロウくん:
先生、map の融合では、Miranda はほとんど速くなりませんでした。でも Difference List では、263倍も速くなっています。
専任講師:
よい対比です。
2つの最適化は、効く理由が違います。
map の融合が削るのは、中間リストを作る費用です。遅延評価では、その中間リストがそもそも一度に作られないので、削るものが少ない。
Difference List が削るのは、計算量そのものです。左結合の連結を繰り返すと、連結のたびに左側の全体を走査し直すため、O(n²) になります。Difference List は、これを O(n) にします。
タロウくん:
計算量の問題は、評価を遅らせても消えないのですね。
専任講師:
そのとおりです。
O(n²) は O(n²) のままです。遅延評価は、計算を後回しにするだけで、計算の総量を減らすわけではありません。
この区別は、本稿の最適化手法を読むときに、繰り返し出てきます。中間のデータ構造を削る手法と、計算量そのものを変える手法は、別のものです。
4-6 正格評価では、底の扱いが変わる
初回記事の第7章で、底(bottom)と seq を扱いました。使われない引数に底を渡したとき、何が起きるかを、両方の言語で確かめました。
| 言語 | 評価した式 | 結果 |
|---|---|---|
| Haskell | (\_ -> 1) (error "bottom") |
1 を返した |
| PureScript | (\_ -> 1) (crash unit) |
例外を投げた |
crash は、呼ばれると例外を投げる関数として FFI で定義しました。
Haskell は非正格評価です。使われない引数は評価されません。したがって、底が渡されても1を返します。
PureScript は正格評価です。関数を呼ぶ前に、引数をすべて評価します。したがって、底を評価した時点で例外が発生します。
タロウくん:
先生、これは PureScript のほうが不便だということでしょうか。
専任講師:
不便かどうかではなく、性質が違う、というのが正確です。
初回記事で論じた「seq を使ったときにだけ恒等律が破れる」という現象は、PureScript では生じません。すべての引数が先に評価されるので、seq で評価を強制するまでもないからです。
代わりに、正格評価には正格評価なりの制約があります。4-2 で測ったとおり、map f (map g xs) の中間リストは、全要素がメモリに作られます。
タロウくん:
片方の問題がなくなる代わりに、別の問題が出てくるのですね。
専任講師:
そういうことです。
どちらが優れているという話ではありません。評価戦略を選ぶと、何が起きて何が起きないかが決まる、ということです。
PureScript は、部分性を型で表す仕組みも持っています。Partial 型クラスです。公式のパッケージには、次のように書かれています。
It's important that types tell the truth wherever possible, because this is a large part of what allows us to understand PureScript code easily and refactor it fearlessly.
筆者による日本語訳:
型が可能なかぎり真実を語ることが重要である。それが、PureScript のコードを容易に理解し、恐れることなくリファクタリングできる理由の大部分だからである。
出典:
purescript-partial パッケージ
https://github.com/purescript/purescript-partial
底を作る手段は unsafeCrashWith :: forall a. String -> a です。名前に unsafe が付いていることからも、これが例外的な操作として扱われていることが分かります。
4-7 恒等律の破れは、Haskell 固有ではない
ここからが、本章でもっとも重要な測定です。
初回記事の第7章で、「Hask は、厳密には圏ではない」という論点を扱いました。seq があるために、圏の公理のひとつである恒等律が破れる、という話です。
同じ現象が、Miranda でも起きるかを確かめました。
| 言語 | seq bottomfn 1 |
seq (bottomfn . id) 1 |
|---|---|---|
| Haskell | 例外 | 1 を返した |
| Miranda | 例外 | 1 を返した |
bottomfn は error "bottom" と定義しました。
あわせて、使われない引数に底を渡す測定も行いました。
| 言語 | 評価した式 | 結果 |
|---|---|---|
| Miranda |
const1 bottomval(const1 x = 1) |
1 を返した |
| Miranda | seq bottomval 1 |
例外 |
Miranda でも、Haskell とまったく同じ形で、恒等律が破れました。
タロウくん:
先生、これは何が起きているのですか。
専任講師:
bottomfn と bottomfn . id は、恒等律によれば等しいはずです。id は何もしない関数なので、合成しても元の関数と同じになる。それが恒等律です。
ところが、seq はこの2つを区別します。
タロウくん:
なぜ区別できるのですか?
専任講師:
bottomfn は、評価すると底になります。seq は引数を弱頭正規形まで評価するので、ここで例外が起きます。
タロウくん:
先生、弱頭正規形というのは、何でしょうか。初めて聞く言葉です。
専任講師:
いちばん外側だけを見て、それ以上簡単にできない形のことです。
たとえば (1+2, 3+4) という組は、中身はまだ計算されていませんが、いちばん外側は「組である」と分かります。これで弱頭正規形です。中の 1+2 は計算しません。
タロウくん:
中まで全部計算するわけではないのですね。
専任講師:
はい。そこが「弱」という言葉の意味です。
seq は、この弱頭正規形までしか評価しません。だから、組の中に底が入っていても、seq は気づきません。外側が組だと分かった時点で止まるからです。
タロウくん:
すると、いま見ている bottomfn . id も、外側だけ見れば……
専任講師:
関数です。だから seq は、そこで止まります。中を見ないので、底に触れません。
一方、bottomfn . id は、関数合成の結果です。合成した時点では、まだ bottomfn を呼んでいません。関数値がひとつできただけです。seq は、この関数値を底とはみなしません。
タロウくん:
同じはずの2つが、seq から見ると違って見える、ということですね。
専任講師:
そのとおりです。
そして、この結果から分かることがあります。
初回記事の「Hask は圏ではない」という論点は、Haskell 固有の問題ではありません。
タロウくん:
Miranda でも同じことが起きたから、ですか。
専任講師:
そうです。
非正格評価であることと、seq を持つことの2つがそろえば、同じ問題が生じます。
Miranda は Haskell の前身で、1985年に登場した言語です。この問題は、Haskell が生まれる前から存在していたことになります。
タロウくん:
型クラスは関係ないのですか。Miranda には型クラスがないのですよね。
専任講師:
よい着眼です。関係ありません。
本連載の4軸でいえば、この問題は「評価戦略」の軸に属します。Miranda は型クラスを持たないのに、同じ問題が起きました。型クラスの有無は、この現象と無関係だということです。
この測定は、Executive Summary で述べた「恒等律の破れは、Haskell だけの問題ではない」という結論の、実機での裏付けです。
4-8 Miranda のビルドで判明した注意点
Miranda を自分で動かしてみたい読者のために、つまずいた箇所を書いておきます。
その1 最適化指定
GitHub のミラーからそのままビルドすると、一部のプログラムが impossible tag (-9) in reduce や BLACK HOLE という異常終了を起こしました。
Miranda の README には、ガベージコレクタが C のスタックを走査して動作するため、積極的なコンパイラ最適化に弱い、という警告があります。
Makefile の最適化指定を -O2 から -O0 に変更してビルドし直したところ、すべてのプログラムが正常に動作しました。
その2 予約されている名前
Miranda では undef が組み込みの名前として予約されています。底を表す変数に undef という名前を付けると、コンパイルが中断されます。
底を表す変数には、別の名前を付けてください。本稿の測定では bottomval と bottomfn を使いました。
導入した処理系は、次のとおりです。
| 言語 | 処理系 | バージョン |
|---|---|---|
| PureScript | purs | 0.15.16(ライブラリは prelude、effect、console を使用) |
| Miranda | mira | 2.066(GitHub 上のミラー ncihnegn/miranda のソースコードからビルド) |
| Haskell(比較用) | GHC | 9.4.7 |
PureScript の実行には Node.js v22.22.2 を用いました。
Miranda の版数2.066は、公式サイトに記載された最終安定版(2020年1月31日)と同じです。
出典:
ncihnegn/miranda(GitHub)
https://github.com/ncihnegn/miranda
出典:
Miranda 公式サイト
https://miranda.org.uk
4-9 本章のまとめ
評価戦略の軸だけを動かして分かったことを、整理します。
| 観測したこと | 結果 |
|---|---|
map の手動融合の効き方 |
正格評価(PureScript)で2.29倍、非正格評価(Miranda)で1.04倍。中間リストが一度に作られるかどうかで決まる |
| Difference List の効き方 | PureScript で972倍、Miranda で263倍。計算量を変える手法なので、評価戦略にかかわらず大きく効く |
| 使われない引数の底 | 非正格評価(Haskell)では1を返す。正格評価(PureScript)では例外になる |
seq による恒等律の破れ |
非正格評価で seq があれば起きる。Haskell でも Miranda でも同じ形で再現した。型クラスの有無は無関係 |
次の第5章では、評価戦略を正格に固定したうえで、言語機能の軸を動かします。OCaml、Standard ML、Scala、F# の4つの言語を見ていきます。
第5章 言語機能を変える:OCaml、Standard ML、Scala、F#
第4章では、評価戦略の軸を動かしました。本章では、評価戦略を正格に固定したうえで、言語機能の軸を動かします。
取り上げるのは、OCaml、Standard ML、Scala、F# の4つです。いずれも正格評価の言語ですが、最適化の実現手段がそれぞれ違います。
| 言語 | 型クラスに相当するもの | 中間データを消す主な手段 |
|---|---|---|
| OCaml | なし。モジュールとファンクタで代用する | プログラマが手で書き換える。Flambda はインライン展開が中心 |
| Standard ML | なし。同上 | MLton の whole-program optimization |
| Scala | implicit で表現する(Cats ライブラリが代表的) |
view(遅延評価のビュー) |
| F# | なし |
Seq(遅延評価の列)、inline 関数 |
本章では、この4つの言語で同じ書き換えを測り、何が言語機能で解決され、何がプログラマの仕事として残るのかを見ていきます。
5-1 OCaml では、融合は手で書く
初回記事の第3章で扱った Functor 則による書き換え(map f (map g xs) = map (f . g) xs)を、OCaml で測りました。
要素数は2,000,000です。5回測定した中央値を示します。
| 書き方 | 中央値 | 最小 | 最大 | 確保語数 |
|---|---|---|---|---|
List.fold_left (+) 0 (List.map f (List.map g xs)) |
540.3 ms | 532.3 ms | 586.9 ms | 23,825,721 words |
List.fold_left (+) 0 (List.map (fun x -> f (g x)) xs) |
266.7 ms | 264.2 ms | 268.5 ms | 11,898,240 words |
両者の結果は一致しました。時間は2.03倍、メモリは2.00倍の差が出ました。
確保語数がちょうど半分になっている点が重要です。中間リストが1本消えたことが、数字にそのまま現れています。
GHC は map f (map g xs) を map (f . g) xs に自動で書き換えます。RULES プラグマが標準ライブラリに書かれているためです。
OCaml には、RULES に相当する仕組みがありません。したがって、この書き換えはプログラマが手で行う必要があります。
5-2 Flambda を有効にしても、融合は行われない
ここで、ひとつの疑問が生じます。
OCaml には Flambda という最適化の仕組みがあります。Flambda を有効にすれば、コンパイラが融合を行ってくれるのではないか、という疑問です。
タロウくん:
先生、Flambda というのは何ですか。
専任講師:
OCaml のコンパイラに備わった、一連の最適化の処理の名前です。関数のインライン展開などを、標準より積極的に行います。
注意すべき点があります。Flambda は、コンパイラを作る段階で有効にしておく必要があります。配布されている OCaml では、無効になっていることが多いのです。
タロウくん:
使っている OCaml で有効になっているかは、どうすれば分かりますか。
専任講師:
ocamlopt -config を実行してください。出力の中に flambda: という行があります。true なら有効、false なら無効です。
Jane Street のブログは、OCaml におけるインライン展開の意味を、次のように説明しています。
In a language like OCaml, inlining is about more than just function call overhead. That's because inlining grows the amount of code that the optimizer can look at a given point, and that makes other optimizations more effective.
筆者による日本語訳:
OCaml のような言語では、インライン展開は関数呼び出しのオーバーヘッド削減以上の意味を持つ。インライン展開によって最適化器が一度に見られるコード量が増え、他の最適化がより効果的になるからである。
出典:
Jane Street Blog, "A better inliner for OCaml, and why it matters"
https://blog.janestreet.com/flambda/
出典:
OCaml 公式マニュアル「Optimisation with Flambda」
https://ocaml.org/manual/5.4/flambda.html
本稿では、GitHub から OCaml 4.14.1 のソースコードを取得し、./configure --enable-flambda でビルドしました。配布されている版と同じ版で、Flambda の有無だけが違います。
ocamlopt -config の出力は flambda: true でした。
両方の処理系で、同じコードを -O3 でコンパイルして測りました。
| 測定 | 書き方 | Flambda なし | Flambda 版 |
|---|---|---|---|
| map の融合(要素数2,000,000) | 融合なし | 544.6 ms(23,825,721 words) | 508.9 ms(23,694,651 words) |
| 同上 | 手で融合 | 265.8 ms(11,898,240 words) | 242.8 ms(11,767,170 words) |
| Difference List(要素数40,000) | 左結合の @
|
23,331.4 ms | 23,516.7 ms |
| 同上 | Difference List | 0.8 ms | 0.8 ms |
| Codensity(n = 12,000) | 素朴な書き方 | 0.9584 s | 0.9495 s |
| 同上 | Codensity を経由 | 0.000750 s | 0.000437 s |
| Codensity(n = 800,000) | Codensity を経由 | 0.1851 s | 0.1421 s |
| Traversable(要素数1,000,000) | 2回の走査 | 129.6 ms | 144.9 ms |
| 同上 | 1回にまとめる | 66.7 ms | 84.8 ms |
| foldr/build(要素数1,000,000) | foldr c 0 (build g) |
118.0 ms | 104.2 ms |
| 同上 |
g c 0(規則を手で適用) |
15.5 ms | 12.1 ms |
すべての測定で、書き方どうしの結果は一致しました。
タロウくん:
先生、Flambda を有効にしても、融合なしの確保語数が2,370万語のままです。
専任講師:
そこが、この測定でもっとも重要な点です。
中間リストは消えていません。手で融合した場合との差は、Flambda なしで2.05倍、Flambda 版で2.10倍であり、ほぼ変わりませんでした。
つまり、Flambda は map の融合を行いません。OCaml で融合を得るには、Flambda の有無にかかわらず、プログラマが手で書き換える必要があります。
タロウくん:
Flambda は、何も効いていないのでしょうか。
専任講師:
いいえ。効いている箇所もあります。
Codensity を経由した書き方と、規則を手で適用した foldr/build は、Flambda 版のほうが速くなりました。インライン展開がよく効いたためと考えられますが、そこまでは確かめていません。
一方、Traversable は Flambda 版のほうが遅くなりました。理由は確かめていません。
素朴な書き方の Codensity と、左結合の @ は、Flambda 版でもほとんど変わりませんでした。計算量の違いは、コンパイラの最適化では埋まりません。
5-3 測定の値を比べるときの注意
第5章の Flambda の測定には、ひとつ注意があります。
この測定は、本稿のほかの節とは別の時期に行いました。そのため、同じコードを測っても、値が一致しません。たとえば Codensity の素朴な書き方は、n = 12,000 で、ほかの節では 0.2297 s、この節では 0.9584 s でした。
したがって、5-2 の表の値は、本稿のほかの節の値と直接比べないでください。
Flambda の有無による2つの値は、同じ時期に続けて測ったので、その2つのあいだでのみ比べられます。
5-4 Standard ML:モジュールで包んでも遅くならない
Standard ML は、広く使われている言語のなかでは珍しく、形式仕様を持っています。
It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML.
筆者による日本語訳:
Standard ML は、広く使われている言語のなかで、型付け規則と操作的意味論として与えられた形式仕様を『The Definition of Standard ML』に持つ点で際立っている。
出典:
Wikipedia「Standard ML」
https://en.wikipedia.org/wiki/Standard_ML
出典:
R. Milner, M. Tofte, R. Harper, D. MacQueen, The Definition of Standard ML (Revised), MIT Press, 1997
まず、map の手動融合を測りました。要素数は2,000,000、5回測定した中央値です。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
foldl (op +) 0 (map f (map g xs)) |
152.1 ms | 122.7 ms | 436.5 ms |
foldl (op +) 0 (map (fn x => f (g x)) xs) |
87.1 ms | 82.1 ms | 92.0 ms |
両者の結果は一致しました。1.75倍の差が出ました。ここまでは OCaml と同じ構図です。
次に、Standard ML に特有の測定を行いました。モジュールで包むと遅くなるか、という測定です。
要素数は5,000,000、5回測定した中央値です。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
| 直接書いた関数 | 21.1 ms | 20.6 ms | 21.4 ms |
| シグネチャ付き structure に包む | 20.7 ms | 20.6 ms | 20.8 ms |
| ファンクタで包む | 20.6 ms | 20.3 ms | 20.6 ms |
| ファンクタで二重に包む | 20.5 ms | 20.4 ms | 21.6 ms |
4つすべての結果は一致しました。差は3パーセント未満で、測定誤差の範囲に収まっています。
タロウくん:
先生、モジュールで包んでも、二重に包んでも、速度が変わらないのですね。
専任講師:
そのとおりです。MLton の文献にある記述を、実機で確かめられました。
MLton's use of defunctorization means that the placement of code in modules has no effect on performance.
筆者による日本語訳:
MLton が defunctorization を行うため、モジュールにおけるコードの配置は性能にまったく影響しない。
出典:
"Adding Real-time Capabilities to a SML Compiler"(MLton の構造を解説)
https://arxiv.org/pdf/1601.03116
出典:
MLton 公式サイト「Whole-Program Optimization」
http://mlton.org/WholeProgramOptimization
タロウくん:
なぜ、そんなことができるのですか。
専任講師:
MLton は、プログラム全体を一度に見てコンパイルします。whole-program optimization と呼びます。
タロウくん:
先生、その whole-program optimization というのは、どういうものですか。
専任講師:
ふつうのコンパイラは、ファイルを1つずつ別々にコンパイルします。分割コンパイルと呼びます。
MLton は、これをしません。プログラム全体を1つのかたまりとして、最初から最後まで見渡してからコンパイルします。
タロウくん:
全部見えていると、何ができるのですか。
専任講師:
ある関数が、どこから、どんな型で呼ばれているかが、すべて分かります。だから、呼ばれ方に合わせて関数を作り直せます。
その過程で、ファンクタを適用箇所ごとに複製し、モジュールを変数の改名で消し去ってしまいます。実行される段階では、モジュールという構造はもう残っていません。
タロウくん:
消してしまうのですか。
専任講師:
はい。この変換を defunctorization と呼びます。
「ファンクタを取り除く」という意味です。MLton はほかに、多相関数を使われる型ごとに複製する monomorphization と、高階関数をデータ構造に置き換える defunctionalization も行います。
タロウくん:
いずれも「抽象化のための仕組みを、実行前に消してしまう」のですね。
専任講師:
よい整理です。そのとおりです。
だから、モジュールで何重に包んでも、実行時の速さが変わりません。
タロウくん:
それなら、性能を気にせずにモジュールで構造化できますね。
専任講師:
そういうことです。これは OCaml との重要な違いです。
OCaml は分割コンパイルを行うため、プログラム全体を一度に見ることができません。whole-program optimization はできません。
同じ ML 系の言語でも、コンパイラの方針が違えば、プログラマが気にすべきことが変わります。
5-5 OCaml と Standard ML に型クラスがないことの意味
ここで、誤解されやすい点を整理します。
OCaml と Standard ML には、型クラスがありません。初回記事で扱った手法のうち、型クラスを使うものは、そのままでは書けません。
タロウくん:
先生、それは OCaml や Standard ML が、Haskell より劣っているということでしょうか。
専任講師:
いいえ。そう書くと、誤解を招きます。
ML のモジュールと Haskell の型クラスは、表現力において等価であることが証明されています。
タロウくん:
証明されているのですか。
専任講師:
はい。Wehr と Chakravarty の論文が、ML のモジュールと Haskell の型クラスのあいだで、型を保存する双方向の翻訳を定式化し、型の正しさが保たれることを証明しています。
出典:
S. Wehr, M. M. T. Chakravarty, "ML Modules and Haskell Type Classes: A Constructive Comparison", APLAS 2008, LNCS 5356, Springer, pp. 188–204
doi: 10.1007/978-3-540-89330-1_14
https://link.springer.com/chapter/10.1007/978-3-540-89330-1_14
出典:
Wehr の修士論文(全文)
https://stefanwehr.de/publications/Wehr_ML_modules_and_Haskell_type_classes.pdf
専任講師:
したがって、「OCaml には型クラスがないから使えない」という書き方は正確ではありません。
正確には、「型クラスとしては書けないが、モジュールとファンクタで同じことを表現できる。ただし、書き方は変わり、コンパイラによる自動の書き換えは期待できない」となります。
表Bで「条件付き」としてある箇所の多くは、この事情によるものです。
5-6 Scala と F#:ライブラリが遅延評価を提供する
Scala と F# は、別の手段で中間データを消します。
Scala の測定(要素数2,000,000。JIT を効かせるため3回のウォームアップの後、5回測定した中央値)
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
xs.map(g).map(f).sum |
456.0 ms | 128.9 ms | 626.4 ms |
xs.map(x => f(g(x))).sum |
111.4 ms | 104.4 ms | 439.6 ms |
xs.view.map(g).map(f).sum |
25.8 ms | 25.4 ms | 98.3 ms |
3つすべての結果は一致しました。
view を挟むと、融合なしの17.7倍速くなりました。手で融合した場合と比べても4.3倍速くなっています。
F# の測定(要素数2,000,000。3回のウォームアップの後、5回測定した中央値)
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
List.map g >> List.map f >> List.sum |
357.8 ms | 317.9 ms | 397.7 ms |
List.map (fun x -> f (g x)) >> List.sum |
184.2 ms | 111.3 ms | 213.3 ms |
Seq.map g >> Seq.map f >> Seq.sum |
67.2 ms | 67.1 ms | 68.8 ms |
3つすべての結果は一致しました。Seq を使うと、融合なしの5.3倍速くなりました。
タロウくん:
先生、view や Seq を挟むと、手で融合するより速いのですね。手で融合したほうが速いと思っていました。
専任講師:
よい気づきです。理由を説明します。
view と Seq は、遅延評価のビューや列を返します。map を2回書いても、中間コレクションは作られません。要素を1つずつ取り出し、2つの関数を続けて適用します。
手で融合した書き方は、中間リストを1本減らしますが、結果のリストは作ります。view と Seq は、その結果のリストすら作らずに、sum へ直接流し込みます。
タロウくん:
第4章で見た、Miranda の遅延評価と同じことですか。
専任講師:
発想は同じです。ただし、実現の場所が違います。
Miranda は、言語そのものが遅延評価です。Scala と F# は正格評価の言語で、ライブラリが遅延評価のデータ構造を提供しているのです。
タロウくん:
Haskell の foldr/build とも、結果として同じことをしているのでしょうか。
専任講師:
結果は近いものになります。しかし、手段が違います。
Haskell は、コンパイラが書き換え規則にもとづいて書き換えます。Scala と F# は、プログラマが view や Seq と書くことで、ライブラリの遅延評価の仕組みを呼び出します。
本連載の4軸でいえば、Scala と F# は「言語機能」の側で解決しています。この区別は、第9章の「誰が圏論の知識を使うのか」で、もう一度扱います。
5-7 F# の inline 関数は、この測定では差が出なかった
F# には inline 関数という機能があります。
an inline function is a function that is integrated into the calling code. It is integrated in the sense that the type is not generalized, but it is compiled accordingly when the inline function is used within other functions.
筆者による日本語訳:
inline 関数とは、呼び出し元のコードに統合される関数である。型が一般化されず、他の関数の中で使われたときにそれに応じてコンパイルされるという意味で統合されている。
出典:
『F# High Performance』第7章「Language Features and Constructs Optimization」
https://packtpub.com/en-us/product/f-high-performance-9781786468079/
この inline が速度に効くかを測りました。要素数は2,000,000、5回測定した中央値です。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
通常の関数 f (g x)
|
180.6 ms | 112.9 ms | 205.2 ms |
inline 関数 finl (ginl x)
|
173.2 ms | 107.7 ms | 207.1 ms |
両者の結果は一致しました。差は1.04倍であり、測定誤差の範囲に収まっています。
有意な差が出なかった理由として、2つ考えられます。
1つ目。この関数は十分に小さく、Mono の JIT がすでにインライン展開していた可能性があります。
2つ目。List.map の呼び出しそのものが支配的で、関数本体の費用が相対的に小さかった可能性があります。
なお、F# の inline は、型が一般化されないという点に本来の意味があります。静的に解決される演算子制約を書くために使うものです。単純な算術関数のインライン展開は、本来の用途ではありません。
この測定は、inline の本来の効果を測ったものではない、という点にご注意ください。
5-8 Difference List は4言語すべてで大きく効く
Difference List を、4つの言語すべてで測りました。要素数は40,000です。
| 言語 | 左結合の連結 | Difference List | 倍率 |
|---|---|---|---|
| Standard ML | 11,989.0 ms | 0.3 ms | 39,963倍 |
| OCaml | 23,331.4 ms | 0.8 ms | 29,238倍 |
| F# | 31,680.7 ms | 1.3 ms | 24,370倍 |
| Scala | 4,024.3 ms | 9.2 ms | 437倍 |
いずれも、両者の結果は一致しました。
第4章で見たとおり、Difference List は計算量そのものを変える手法です。O(n²) を O(n) にします。したがって、言語機能や評価戦略にかかわらず、大きく効きます。
Scala の倍率が小さいのは、左結合の連結の側がほかの言語より速いためです。JVM の性能と、List の実装の違いによるものと考えられます。
なお、Scala では、連結の順序による差も測りました。2,000本のリスト(各1,000要素)を連結した測定です。
| 書き方 | 中央値 |
|---|---|
左結合 foldLeft((acc, c) => acc ++ c)
|
30,972.5 ms |
右結合 foldRight((c, acc) => c ++ acc)
|
33.3 ms |
両者の結果は一致しました。930倍の差が出ました。
結合律が成り立つことと、どちらが速いかは、別の話です。圏論は「書き換えてよい」という許可を出しますが、「どちらが速いか」は教えてくれません。第1章で述べた論点が、ここでも現れています。
5-9 Scala で Cats を使う
Scala には Cats という関数型プログラミングのライブラリがあります。初回記事で扱った手法の多くが、ここに実装されています。
本稿では、GitHub から Cats 2.13.0 のソースコードを取得し、Scala 3.3.6 でビルドして測りました。kernel(534クラス)、core(2,409クラス)、free(127クラス)をコンパイルしています。
出典:
typelevel/cats(GitHub)タグ v2.13.0
https://github.com/typelevel/cats
出典:
scala/scala3(GitHub)リリース 3.3.6
https://github.com/scala/scala3
測定の結果は、次のとおりです。
| 手法 | Cats の仕組み | 結果 |
|---|---|---|
| foldMap | Foldable.foldMap |
1から10までを2倍して合計し、110 |
| Traversable(要素数1,000,000、Option) | Traverse |
2回の走査 1,140.3 ms、1回にまとめて 383.0 ms。2.98倍。結果は一致 |
| Difference List(要素数40,000) | Chain |
List の左結合の ++ 3,350.7 ms、Chain の ++ 4.97 ms。結果は一致 |
| 全エラー集約 |
Validated(ValidatedNel と mapN) |
2つとも誤りのとき Invalid(NonEmptyList(name is empty, age is negative))。2つとも正しいとき Valid((Taro,20))
|
いずれも、表Bの判定と整合しました。
なお、この測定は Scala 3.3.6 で行いました。5-6 と 5-8 の Scala の測定は 2.11.12 で行っています。版も測定の時期も異なるため、値を直接比べないでください。
5-10 Cats の Free は、ライブラリ自身が結合律で書き換えている
Cats には Codensity が含まれていませんでした。そこで、それに近い効果を持つ仕組みとして、cats-free の Free を測りました。
flatMap を左結合に n 回重ね、State モナドへの自然変換で解釈しました。
| n | 所要時間 |
|---|---|
| 3,000 | 22.667 ms |
| 6,000 | 18.742 ms |
| 12,000 | 15.847 ms |
| 100,000 | 70.477 ms |
| 200,000 | 108.738 ms |
| 400,000 | 208.658 ms |
n が小さい範囲では、JIT の効き始めの影響で、n が増えても所要時間が減っています。n が100,000を超える範囲では、n が倍になるたびにおよそ1.5倍から1.9倍に伸びました。2乗には伸びていません。
タロウくん:
先生、左結合に重ねたのに、2乗になっていません。なぜですか。
専任講師:
ライブラリが、内部で書き換えているからです。
cats-free の Free のソースを確かめたところ、step という関数で、左結合に重なった bind を右結合に組み替えていました。
case FlatMapped(FlatMapped(c, f), g) => c.flatMap(cc => f(cc).flatMap(g)).step
タロウくん:
これは、モナドの結合律そのものですね。
専任講師:
そのとおりです。よい整理です。
第8章で扱う Codensity は、この書き換えを利用者の側で行う手法です。cats-free では、ライブラリの作者が、同じ書き換えを内部に組み込んでいます。
タロウくん:
だから、利用者は左結合で書いても、遅くならないのですね。
専任講師:
そういうことです。
第9章で扱う「誰が圏論の知識を使うのか」という問いの、ひとつの答えがここにあります。この場合、圏論の知識を使ったのは、ライブラリの作者です。利用者は、その恩恵だけを受けています。
5-11 測定で判明した注意点
4つの言語で、それぞれつまずいた箇所を書いておきます。
Standard ML(MLton)
MLton の既定の int は32ビットです。Int.maxInt は2,147,483,647でした。要素数2,000,000の総和を計算すると4,000,000,000,000となり、32ビットの範囲を超えて Overflow 例外が発生します。
-default-type int64 オプションを指定して解決しました。
Standard ML の言語仕様は、int の大きさを実装依存としています。
F#
F# の int も32ビットです。同じ桁あふれが起きます。F# では例外になりました。
第4章で述べたとおり、PureScript では例外にならず、黙って折り返します。同じ桁あふれでも、言語によって起きることが違います。
Scala
5-6 と 5-8 の測定では Cats を使っていません。5-9 と 5-10 は、ソースからビルドした Cats で測りました。測定の時期も Scala の版も異なるため、両者の値を直接比べないでください。
5-12 本章のまとめ
正格評価の4言語で、言語機能の軸を動かして分かったことを整理します。
| 言語 | 中間データを消す手段 | 誰が書くか |
|---|---|---|
| OCaml | 手で書き換える。Flambda は融合を行わない | プログラマ |
| Standard ML | 手で書き換える。ただしモジュールの抽象化は無料(MLton) | プログラマ |
| Scala |
view、または Cats の Chain など |
プログラマがライブラリを呼ぶ。書き換えはライブラリの作者が組み込み済み |
| F# | Seq |
同上 |
4つの言語はいずれも正格評価ですが、最適化の実現手段は異なります。
Haskell のようにコンパイラが自動で書き換える言語は、この4つの中にはありません。プログラマが書くか、ライブラリの作者があらかじめ書いておくかの、どちらかです。
次の第6章では、型付けの軸を動かします。Clojure、Erlang、Common Lisp という動的型付けの言語を見ていきます。型がないところで、圏論由来の最適化がどう扱われるのかが主題です。
第6章 型付けを変える:Clojure、Erlang、Common Lisp
第5章までで、正格評価の言語を型付きの側から見てきました。本章では、型付けの軸を動かします。
取り上げるのは、Clojure、Erlang、Common Lisp の3つです。いずれも動的型付けの言語です。
第2章で述べたとおり、初回記事で扱った手法の多くは、型の情報を使います。自由定理とパラメトリシティは、型シグネチャがあって初めて成り立ちます。
それでは、型シグネチャのない言語では、これらの手法は使えないのでしょうか。
本章の答えは、「手法そのものは使えないが、同じ目的は別の手段で達成されている」です。
6-1 Clojure の transducers は、型を使わずに中間データを消す
Clojure には transducers という仕組みがあります。公式ドキュメントは、次のように説明しています。
Transducers are composable algorithmic transformations. They are independent from the context of their input and output sources and specify only the essence of the transformation in terms of an individual element. Transducers compose directly, without awareness of input or creation of intermediate aggregates.
筆者による日本語訳:
transducers は合成可能なアルゴリズム的変換である。入出力のコンテキストから独立しており、個々の要素に対する変換の本質だけを指定する。transducers は、入力を意識することなく、また中間集約を作ることなく、直接合成される。
出典:
Clojure 公式ドキュメント「Transducers」
https://clojure.org/reference/transducers
実機で測りました。要素数は1,000,000、5回測定した中央値です。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
(->> xs (map f) (filter p) (reduce +)) |
140.4 ms | 121.4 ms | 177.1 ms |
(transduce (comp (map f) (filter p)) + 0 xs) |
89.2 ms | 88.1 ms | 90.7 ms |
両者の結果は一致しました。1.57倍の差が出ました。
3段の変換と、into による収集も測りました。
| 測定 | 書き方 | 中央値 |
|---|---|---|
| 3段の変換(要素数1,000,000) | (->> xs (map f) (map g) (filter p) (reduce +)) |
169.6 ms |
| 同上 | (transduce (comp (map f) (map g) (filter p)) + 0 xs) |
151.2 ms |
into による収集(要素数1,000,000) |
(into [] (filter p (map f xs))) |
104.4 ms |
| 同上 | (into [] (comp (map f) (filter p)) xs) |
89.8 ms |
いずれも、書き方どうしの結果は一致しました。
タロウくん:
先生、Clojure には型シグネチャがありません。それなのに、中間データを消せるのですか。
専任講師:
消せます。仕組みが違うのです。
transducers は、reducing function を別の reducing function に変換する関数です。通常の関数合成、つまり comp で合成できます。
タロウくん:
型は使っていないのですか。
専任講師:
使っていません。関数合成だけで成り立っています。
初回記事で扱った foldr/build の書き換えは、rank-2 type とパラメトリシティを使って、規則の正しさを保証していました。transducers には、そうした型による保証はありません。
代わりに、中間集約を作らないという性質が、仕組みそのものに組み込まれています。
タロウくん:
どちらが良いのでしょうか。
専任講師:
目的が違うので、良し悪しでは比べられません。
型による保証がある側は、「この書き換えをしてよい」という根拠が型から出てきます。コンパイラが自動で書き換えられるのは、そのためです。
transducers は、プログラマが「この書き方を使う」と選びます。書き換えの正しさは、ライブラリの作者が保証しています。
本連載の4軸でいえば、「型理論」の軸に○が付かなくても、別の手段で同じ目的を達成できる、という例です。
6-2 Clojure で差が小さいのは、なぜか
Clojure の測定で得られた差は、1.12倍から1.57倍でした。第5章で見た OCaml の Difference List の29,238倍とは、桁が違います。
タロウくん:
先生、transducers の効果は、思ったより小さいですね。
専任講師:
その理由は、2つ考えられます。
1つ目。Clojure の lazy sequence は、もともと要素を1つずつ生成します。中間コレクションを全部メモリに置くわけではありません。したがって、transducers による削減の余地が小さいのです。
第4章で見た Miranda と、同じ構図です。遅延して作られるものは、もともと融合されたように動いています。
2つ目。この測定は、babashka という処理系の SCI インタプリタで行いました。JVM 上の通常の Clojure ではありません。インタプリタの負担が、実行時間の大半を占めていた可能性があります。
タロウくん:
どちらが理由なのか、確かめられるのですか。
専任講師:
2つ目については確かめられます。JVM 上の通常の Clojure で測り直しました。
Clojure 1.11.1 を、OpenJDK 21 の上で実行しました。JIT を効かせるため、各測定の前に5回の予備実行を行い、7回測定した中央値を示します。
| 測定 | 書き方 | JVM(中央値) | babashka(中央値) |
|---|---|---|---|
| map の融合(要素数2,000,000) | (reduce + (map f (map g xs))) |
36.5 ms | 349.5 ms |
| 同上 | (reduce + (map (comp f g) xs)) |
30.7 ms | 283.7 ms |
| 同上 | transducers | 19.7 ms | 214.1 ms |
| map と filter(要素数1,000,000、ベクタ) | (->> v (map f) (filter p) (reduce +)) |
13.5 ms | 140.4 ms |
| 同上 | transducers | 9.3 ms | 89.2 ms |
| Difference List(要素数40,000) |
(doall (concat acc '(1))) の繰り返し |
39,024.8 ms | 45,795.6 ms |
| 同上 | Difference List | 1.4 ms | 8.8 ms |
いずれの測定でも、書き方どうしの結果は一致しました。
倍率だけを取り出すと、次のようになります。
| 測定 | JVM の倍率 | babashka の倍率 |
|---|---|---|
| 手で融合 | 1.19倍 | 1.23倍 |
| transducers(map を2回) | 1.85倍 | 1.63倍 |
| transducers(map と filter) | 1.45倍 | 1.57倍 |
専任講師:
絶対値は、JVM 上のほうがおよそ10分の1になりました。しかし、倍率の傾向は変わりませんでした。
タロウくん:
それなら、1つ目の理由のほうが大きい、ということですか。
専任講師:
そう考えられます。ただし、その理由づけ自体は測定していません。断定はしません。
6-3 Clojure でも、Difference List は大きく効く
同じ Clojure で、Difference List を測ると、結果が変わります。
| 処理系 | 左結合の連結(要素数40,000) | Difference List | 倍率 |
|---|---|---|---|
| JVM 上の Clojure | 39,024.8 ms | 1.4 ms | 27,875倍 |
| babashka | 45,795.6 ms | 8.8 ms | 5,204倍 |
第4章と第5章で見たとおりです。中間データを削る手法は、言語や処理系の事情に左右されます。計算量そのものを変える手法は、どこでも大きく効きます。
動的型付けの言語でも、この区別は変わりません。
6-4 Common Lisp:loop マクロが中間リストをゼロにする
Common Lisp で mapcar の手動融合を測りました。要素数は4,000,000、5回測定した中央値です。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
(reduce #'+ (mapcar #'f (mapcar #'g xs))) |
112.0 ms | 84.0 ms | 148.0 ms |
(reduce #'+ (mapcar (lambda (x) (f (g x))) xs)) |
68.0 ms | 56.0 ms | 76.0 ms |
(loop for x in xs sum (f (g x))) |
12.0 ms | 8.0 ms | 12.0 ms |
3つすべての結果は一致しました。loop を使った書き方が、融合なしの9.3倍速くなりました。
タロウくん:
先生、loop が飛び抜けて速いです。
専任講師:
loop は、中間リストを1本も作らないからです。
mapcar を2回使うと、中間リストが1本できます。手で融合すると1本減ります。loop を使うと、ゼロになります。
タロウくん:
これも圏論の法則による書き換えなのでしょうか。
専任講師:
いいえ。loop はマクロです。コンパイル時に、繰り返しのコードへ展開されます。
Functor 則も自由定理も使っていません。同じ目的を、言語機能の側から達成している例です。
Common Lisp には、コンパイラマクロという仕組みもあります。
Common Lisp in particular offers unique features to optimize those parts of the code which really need to be as fast as possible. This includes so-called compiler macros, which can transform function calls into more efficient code at runtime, and a mandatory disassembler.
筆者による日本語訳:
とくに Common Lisp は、本当に可能なかぎり速くする必要があるコード部分を最適化するための独自の機能を提供する。これには、関数呼び出しを実行時により効率的なコードに変換できるコンパイラマクロと、必須とされる逆アセンブラが含まれる。
出典:
"The Machine that Builds Itself: How the Strengths of Lisp Family Languages Facilitate Building Complex and Flexible Bioinformatic Models"
https://arxiv.org/pdf/1608.02621
専任講師:
コンパイラマクロは、GHC の RULES と発想が近いものです。関数呼び出しを、より効率的なコードに書き換えます。
ただし、決定的な違いがあります。型にもとづく保証がありません。書き換えが正しいかどうかは、書いたプログラマの責任です。
6-5 Common Lisp では、型を宣言すると10倍速くなる
Common Lisp は動的型付けの言語ですが、プログラマが型を宣言できます。その効果を測りました。
要素数5,000,000の配列を10回走査した合計時間です。5回測定した中央値を示します。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
| 型宣言なし | 216.0 ms | 216.0 ms | 220.0 ms |
(declare (type (simple-array fixnum (*)) v)) (optimize (speed 3) (safety 0)) |
20.0 ms | 16.0 ms | 24.0 ms |
両者の結果は一致しました。10.8倍の差が出ました。
タロウくん:
先生、動的型付けの言語なのに、型を書くと速くなるのですね。
専任講師:
はい。プログラマが型を宣言すれば、コンパイラはそれを使って最適化します。
本連載の4軸でいえば、「型理論」の軸に○が付かない言語でも、言語機能として型宣言を持てば、型にもとづく最適化の一部を得られる、ということです。
タロウくん:
それなら、Haskell と同じことができるのではないですか。
専任講師:
いいえ。決定的な違いがあります。
この型宣言は検査されません。(safety 0) を指定すると、宣言が誤っていても、実行時に検出されません。
タロウくん:
誤った宣言を書いたら、どうなるのですか。
専任講師:
何が起きるかは分かりません。誤った結果を返すかもしれませんし、異常終了するかもしれません。
Haskell の型検査とは、性質が異なります。Haskell では、型が合わなければコンパイルが通りません。Common Lisp では、プログラマが責任を負います。
速度を得る代わりに、保証を手放している、ということです。
6-6 Erlang:コンパイラは内部で型を推論している
Erlang も動的型付けの言語です。まず、lists:map の手動融合を測りました。要素数は2,000,000、5回測定した中央値です。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
lists:map(f, lists:map(g, Xs)) |
201.7 ms | 195.3 ms | 443.7 ms |
lists:map(fun(X) -> f(g(X)) end, Xs) |
110.0 ms | 68.0 ms | 118.5 ms |
[f(g(X)) || X <- Xs] |
100.0 ms | 60.7 ms | 106.3 ms |
3つすべての結果は一致しました。リスト内包表記が、融合なしの2.0倍速くなりました。
Difference List も測りました(要素数40,000)。
| 書き方 | 中央値 |
|---|---|
Acc ++ [1] の繰り返し |
3,503.4 ms |
| Difference List | 2.2 ms |
両者の結果は一致しました。1,592倍の差が出ました。ここまでは、ほかの言語と同じ構図です。
ここからが、Erlang に特有の話題です。
Erlang/OTP 25 では、コンパイラが型情報を BEAM ファイルに埋め込み、JIT がそれを使うようになりました。
In OTP 25, the compiler was updated to embed type information in the BEAM file and the JIT was extended to emit better code based on that type information.
筆者による日本語訳:
OTP 25 では、コンパイラが BEAM ファイルに型情報を埋め込むよう更新され、JIT がその型情報にもとづいてより良いコードを生成するよう拡張された。
If the type of the operands are known to be integers sufficiently small making overflow impossible, the JIT needs to emit only 5 native instructions for the addition.
筆者による日本語訳:
オペランドの型が、桁あふれが起こりえないほど小さな整数であると分かっていれば、JIT が加算のために生成するネイティブ命令は5個で済む。
出典:
Erlang/OTP 公式ブログ「More Optimizations in the Compiler and JIT」
https://www.erlang.org/blog/more-optimizations/
6-7 最初の測定で、公式ブログと逆の結果が出た
この記述を実機で確かめようとしました。1,000,000回の加算を行い、5回測定した中央値です。
| 書き方 | 中央値 | 最小 | 最大 |
|---|---|---|---|
| 型が分からない加算 | 10.0 ms | 10.0 ms | 10.2 ms |
| 型と範囲が既知の加算(ガードで小整数を示す) | 11.8 ms | 11.8 ms | 12.0 ms |
型と範囲を示したほうが、1.18倍遅くなりました。公式ブログの記述と、逆向きの結果です。
タロウくん:
先生、公式ブログの記述が誤っているのでしょうか。
専任講師:
そう結論する前に、確かめるべきことがあります。
公式ブログが述べているのは、JIT が生成する命令数です。実行時間の話ではありません。測っているものが違う可能性があります。
そこで、命令数そのものを確かめました。
Erlang/OTP 25 の JIT は、+JDdump true を指定して起動すると、生成したネイティブコードをファイルに書き出します。3つの関数について、加算の部分の命令を数えました。
| 関数 | 定義 | 加算の部分の命令数 |
|---|---|---|
add_generic |
X + Y |
14 |
add_small |
ガードで X、Y が小さな整数であることを示し、X + Y
|
5 |
add_band |
(X band 16#3FF) + (Y band 16#3FF) |
5 |
型が分からない加算では、2つの値が小さな整数かどうかの検査と、桁あふれの検査が入り、14命令になりました。
型と範囲が分かっている加算では、どちらの検査も省かれ、5命令になりました。JIT の出力には、「add without overflow check」という注記が付いていました。
公式ブログの「14命令から5命令に減る」という記述と、完全に一致しました。
さらに、ガードを書かなくても、band の結果からコンパイラが型と範囲を推論し、5命令の加算を生成することも確かめられました。
6-8 なぜ最初の測定で遅くなったのか
JIT の出力を見ると、理由が分かりました。
add_small は、加算を5命令に減らす代わりに、ガードのために band を2回と比較を2回、余分に実行していました。
最初の測定では、このガードの負担が、加算で節約した分を上回ったのです。
そこで、band の処理を両方に同じだけ持たせ、加算の部分だけが違う形で測り直しました。1,000万回の繰り返しを7回測定した中央値です。
| 書き方 | 加算の命令数 | 中央値 | 最小 | 最大 |
|---|---|---|---|---|
呼び出し側で band し、関数の中では型が分からない加算を行う |
14 | 109.9 ms | 109.3 ms | 110.4 ms |
関数の中で band し、型が推論された加算を行う |
5 | 103.1 ms | 102.6 ms | 103.7 ms |
両者の結果は一致しました。型が推論された側が1.07倍速くなりました。公式ブログの記述どおりの向きです。
差が小さいのは、ループ全体の処理のうち、加算が占める割合が小さいためです。
タロウくん:
先生、最初の測定は、何が間違っていたのですか。
専任講師:
公式ブログの記述は正しかったのです。最初の結果が逆になったのは、測定の方法が、ガードという別の負担を持ち込んでいたためです。
命令数が減ることと、実行時間が短くなることは、別のことです。
タロウくん:
文献に書いてあることを実機で確かめるときは、何を測っているのかを合わせないといけないのですね。
専任講師:
よい整理です。本稿の測定を読むときにも、同じ注意が必要です。
6-9 動的型付けの言語でも、処理系は型を使っている
この追試は、本章にとって示唆的です。
Erlang は動的型付けの言語です。プログラマは型シグネチャを書きません。
しかし、コンパイラは内部で型を推論し、最適化に使っています。
本連載の4軸でいえば、「型理論」の軸に○が付かない言語でも、処理系の内部では型の情報が使われている、ということです。
ただし、これは圏論の知見にもとづく最適化ではありません。表Bの判定は変わりません。
同じことが、Common Lisp の型宣言(6-5)と、Erlang の型推論(6-7)に共通しています。動的型付けの言語でも、型の情報があれば速くなります。しかし、その型は、自由定理を導くための型ではありません。
6-10 副作用があると、融合で結果が変わる
本章の最後に、動的型付けの言語に共通する、重要な制約を扱います。
f と g が、呼ばれるたびに画面に1文字を出す関数であるとき、map f (map g [1, 2, 3]) と map (f . g) [1, 2, 3] を比べました。
| 言語 | 融合しない書き方の出力 | 融合した書き方の出力 | 返す値 |
|---|---|---|---|
| OCaml | gggfff | gfgfgf | 一致 |
| Standard ML | gggfff | gfgfgf | 一致 |
| F# | gggfff | gfgfgf | 一致 |
| Scala | gggfff | gfgfgf | 一致 |
| Erlang | gggfff | gfgfgf | 一致 |
| Common Lisp | gggfff | gfgfgf | 一致 |
| Clojure(リストを入力) | gfgfgf | gfgfgf | 一致 |
| Clojure(ベクタを入力) | gggfff | 測定せず | 一致 |
純粋でない7言語すべてで、返す値は同じでも、副作用が起きる順序が変わりました。
タロウくん:
先生、返す値が同じなら、問題ないのではないですか。
専任講師:
返す値だけを見れば、そうです。しかし、画面への出力、ファイルへの書き込み、データベースの更新などが絡むと、順序が変わることは重大な違いになります。
第3章の表Bで、いくつかの手法を「条件付き」とし、条件を「関数に副作用がないことをプログラマが保証する必要がある」としました。この測定が、その裏づけです。
タロウくん:
Clojure だけ、結果が違いますね。
専任講師:
よく見ています。Clojure では、融合しない書き方の出力が、入力の型によって変わりました。
リストを入力にすると gfgfgf、ベクタを入力にすると gggfff です。lazy sequence の作られ方が、入力の型によって違うためと考えられます。
副作用の順序が入力の型にも左右されるという点で、Clojure では条件がさらに厳しくなります。
6-11 純粋な言語では、そもそも書けない
同じ関数を Haskell と PureScript で書こうとすると、型が合わず、コンパイルが通りませんでした。
| 言語 | コンパイラの出力 |
|---|---|
| Haskell(GHC 9.4.7) | Couldn't match expected type Int' with actual type IO Int' |
| PureScript(0.15.16) | Could not match type(TypesDoNotUnify) |
タロウくん:
先生、コンパイルが通らないのは、不便ではないですか。
専任講師:
見方を変えてください。危険な書き換えを、型が事前に止めているのです。
純粋な言語では、副作用を持つ関数は型が変わります。Haskell では IO Int、PureScript では Effect Int になります。
したがって、Int -> Int の関数どうしを融合しても、副作用の順序が変わることはありません。そもそも、Int -> Int の関数に副作用を書けないからです。
タロウくん:
だから、GHC は安心して自動で書き換えられるのですね。
専任講師:
そういうことです。よい整理です。
第1章で述べた「圏論が出すのは、書き換えてよいという許可である」という論点と、つながっています。純粋であることが型で保証されていれば、その許可を、コンパイラが機械的に使えます。
動的型付けの言語では、その保証がありません。だから、同じ書き換えをプログラマが自分の責任で行う必要があります。
6-12 本章のまとめ
動的型付けの3言語で分かったことを整理します。
| 言語 | 中間データを消す手段 | 型の情報は使われているか |
|---|---|---|
| Clojure | transducers(関数合成だけで成り立つ) | 使っていない |
| Common Lisp |
loop マクロ、コンパイラマクロ |
プログラマが宣言すれば使われる。ただし検査されない |
| Erlang | リスト内包表記 | コンパイラが内部で推論し、JIT が使う |
3つの言語に共通するのは、次の2点です。
1つ目。中間データを消す目的は達成されている。ただし、手段は型ではなく、言語機能やライブラリです。
2つ目。副作用がないことの保証は、プログラマの責任である。純粋な言語のように、型が事前に止めてはくれません。
次の第7章では、もう一度、非正格評価の言語に戻ります。Clean を取り上げ、非正格のまま、別の言語機能を見るとどうなるかを扱います。Clean は、コンパイラが融合を行う数少ない言語のひとつであり、一意型という独自の仕組みを持っています。
第7章 非正格のまま別の言語機能を見る:Clean
第6章までで、評価戦略の軸(第4章)、言語機能の軸(第5章)、型付けの軸(第6章)を、順に動かしてきました。
本章では、もう一度、非正格評価の言語に戻ります。取り上げるのは Clean です。
Clean は、次の点で、本稿のほかのどの言語とも違います。
| 特徴 | 内容 |
|---|---|
| 評価戦略 | 既定では遅延評価。! で正格性を注釈できる |
| 型クラス | ある。Haskell と同様、dictionary passing に解決される |
| コンパイラによる融合 | ある。Clean 2.0 のコンパイラに融合アルゴリズムが実装されている |
| 独自の機能 | 一意型(uniqueness type)。破壊的更新を可能にする |
タロウくん:
先生、表にある dictionary passing とは、何でしょうか。
専任講師:
型クラスを、コンパイラがどう実現するかの方式です。
show のような型クラスの関数を呼ぶと、コンパイラは「この型の show は、この中身を使う」という対応表を、隠れた引数として関数に渡します。この対応表を辞書(dictionary)と呼び、渡す方式を dictionary passing と呼びます。
タロウくん:
書いていない引数が、裏で渡されているのですね。
専任講師:
そうです。だから型クラスは、実行時にわずかな費用がかかります。ただし、多くの場合はコンパイラがその費用を取り除きます。
Haskell も Clean も、同じ方式です。この点で、2つの言語は同じ土俵にあります。
Haskell 以外で、コンパイラが融合を行う言語は、本稿で扱う11の関数型言語のうち Clean だけです。
第5章で見たとおり、OCaml は Flambda を有効にしても融合を行いませんでした。第6章の3言語も、融合はライブラリか、プログラマの手によるものでした。
7-1 Clean を動かすまで
Clean の処理系を用意するには、少し手間がかかりました。同じことを試す読者のために、たどった道筋を書いておきます。
まず、GitHub 上に Clean コンパイラのソースコードのミラーがあります。ただし、フロントエンドを構成する70のファイルは、いずれも Clean 自身で書かれた .icl ファイルです。これをビルドするには、すでに動作する Clean コンパイラが必要でした。
そこで、GitHub で配布されている、Windows 版の Clean を Wine で動かすためのアプリを使いました。この中に、Windows 版の Clean 3.1(64ビット)一式が入っています。これを取り出し、Linux 上の Wine 9.0 で動かしました。
出典:
harcokuppens/CleanIDE-wine-app-MacOS(GitHub)
https://github.com/harcokuppens/CleanIDE-wine-app-MacOS
出典:
harcokuppens/clean-classic-helloworld(GitHub)
https://github.com/harcokuppens/clean-classic-helloworld
| 項目 | 内容 |
|---|---|
| 処理系 | Clean 3.1(Windows 版、64ビット)。CleanCompiler64.exe、CodeGenerator.exe、StaticLinker.exe、cpm.exe |
| 実行環境 | Wine 9.0 |
| 測定の方法 | プログラム全体の実行時間を外部から測った |
| Wine の起動時間 |
Start = 0 のプログラムの実行に57 msかかった。以下の値は、この57 msを差し引いたもの |
この測定は、Linux 上のネイティブの Clean ではなく、Wine の上で動く Windows 版です。ほかの言語の測定と、実行環境が異なります。この点を踏まえて、値をお読みください。
7-2 Clean のコンパイラは、本当に融合を行う
Clean 2.0 のコンパイラに融合アルゴリズムが実装されていることは、論文に書かれています。
The extended fusion algorithm is able to deal with standard deforestation, but also with higher-order function removal and dictionary elimination. We have implemented this extended algorithm in the Clean 2.0 compiler.
筆者による日本語訳:
拡張された融合アルゴリズムは、標準的な deforestation に加え、高階関数の除去や辞書の除去も扱える。この拡張アルゴリズムを Clean 2.0 コンパイラに実装した。
出典:
A. Alimarine, S. Smetsers, "Improved Fusion for Optimizing Generics", IFL 2002, LNCS 2670, Springer, pp. 51–67
doi: 10.1007/3-540-44854-3_4
https://link.springer.com/chapter/10.1007/3-540-44854-3_4
これを実機で確かめました。Clean のプロジェクトには、コンパイラの融合を有効にするか無効にするかの設定があります。要素数10,000,000で測り、5回測定した中央値から Wine の起動時間を差し引いた値を示します。
| 書き方 | 融合を無効 | 融合を有効 |
|---|---|---|
標準ライブラリの map を2回 |
187 ms | 203 ms |
標準ライブラリの map で手で融合 |
110 ms | 112 ms |
同じモジュールで定義した map を2回 |
199 ms | 99 ms |
同じモジュールで定義した map で手で融合 |
119 ms | 100 ms |
すべての書き方で、結果は一致しました。
タロウくん:
先生、同じモジュールで定義した map だけ、融合を有効にすると2倍速くなっています。
専任講師:
そこが、この測定の要点です。
同じモジュールで定義した map では、コンパイラの融合によって2.0倍速くなり、手で融合した場合と同じ水準になりました。文献の記述を、実機で確かめられました。
タロウくん:
標準ライブラリの map には、効いていませんね。
専任講師:
はい。標準ライブラリはあらかじめコンパイルされており、コンパイラが map の定義を見られないためと考えられます。ただし、この理由は確かめていません。
タロウくん:
すると、Clean で融合の恩恵を受けるには、自分のモジュールに map を定義し直す必要があるのでしょうか。
専任講師:
この測定の範囲では、そうなります。
ここは、GHC との違いとして重要です。GHC は、標準ライブラリの map に RULES プラグマを書いてあるので、利用者が何もしなくても融合が効きます。
なお、Clean で融合を有効にするには、プロジェクト全体の設定だけでなく、モジュールごとの設定も書き換える必要がありました。モジュールごとの設定は、最初のビルドのときに作られます。同じことを試す読者のために、書き添えておきます。
7-3 Clean では、rank-2 type を書ける
初回記事の第4章で扱った foldr/build の書き換えには、rank-2 type が必要です。
Clean では、全称量化を A.b: という書き方で表します。次のように書きました。
build :: (A.b: (a b -> b) b -> b) -> [a]
コンパイルと実行に成功しました。要素数1,000,000で測り、7回測定した中央値から Wine の起動時間を差し引いた値を示します。
| 書き方 | 融合を無効 | 融合を有効 |
|---|---|---|
foldr c 0 (build g) |
70 ms | 18 ms |
g c 0(規則を手で適用) |
98 ms | 17 ms |
融合を有効にすると、どちらの書き方も約18 msになりました。文献にある、Clean の融合が高階関数の除去も行うという記述と整合します。
融合を無効にしたとき、規則を手で適用した書き方のほうが遅くなりました。理由は確かめていません。
7-4 Codensity と Traversable も書けた
Clean には型クラスがあるため、初回記事で扱ったほかの手法も書けます。
Codensity(10-5)
rank-2 type を持つデータ構築子を、次のように書きました。
:: C a = C (A.r: (a -> Free r) -> Free r)
コンパイルと実行に成功しました。
| n | 素朴な書き方 | Codensity を経由 | 結果の一致 |
|---|---|---|---|
| 3,000 | 66 ms | 1 ms 未満 | 一致 |
| 6,000 | 262 ms | 1 ms 未満 | 一致 |
| 12,000 | 1,060 ms | 1 ms 未満 | 一致 |
素朴な書き方は、n が2倍になるたびに所要時間が約4倍になっています。2乗に伸びています。
Codensity を経由した書き方の所要時間は、Wine の起動時間のばらつきの範囲に収まり、区別できませんでした。
Traversable(10-2)
type constructor class として Applicative と Traversable を定義し、リストについての汎用の traverse を書きました。コンパイルと実行に成功しました。
2回の走査を1回にまとめる効果は、リストと Opt(Maybe にあたる型)に固定した traverse で測りました。要素数は1,000,000です。
| 書き方 | 所要時間 |
|---|---|
| 2回の走査 | 198 ms |
| 1回にまとめる | 177 ms |
結果は一致しました。1.12倍であり、ほかの言語より差が小さくなりました。理由は確かめていません。
そのほかの手法
| 手法 | 確かめた内容 | 結果 |
|---|---|---|
| 10-1 foldMap | Monoid を型クラスとして定義し、foldMap を書いた | 実行に成功した(110) |
| 10-3 bind の再結合 | 左結合と右結合の bind が同じ値になるかを確かめた | 一致した |
| 10-4 Difference List(要素数40,000) | 左結合の ++ の繰り返しと比較 |
12,459 ms が 1 ms 未満になった |
| 10-6 全エラー集約 | エラーを集める検証を書いた | 名前と年齢の2つのエラーを両方とも集めた |
これで、表Bの Clean の行の判定は、すべて実機で確かめられたことになります。
7-5 一意型:型が保証するから、破壊的に書き換えられる
Clean のもっとも特徴的な機能が、一意型です。
タロウくん:
先生、破壊的更新という言葉が出てきました。すでにある値を、そのまま書き換えてしまうことを指すのでしたか。
専任講師:
はい。すでにメモリにある値を、そのまま書き換えることです。
関数型言語は、ふつうこれをしません。新しい値を作って返します。配列の1要素を変えたいときも、配列全体を写してから、写したほうを変えます。
タロウくん:
それは、遅くなりそうですね。
専任講師:
そのとおりです。この節で測るのは、まさにその差です。
Types in Clean may be unique, which means that they may not be shared. The uniqueness type system allows the compiler to generate efficient code because unique data structures can be destructively updated.
筆者による日本語訳:
Clean では型が一意でありうる。すなわち、その型の値が共有されないことを意味する。一意型システムにより、コンパイラは効率的なコードを生成できる。一意なデータ構造は破壊的に更新できるからである。
出典:
"Clean for Haskell Programmers"(2024年)
https://arxiv.org/pdf/2411.00037
出典:
E. Barendsen, S. Smetsers, "Uniqueness Typing for Functional Languages with Graph Rewriting Semantics", Mathematical Structures in Computer Science, 1996
実機で測りました。要素数10,000の配列の要素を、100,000回書き換えます。Wine の起動時間(57 ms)を差し引いた値を示します。
| 書き方 | 所要時間 | 結果 |
|---|---|---|
一意な配列(*{#Int})をその場で書き換える |
1 ms 未満 | 100000 |
| 共有されうる配列を、書き換えのたびに配列全体をコピーしてから書き換える | 614 ms | 100000 |
書き換えの回数が10,000回のときは、一意な配列で1 ms未満、コピーを伴う書き換えで68 msでした。
タロウくん:
先生、一意型というのは、何を保証するものなのですか。
専任講師:
その値が、ほかの場所から参照されていないことを保証します。
共有されていないことが保証されていれば、値をその場で書き換えても、ほかの場所から見た結果は変わりません。だから、コンパイラは安心して破壊的更新に変換できます。
タロウくん:
共有されている値を書き換えようとしたら、どうなるのですか。
専任講師:
コンパイラが止めます。実際に、一意な配列を2か所で使おうとしたところ、次のように拒否されました。
Uniqueness error [uniqbad.icl,4,bad]: "a" demanded attribute cannot be offered by shared object
タロウくん:
関数型言語なのに、値を書き換えてよいのですね。
専任講師:
書き換えても、外から見た振る舞いが変わらない場合に限って、書き換えています。
関数型言語が値を書き換えないのは、書き換えそのものが悪いからではありません。書き換えると、ほかの場所から見た値が変わってしまうからです。その心配がないことを型で保証できれば、書き換えてかまいません。
タロウくん:
型が保証するから、速くできる、ということですか。
専任講師:
そのとおりです。よい整理です。
これは、本連載の主題とまったく同じ構図です。第1章で述べたとおり、圏論の法則は「書き換えてよい」という許可を出します。一意型は、別の種類の保証によって、別の種類の書き換えの許可を出しています。
どちらも、型やその背後の理論が、最適化の根拠になっているという点で共通しています。
7-6 Clean は純粋な言語である
第6章の 6-10 で、副作用があると融合で順序が変わることを見ました。Clean はどうでしょうか。
Clean の標準ライブラリ(StdFile.dcl)では、画面への書き込みが次の型を持っています。
fwrites :: !{#Char} !*File -> *File
書き込むには *File 型の値が必要です。その値は、次の関数によって、一意な環境から取り出すしかありません。
stdio :: !*f -> (!*File,!*f)
したがって、Int -> Int の関数は環境を受け取らないため、画面に書き込めません。
タロウくん:
先生、これは Haskell の IO と同じ考え方でしょうか。
専任講師:
目的は同じです。副作用を持つ関数の型を、純粋な関数と区別しています。
ただし、手段が違います。Haskell は IO というモナドで包みます。Clean は、一意な環境の値を引き回すという形で表します。
タロウくん:
どちらでも、Int -> Int の関数に副作用を書けないのですね。
専任講師:
そうです。だから、第3章の表Bで Clean を純粋な言語として扱い、副作用に関する条件を付けませんでした。その根拠を、標準ライブラリの型で確かめたことになります。
7-7 GHC の融合との対比
Clean の融合と、GHC の融合を比べておきます。
| 項目 | GHC | Clean |
|---|---|---|
| 融合の仕組み | RULES プラグマによる書き換え規則。標準ライブラリに記述済み | コンパイラの融合アルゴリズム |
| 標準ライブラリの関数に効くか | 効く | この測定では効かなかった |
| 利用者が自分で書く必要 | ない | 同じモジュールに定義し直す必要があった |
| 扱える範囲 | 書き換え規則として書いたもの | 標準的な deforestation、高階関数の除去、辞書の除去 |
なお、GHC の融合の効果については、次の報告があります。
fusion technique of the Glasgow Haskell Compiler (GHC), which only works for call-by-need programs, had an average speedup of 6.5%.
筆者による日本語訳:
Glasgow Haskell Compiler(GHC)の融合技法は、call-by-need のプログラムにのみ機能し、平均6.5%の高速化であった。
出典:
Y. Chen, L. Parreaux, "The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures", 2024年
https://arxiv.org/pdf/2410.02232
この「平均6.5%」という数字は、実際のプログラム群を対象に測った平均です。本稿の測定で得た「map を2回書いたときに4.6倍」という数字とは、測っている対象が違います。
特定の書き方に絞れば大きな差が出ますが、プログラム全体では、融合が効く箇所は限られる、ということです。この点は、第11章の「本稿の限界」でも、もう一度触れます。
7-8 本章のまとめ
Clean を見て分かったことを整理します。
| 観測したこと | 結果 |
|---|---|
| コンパイラによる融合 | 同じモジュールで定義した map で2.0倍。手で融合した場合と同じ水準。標準ライブラリの map には効かなかった |
| rank-2 type | 書ける(A.b: の記法)。foldr/build、Codensity を実装できた |
| 型クラス | ある。foldMap、Traversable、全エラー集約を実装できた |
| 一意型による破壊的更新 | 614 ms が 1 ms 未満に。共有されうる値では、コンパイラが拒否する |
| 純粋であること | 標準ライブラリの型で確かめた。Int -> Int の関数に副作用を書けない |
Clean は、Haskell 以外で、本稿の手法をほぼすべて書ける唯一の言語でした。非正格評価、型クラス、rank-2 type、コンパイラによる融合という条件が、すべてそろっているためです。
そのうえで、一意型という、Haskell にはない保証の仕組みを持っています。
次の第8章では、言語ごとの記述を離れ、横断で見ます。条件をそろえて測った表を示し、Codensity、Traversable、foldr/build の3つの手法を、11の関数型言語にまたがって比べます。
第8章 横断で見る:条件をそろえた表と、3つの手法
第4章から第7章まで、言語ごとに見てきました。本章では、言語の枠を外し、手法ごとに横断して見ます。
第3章までの表は、「その手法を書けるか」を示すものでした。本章の表は、「書いたとき、どれだけ効くか」を示します。
本章で比べる2種類の手法を、図に示します。
8-1 条件をそろえて測り直した
第4章から第7章までの測定は、言語によって要素数が異なっていました。処理系の速さや、スタックの制約が違うためです。
そのままでは、倍率を言語のあいだで比べられません。そこで、条件をそろえて測り直しました。
| 測定 | 要素数 |
|---|---|
| map の手動融合 | 2,000,000 |
| Difference List | 40,000 |
Haskell も、同じ条件で測りました。GHC 9.4.7 で -O2 を指定し、書き換え規則を有効にした場合と、-fno-enable-rewrite-rules で無効にした場合の両方を測っています。
8-2 map の手動融合:効き方は評価戦略で決まる
要素数2,000,000での結果です。
| 言語 | 評価戦略 | 融合なし | 手で融合 | 倍率 |
|---|---|---|---|---|
| Scala | 正格 | 456.0 ms | 111.4 ms | 4.09倍 |
| PureScript | 正格 | 1,042.6 ms | 454.5 ms | 2.29倍 |
| OCaml | 正格 | 540.3 ms | 266.7 ms | 2.03倍 |
| F# | 正格 | 357.8 ms | 184.2 ms | 1.94倍 |
| Erlang | 正格 | 201.7 ms | 110.0 ms | 1.83倍 |
| Haskell(書き換え規則なし) | 非正格 | 49.5 ms | 28.2 ms | 1.76倍 |
| Standard ML | 正格 | 152.1 ms | 87.1 ms | 1.75倍 |
| Common Lisp | 正格 | 56.0 ms | 36.0 ms | 1.56倍 |
| Haskell(書き換え規則あり) | 非正格 | 10.7 ms | 8.2 ms | 1.30倍 |
| Clojure | 正格(lazy sequence) | 349.5 ms | 283.7 ms | 1.23倍 |
| Miranda | 非正格 | 877 ms | 839 ms | 1.05倍 |
Common Lisp の測定の分解能は4ミリ秒です。
タロウくん:
先生、表の下のほうに、非正格の言語と Clojure が集まっています。
専任講師:
よく見ています。この表の並びが、本稿の結論のひとつです。
map の融合がどれだけ効くかは、評価戦略で決まります。
正格評価の言語では、手で融合すると1.56倍から4.09倍速くなりました。中間リストの全体がメモリに作られるためです。
遅延評価の Miranda と、lazy sequence を使う Clojure では、差が小さくなりました。中間リストの要素が1つずつ作られ、すぐに消費されるためです。
タロウくん:
Haskell は、2か所に出てきますね。
専任講師:
書き換え規則を有効にした場合と、無効にした場合です。
無効にすると1.76倍になり、ほかの言語で手で融合したときの差と、ほぼ同じ大きさになりました。有効にすると1.30倍まで縮みます。
タロウくん:
縮むのは、なぜですか。
専任講師:
GHC がすでに書き換えているからです。プログラマが手で書き換える余地が、もう残っていません。
絶対値を見てください。map f (map g xs) と書いたコードが、規則を無効にすると49.5 msですが、有効にすると10.7 msになります。4.6倍です。この4.6倍が、プログラマが手で書き換えなくても GHC が代わりに書き換えた分です。
なお、リストの生成も時間に含めた測定では、書き換え規則を有効にすると2つの書き方がどちらも5.0 msになりました。GHC が、リストの生成まで含めて1つのループにまとめたためです。規則を無効にすると52.0 msと31.7 msでした。
8-3 Difference List:どの言語でも桁違いに効く
要素数40,000での結果です。
| 言語 | 評価戦略 | 型付け | 左結合の連結 | Difference List |
|---|---|---|---|---|
| Clojure | 正格 | 動的 | 45,795.6 ms | 8.8 ms |
| F# | 正格 | 静的 | 31,680.7 ms | 1.3 ms |
| Miranda | 非正格 | 静的 | 27,219 ms | 23 ms |
| OCaml | 正格 | 静的 | 23,390.6 ms | 0.8 ms |
| PureScript | 正格 | 静的 | 18,396.5 ms | 9.5 ms |
| Haskell | 非正格 | 静的 | 15,107.8 ms | 0.2 ms |
| Standard ML | 正格 | 静的 | 11,989.0 ms | 0.3 ms |
| Scala | 正格 | 静的 | 4,024.3 ms | 9.2 ms |
| Erlang | 正格 | 動的 | 3,503.4 ms | 2.2 ms |
| Common Lisp | 正格 | 動的 | 3,504.0 ms | 4 ms 未満 |
10言語すべてで、Difference List のほうが桁違いに速くなりました。
倍率を書いていないのは、意図があります。Difference List の所要時間は1ミリ秒前後と小さく、測定の分解能の影響を受けます。倍率を細かく比べることに、意味がありません。
なお、Haskell では、書き換え規則を無効にしても結果はほぼ同じでした(15,052.1 msと0.2 ms)。Difference List は、コンパイラが自動で行う最適化ではなく、プログラマが書き方を選ぶ最適化だからです。
8-4 2つの表が示すこと
2つの表を並べると、本稿の中心的な論点が見えます。
| 手法 | 何を削るか | 何に依存するか |
|---|---|---|
| map の融合 | 中間リストを作る費用 | 評価戦略に強く依存する。1.05倍から4.09倍 |
| Difference List | 計算量そのもの(O(n²) を O(n) に) | 依存しない。10言語すべてで桁違い |
タロウくん:
先生、同じ「圏論の知見から導かれた最適化」なのに、性質がまったく違うのですね。
専任講師:
そこが重要です。
初回記事では、どちらも圏論の法則から導かれる書き換えとして扱いました。Functor 則からの融合と、Cayley 表現からの Difference List です。
しかし、どの軸に依存するかは、手法ごとに違います。
タロウくん:
使う前に、その手法がどの軸に依存するかを知っておく必要がありますね。
専任講師:
そのとおりです。よい整理です。
言語を選ぶとき、あるいは既存のコードを速くしようとするとき、「この手法は、自分の言語で効くのか」を見極める材料になります。
8-5 Codensity:4つの言語で、2乗が消えた
初回記事の看板となった Codensity を、横断で測りました。
Free モナドで bind を左結合に n 回重ね、素朴な書き方と、Codensity を経由する書き方を比べます。関手は、1つ先に進むだけの Tick に固定しました。
| 言語 | n | 素朴な書き方 | Codensity を経由 | 結果の一致 |
|---|---|---|---|---|
| OCaml | 3,000 | 0.0100 s | 0.000029 s | 一致 |
| OCaml | 6,000 | 0.0512 s | 0.000139 s | 一致 |
| OCaml | 12,000 | 0.2297 s | 0.000571 s | 一致 |
| Scala | 3,000 | 0.0190 s | 0.000185 s | 一致 |
| Scala | 6,000 | 0.0735 s | 0.000300 s | 一致 |
| Scala | 12,000 | 0.3182 s | 0.000353 s | 一致 |
| PureScript | 3,000 | 0.0814 s | 0.0024 s | 一致 |
| PureScript | 6,000 | 0.3885 s | 0.0013 s | 一致 |
| PureScript | 12,000 | 1.8351 s | 0.0072 s | 一致 |
| Haskell(参考) | 3,000 | 0.0427 s | 0.000021 s | 一致 |
| Haskell(参考) | 6,000 | 0.1997 s | 0.000041 s | 一致 |
| Haskell(参考) | 12,000 | 0.8968 s | 0.000074 s | 一致 |
素朴な書き方は、n が倍になるたびに、所要時間がおよそ4倍から5倍に伸びました。n の2乗に近い伸び方です。
Codensity を経由した書き方の伸び方を、n を大きくして確かめました。
| 言語 | n = 100,000 | n = 200,000 | n = 400,000 | n = 800,000 |
|---|---|---|---|---|
| OCaml | 0.0094 s | 0.0242 s | 0.0678 s | 0.1563 s |
| Scala | 0.0093 s | 0.0378 s | 0.0728 s | 0.1542 s |
| Haskell(参考) | 0.0012 s | 0.0060 s | 0.0145 s | 0.0310 s |
n が倍になるたびに、およそ2倍から3倍に伸びました。完全な比例ではありませんが、素朴な書き方の2乗に近い伸び方よりは、はるかに緩やかです。
比例から外れる分は、メモリの確保と回収の負担と考えられますが、確かめていません。
タロウくん:
先生、PureScript は n = 12,000 までしかありませんね。
専任講師:
n が12,000を超えると、JavaScript のスタックが尽きて異常終了しました。
Codensity は継続を n 段重ねるため、呼び出しの深さが n に比例します。PureScript は JavaScript にコンパイルされるので、JavaScript のスタックの制約を受けます。
タロウくん:
手法が使えても、実行環境の制約で限界があるのですね。
専任講師:
そういうことです。この種の制約は、表Bには現れません。実際に動かして初めて分かります。
8-6 rank-2 type を、別の仕組みで表す
Codensity を書くには rank-2 type が必要です。第3章で見たとおり、直接書けるのは Haskell、PureScript、Clean だけです。
OCaml と Scala では、どう書いたのでしょうか。
| 言語 | rank-2 type を表す仕組み |
|---|---|
| OCaml | polymorphic record field(レコードのフィールドに多相型を書く) |
| Scala | polymorphic method を持つ trait |
| F# | generic method |
| Clean | 全称量化の記法(A.b:) |
タロウくん:
先生、直接書けなくても、代わりの仕組みがあるのですね。
専任講師:
あります。ただし、書き方は変わります。
第3章の表Bで、Codensity を PureScript で「使える」、OCaml と Scala で「条件付き」としました。この「条件付き」の条件が、rank-2 type を別の仕組みで表す必要があるということです。
タロウくん:
条件を満たせば、効果は同じなのでしょうか。
専任講師:
この測定の範囲では、同じでした。2乗の伸びが消えています。
書き方が面倒になるだけで、得られる効果は変わりません。
なお、Haskell の倍率は、初回記事の測定(n が3,000のとき約3,300倍)とは異なります。測定の条件とコードが異なるためです。本稿では、同じ条件で測った4言語どうしを比べています。
測定の際、Haskell では GHC の最適化(full laziness)が、繰り返しの測定のあいだで計算結果を使い回すことがありました。-fno-full-laziness を付けて測り直した値を示しています。
8-7 Traversable:2回の走査を1回にまとめる
初回記事の 10-2 と同じ形で測りました。要素数1,000,000のリストに、失敗しうる処理を2回かけます。
traverse f xs のあとに traverse g を行う書き方と、traverse (\x -> f x >>= g) xs と1回にまとめる書き方を比べます。
| 言語 | 2回の走査 | 1回にまとめる | 倍率 | 結果の一致 |
|---|---|---|---|---|
| Scala | 282.6 ms | 57.8 ms | 4.89倍 | 一致 |
| OCaml | 113.5 ms | 56.9 ms | 1.99倍 | 一致 |
| Standard ML | 57.5 ms | 31.4 ms | 1.83倍 | 一致 |
| Haskell(参考) | 155.6 ms | 89.6 ms | 1.74倍 | 一致 |
| PureScript | 415.5 ms | 245.8 ms | 1.69倍 | 一致 |
すべての言語で、1回にまとめたほうが速くなりました。
OCaml、Standard ML、Scala、PureScript では、Traversable の汎用の仕組みではなく、リストと option(Maybe)に固定した traverse を書いて測りました。
汎用の仕組みで書けることは、別に確かめてあります。PureScript はライブラリのソースで、Standard ML はファンクタとしてのコンパイルで、Scala は Cats のソースで確認しました。
Haskell の倍率は、初回記事の測定(約4.5倍)とは異なります。測定の条件とコードが異なるためです。Haskell も -fno-full-laziness を付けて測りました。
8-8 foldr/build:規則を手で適用すると、大きく効く
build で作ったリストを foldr で畳み込む書き方と、規則 foldr c n (build g) = g c n を手で適用して g c n と直接書く書き方を比べました。要素数は1,000,000です。
| 言語 | foldr c 0 (build g) |
g c 0(規則を手で適用) |
倍率 | 結果の一致 |
|---|---|---|---|---|
| OCaml | 98.1 ms | 4.0 ms | 24.5倍 | 一致 |
| F# | 187.5 ms | 6.5 ms | 28.8倍 | 一致 |
| Scala | 221.5 ms | 32.5 ms | 6.82倍 | 一致 |
| PureScript(要素数10,000) | 3.0 ms | 0.7 ms | 4.3倍 | 一致 |
PureScript は、末尾再帰でない再帰の深さが JavaScript のスタックの制約を受けるため、要素数を10,000にしました。
Haskell は、GHC が自動で書き換える場合と、書き換え規則を無効にした場合を比べました。
| 言語 | 書き換え規則あり | 書き換え規則なし |
|---|---|---|
| Haskell(参考) | 19.8 ms | 26.9 ms |
タロウくん:
先生、OCaml と F# で20倍以上の差が出ています。map の融合より、ずっと大きいですね。
専任講師:
そうです。この規則は、中間リストを丸ごと1本、消すからです。
build g は、リストを作ります。foldr c 0 は、そのリストを読んで畳み込みます。規則を手で適用して g c 0 と書くと、リストを作らずに、直接畳み込みます。
タロウくん:
Haskell では、差が1.36倍しかありません。
専任講師:
GHC が、書き換え規則とは別の最適化でも中間リストの一部を取り除いている可能性があります。インライン展開などです。ただし、この理由は確かめていません。
タロウくん:
先生、この規則が正しいことは、どうやって保証されるのですか。
専任講師:
第3章の上級者向けコラムで扱ったとおり、rank-2 type とパラメトリシティです。
build の引数 g の型は forall b. (a -> b -> b) -> b -> b です。この型を持つ関数は、型 b の中身を調べられません。だから、(:) と [] を渡したときと、c と n を渡したときとで、同じ形の値を作ります。
タロウくん:
型が中身を隠しているから、規則が成り立つのですね。
専任講師:
そのとおりです。よい整理です。
第6章で見たとおり、動的型付けの言語では、この保証がありません。型の中身を調べる g を書けてしまい、規則が崩れます。
OCaml、Scala、F# では、rank-2 type を別の仕組みで表して build を書きました。表Bで、foldr/build をこの3言語で「条件付き」としたことと整合します。条件のうち「rank-2 type を別の仕組みで表す」ことは、実際に書いて確かめました。
8-9 3つの手法の横断まとめ
本章で測った3つの手法を、整理します。
| 手法 | 何を削るか | 効き方 | 必要なもの |
|---|---|---|---|
| Codensity | bind の左結合による2乗の伸び | 2乗が消える。n が大きいほど差が大きくなる | rank-2 type(直接、または代わりの仕組み) |
| Traversable | 2回の走査を1回に | 1.69倍から4.89倍 | higher-kinded type、または特定の型に固定 |
| foldr/build | 中間リストを1本 | 4.3倍から28.8倍 | rank-2 type とパラメトリシティ |
3つに共通するのは、次の2点です。
1つ目。Haskell の外でも成り立ちました。初回記事で Haskell を題材に扱った手法が、ほかの言語でも同じ向きに効きました。
2つ目。rank-2 type を直接書けない言語では、代わりの仕組みで表す必要がありました。書けるかどうかは、第3章の表Bのとおりです。
8-10 本章のまとめと、ここまでの整理
第4章から本章まで、11の関数型言語を4つの軸で見てきました。整理します。
| 軸 | 動かした章 | 分かったこと |
|---|---|---|
| 評価戦略 | 第4章 | map の融合の効き方が決まる。seq があれば恒等律が破れる。型クラスの有無は無関係 |
| 言語機能 | 第5章 | 融合をコンパイラが行うか、ライブラリが行うか、プログラマが行うかが決まる |
| 型付け | 第6章 | 手法の正しさを言語が保証するか、プログラマが保証するかが決まる |
| 4つがそろう場合 | 第7章 | Clean では、本稿の手法をほぼすべて書け、コンパイラも融合を行う |
| 手法ごとの横断 | 第8章 | 手法によって、どの軸に依存するかが違う |
次の第9章では、ここまでの測定を踏まえて、本稿の問いのひとつに答えます。
圏論の知識は、誰が持っている必要があるのか。
言語によって、答えが変わります。
第9章 誰が圏論の知識を使うのか
第8章までで、11の関数型言語の測定を並べました。本章では、その結果から、本稿の問いのひとつに答えます。
圏論の知識は、誰が持っている必要があるのか。
測定の結果を、担う主体ごとに図にまとめます。
9-1 同じ最適化でも、担う主体が違う
10の関数型言語で測ってみると、2回の map を1回にまとめるという同じ最適化でも、それを担う主体が言語によって違うことが分かりました。
圏論の知識が要ることは、どの言語でも変わりません。
違うのは、誰がその知識を使うかです。
| 誰が圏論の知識を使うか | 言語と仕組み | 実測で確かめたこと(要素数2,000,000) |
|---|---|---|
| コンパイラの作者 | Haskell(GHC の RULES プラグマ) | 書き換え規則を有効にすると、map f (map g xs) と記述したコードが 49.5 ms から 10.7 ms になった |
| コンパイラの作者 | Clean(コンパイラが融合を実装) | 同じモジュールで定義した map では、融合を有効にすると 199 ms が 99 ms になった(要素数10,000,000、Wine の上で測定)。標準ライブラリの map には効かなかった |
| ライブラリの作者 | Scala の view
|
融合なしの書き方の17.7倍速かった |
| ライブラリの作者 | F# の Seq
|
融合なしの書き方の5.3倍速かった |
| ライブラリの作者 | Scala の cats-free の Free
|
左結合に重なった bind を、内部で右結合に組み替えている(ソースで確認)。n が倍になっても所要時間はおよそ1.5倍から1.9倍の伸びにとどまった |
| 言語の設計者 | Clojure の transducers | 融合なしの書き方の1.63倍速かった |
| マクロの作者 | Common Lisp の loop
|
融合なしの書き方の約14倍速かった(測定の分解能は4ミリ秒) |
| プログラマ自身 | OCaml、Standard ML、PureScript、Erlang、F# の List、Scala の List、Common Lisp の mapcar
|
手で融合すると、1.56倍から4.09倍速くなった |
| 誰も使わなくてよい | Miranda(遅延評価) | 手で融合しても1.05倍にとどまった。中間リストの全体が、もともと作られない |
9-2 5つの主体
表の左の列を、順に見ていきます。
コンパイラの作者
Haskell では、GHC の作者が圏論の知識を使い、書き換え規則として標準ライブラリに書き込みました。
プログラマは、何も知らなくても、その恩恵を受けられます。map f (map g xs) と書けば、GHC が map (f . g) xs に書き換えます。
Clean でも、コンパイラが融合を行います。ただし第7章で見たとおり、この測定では標準ライブラリの map に効きませんでした。同じモジュールに定義し直す必要がありました。
ライブラリの作者
Scala の view や F# の Seq では、ライブラリの作者が、中間コレクションを作らない仕組みを用意しました。
プログラマは、view や Seq を挟むだけで済みます。
第5章で見た cats-free の Free も、この型です。ライブラリの作者が、左結合に重なった bind を右結合に組み替える処理を、内部に書いています。利用者は、結合律を知らなくても、恩恵を受けられます。
言語の設計者
Clojure の transducers は、言語の設計者が用意した仕組みです。
第6章で見たとおり、型を使わずに中間データを消します。プログラマは transduce と書くだけです。
マクロの作者
Common Lisp の loop は、マクロです。コンパイル時に、中間リストを作らない繰り返しのコードへ展開されます。
loop を書いた人が、中間リストを作らない展開を設計しました。
プログラマ自身
OCaml と Standard ML では、コンパイラはこの書き換えを行いません。
プログラマ自身が、「この2回の map は1回にまとめてよい」と判断し、自分で書き換える必要があります。
その判断を支えるのが、Functor 則という圏論の知識です。
9-3 誰も使わなくてよい場合もある
表の最後の行が、Miranda です。
Miranda では、遅延評価のため、中間リストの全体がもともと作られません。
この最適化に関しては、誰も圏論の知識を使う必要がありません。
タロウくん:
先生、それなら遅延評価の言語を使えばよいのではないですか。
専任講師:
この最適化に関しては、そう言えます。しかし、話はそこで終わりません。
第4章で見たとおり、遅延評価の言語でも、Difference List の効果は大きく残りました。Miranda で263倍です。
タロウくん:
計算量を変える最適化は、評価戦略では代わりが利かないのでしたね。
専任講師:
そのとおりです。よい整理です。
遅延評価は、中間データを作る費用を減らします。しかし、O(n²) を O(n) にはしません。
したがって、Miranda を使う人も、Difference List については、自分で圏論の知識(この場合は Cayley 表現の考え方)を使う必要があります。
タロウくん:
手法ごとに、担う主体が変わるのですね。
専任講師:
そうです。表は map の融合についてのものです。手法が変われば、表の中身も変わります。
9-4 初回記事の区別が、さらに細かく分かれた
初回記事の第10章では、GHC が自動で行う最適化と、プログラマが自分で行う最適化を区別しました。
10の関数型言語を並べると、その区別がさらに細かく分かれます。
| 初回記事の区別 | 本稿で分かれた主体 |
|---|---|
| コンパイラが自動で行う | コンパイラの作者、言語の設計者、マクロの作者 |
| プログラマが自分で行う | ライブラリの作者(利用者は呼ぶだけ)、プログラマ自身 |
タロウくん:
先生、「ライブラリの作者」が真ん中にあるのが、面白いですね。
専任講師:
そこが、本章でもっとも実務的な論点です。
view や Seq や transduce を書くプログラマは、圏論を知らなくても使えます。しかし、それを用意した人は知っている必要がありました。
タロウくん:
どちらの側にいるかで、必要な知識が変わるということですか。
専任講師:
そうです。そして、自分がどちらの側にいるかは、状況によって変わります。
社内で共通のライブラリを作る立場になれば、作者の側です。そのライブラリを使う立場なら、利用者の側です。
9-5 この整理が実務で持つ意味
タロウくん:
先生、この整理は、実務でどう役立つのでしょうか。
専任講師:
3つ挙げます。
1つ目。コードが遅いとき、どこを見ればよいかが分かります。
Haskell で map を2回書いて遅いなら、書き換え規則が効いていない理由を探します。OCaml で同じコードが遅いなら、自分で書き換えればよいだけです。原因の探し方が変わります。
2つ目。言語を移るとき、何が失われるかが分かります。
Haskell から OCaml へコードを移すとき、map を2回書いたコードは、そのままでは遅くなります。GHC が代わりにやっていたことを、自分でやる必要があるためです。
3つ目。ライブラリを選ぶ基準になります。
Scala で List を使うか view を使うか、Clojure で map を重ねるか transduce を使うか。この選択が性能に直結することを、あらかじめ知っていられます。
9-6 本章のまとめ
自分の使っている言語で、圏論の知識を使うのは誰なのか。
それを知っておくことが、最適化を運任せにしないための第一歩です。
| 自分の立場 | 必要な知識 |
|---|---|
| Haskell や Clean で、標準ライブラリを使うだけ | 知らなくても恩恵を受けられる。ただし、なぜ速いかは説明できない |
| Scala や F# や Clojure で、用意された仕組みを使う | どの仕組みがどの場面で効くかを知っている必要がある |
| OCaml や Standard ML で書く | Functor 則などの法則を、自分で適用する必要がある |
| 社内の共通ライブラリを作る | 法則の正しさを、自分で保証する必要がある |
| 動的型付けの言語で書く | 法則が成り立つ条件を、言語が検査してくれない。自分で保証する必要がある |
最後の行が、第6章で見た論点です。動的型付けの言語では、規則を満たさない関数を書いても、言語は止めてくれません。
次の第10章では、この論点を、いまの実務にもっとも近い場面につなぎます。Coding Agent に最適化を頼むとき、何が起きるのかを扱います。
第10章 Coding Agent に最適化を頼むとき
初回記事の第1章で、次のように述べました。
Coding Agent に最適化を任せる時代だからこそ、プログラマの側から問いを立てる必要がある。
本章では、第3章の表Bを使って、その問いを言語ごとに具体的にします。
10-1 なぜ、問いを立てる必要があるのか
タロウくん:
先生、コードを速くしたいとき、いまは Coding Agent に頼めば書き換えてくれます。それでは、いけないのでしょうか。
専任講師:
頼むこと自体は、まったく問題ありません。
問題になるのは、提案された書き換えが正しいかどうかを、誰も確かめない場合です。
タロウくん:
書き換えが正しくない、ということがあるのですか。
専任講師:
第6章で見たとおりです。map f (map g xs) を map (f . g) xs に書き換えると、返す値は同じでも、副作用の順序が変わりました。
画面への出力、ファイルへの書き込み、データベースの更新が絡んでいれば、これは重大な違いです。
タロウくん:
でも、Coding Agent が、それを教えてくれるのではないですか。
専任講師:
教えてくれることもあります。しかし、教えてくれなかったときに気づけるかどうかが、この章の主題です。
本稿の測定で見たとおり、同じ書き換えでも、言語によって成り立つ条件が違います。その条件を知っていれば、提案を受け取ったときに、確認すべき点を自分で指定できます。
提案された書き換えを受け取ったときの、判断の手順を図に示します。
10-2 言語ごとに、何を確認させるか
LLM に最適化を依頼したとき、提案された書き換えについて、次の点を確認させるとよいと筆者は考えます。
| 言語 | 最適化手法 | 確認させる点 |
|---|---|---|
| OCaml、Standard ML、Scala、F#、Clojure、Erlang、Common Lisp | 2回の map を1回にまとめる、foldMap | 書き換えの前後で、関数を適用する順序が変わる。関数に副作用がないか |
| すべての言語 | bind の再結合 | そのモナドが結合律を満たしているか |
| OCaml | 同上 | 上記に加え、評価順序に依存した処理がないか。OCaml は評価順序を仕様で定めていない |
| F# | Codensity | 特定のモナドに固定した実装になっているか。F# は higher-kinded type を持たないため、任意のモナドについては書けない |
| OCaml、Scala、F# | foldr/build | rank-2 type を、polymorphic record field、polymorphic method、generic method のいずれで表しているか |
| Miranda、Standard ML | foldr/build、Codensity | この2つの手法を提案してきた場合、そのままでは型が付かないことを確かめる |
| Clojure、Erlang、Common Lisp | foldr/build、Traversable、Codensity | 型による正しさの保証がないことを前提に、同じ結果になることをテストで確かめる |
| すべての言語 | Difference List | 左結合の連結を繰り返していないか。この手法は言語を問わず効く |
この表は、本稿の測定から導いた提案です。筆者が LLM に実際に最適化を依頼し、その結果を確かめたものではありません。
10-3 表の読み方
表の行を、いくつか取り上げて説明します。
副作用の確認(1行目)
第6章の 6-10 で測ったとおり、純粋でない7言語すべてで、融合の前後で副作用の順序が変わりました。
したがって、これらの言語で融合を提案されたら、「対象の関数に副作用がないか」を確認する必要があります。
Haskell、PureScript、Clean では、この確認は要りません。型が、Int -> Int の関数に副作用を書くことを禁じているためです。
結合律の確認(2行目)
bind の再結合は、そのモナドが結合律を満たすことに依存します。
結合律は、どの言語の型検査でも確かめられません。Haskell でも同じです。モナドのインスタンスを定義するとき、結合律を満たすかどうかは、書いた人の責任です。
したがって、この確認は、言語を問わず必要です。
評価順序の確認(3行目)
OCaml は、評価順序を仕様で定めていません。実装では右から左に評価されますが、これは仕様上の保証ではありません。
引数の評価順序に依存した処理があると、書き換えによって結果が変わる場合があります。
型が付かないことの確認(6行目)
Miranda と Standard ML には、rank-2 type がありません。
foldr/build や Codensity を提案されたら、そのままでは型が付きません。提案を受け入れる前に、コンパイルが通るかを確かめる必要があります。
テストで確かめる(7行目)
動的型付けの3言語では、第6章で見たとおり、規則を満たさない関数を書いても、言語は止めてくれません。
したがって、書き換えの前後で同じ結果になることを、テストで確かめる必要があります。型が保証してくれない分を、テストで埋めることになります。
10-4 4軸で判断する
タロウくん:
先生、表にない言語や手法については、どう判断すればよいのでしょうか。
専任講師:
本連載の4軸に戻ってください。
提案された書き換えについて、次の4つを確かめます。
| 軸 | 確かめること |
|---|---|
| 型理論 | その書き換えの正しさは、型から導かれるか。動的型付けなら、言語は保証しない |
| 評価戦略 | 正格か非正格か。副作用の順序や、底の扱いが変わるか |
| 論理体系 | (定理証明言語を扱う第3回で問題になる) |
| 言語機能 | その書き換えを表す仕組みが、その言語にあるか |
タロウくん:
第3章の表Bを作るときに使った判断を、自分でやり直す、ということですね。
専任講師:
そのとおりです。よい整理です。
表Bは、本稿で扱った8つの手法についての判定です。ほかの手法が出てきたら、同じ4軸で自分で判定できます。
10-5 依頼するときの書き方
タロウくん:
先生、依頼するときに、あらかじめ伝えておくとよいことはありますか。
専任講師:
3つ挙げます。
1つ目。言語と、その言語の性質を明示することです。
「OCaml で」と書くだけでなく、「OCaml は正格評価で、型クラスがなく、評価順序を仕様で定めていない」と添えます。
2つ目。確認してほしい点を、依頼の時点で指定することです。
「書き換えの前後で、副作用の順序が変わらないかを確認してください」と書いておきます。10-2 の表が、そのまま指定の材料になります。
3つ目。測って確かめることです。
本稿の測定で見たとおり、同じ手法でも言語によって効き方が違いました。提案を受け入れる前に、自分の環境で測ってください。
タロウくん:
測ると、思ったのと違う結果が出ることもありますよね。
専任講師:
第6章の Erlang が、まさにその例でした。
公式の文書に書かれていることを実機で確かめたら、逆の結果が出ました。測っているものが違っていたのです。命令数と実行時間は、別のものでした。
タロウくん:
測って初めて分かることがあるのですね。
専任講師:
そうです。そして、測った結果をどう読むかにも、知識が要ります。
10-6 本章のまとめ
Coding Agent に最適化を任せることと、プログラマが判断を手放すことは、別のことです。
| 手放してよいこと | 手放せないこと |
|---|---|
| 書き換えのコードを書く作業 | その書き換えが、その言語で正しいかの判断 |
| どの手法があるかを思い出すこと | その手法が、その言語で使える条件を満たすかの確認 |
| 測定のコードを書く作業 | 測定の結果をどう読むかの判断 |
第9章で述べた「圏論の知識を使うのは誰か」という問いに、もうひとつの答えが加わります。
提案を受け取って判断する人も、その知識を使っています。
次の第11章では、本稿の限界を述べ、第3回への橋渡しをします。
第11章 本稿の限界と、第3回への橋渡し
11-1 本稿の限界
本稿の結論は、次の条件のもとで得られたものです。
条件が変われば、結論の一部が変わる可能性があります。
| 限界 | 内容 | 結論への影響 |
|---|---|---|
| 測定の時期 | 測定は複数の時期にわたって行った。時期が違うと、同じ処理系、同じコードでも値が変わった | Flambda 版と Cats の測定は別の時期に行った。これらは、同じ時期に測った値どうしでのみ比べた |
| 測定の条件 | 単一の計算機環境で測定した | 絶対値は環境によって変わる。倍率の傾向は変わりにくいと考えるが、確かめてはいない |
| Flambda | 主な測定は Flambda を有効にしていない版で行った。Flambda 版はソースからビルドし、後から別に測った | Flambda 版でも map の融合は行われず、手で融合したときの倍率はほぼ変わらなかった(2.05倍と2.10倍) |
| Clojure の処理系 | 主な測定は SCI インタプリタで行い、JVM 上の通常の Clojure でも同じ測定を行った | 絶対値はおよそ10分の1になったが、倍率の傾向は変わらなかった |
| Scala のライブラリ | Cats はソースからビルドし、Scala 3.3.6 で測った。ほかの Scala の測定(2.11)とは版も時期も異なる。Cats には Codensity が含まれていない | Codensity は Cats を使わずに自前で書いて測った。Kan 拡張は Scala では測っていない |
| Clean | Wine の上で Windows 版の Clean 3.1 を動かして測った。Linux 上のネイティブの処理系ではない | Wine の起動時間(57 ms)を差し引いて示した。起動時間のばらつきが、数ミリ秒の値に影響する |
| 表Bの判定 | すべての判定を、実機または文献で確かめた。10-3 の判定は、実機での確認により当初の判定を改めた | どの判定がどの根拠によるかは、表Bの根拠の表に示した |
| Miranda の測定条件 | Miranda だけは、リストの生成も時間に含めて測った | Miranda の倍率は、ほかの言語と条件が一致していない |
| 処理系の方式 | Miranda はインタプリタであり、ほかの言語の多くはネイティブコードへのコンパイラである | map の融合で Miranda の差が小さかった理由の一部は、処理系の方式にある可能性がある |
| 測定の分解能 | Common Lisp の測定の分解能は4ミリ秒である。Difference List の所要時間は1ミリ秒前後と小さい | Difference List の倍率は、細かく比べる意味がない。所要時間の桁の違いとして読む |
| 整数の大きさ | MLton と F# は既定の整数が32ビットであり、64ビットに変えて測った。PureScript の整数は32ビットで、桁あふれを折り返したまま測った | 総和の値そのものは言語間で比べられない。書き方どうしの結果の一致は確かめている |
| Coding Agent についての章 | 第10章の、確認させる点の表は、表Bから導いた筆者の提案である | LLM に実際に依頼して確かめたものではない |
map の融合について「効果の大きさは評価戦略で決まる」とした結論は、Flambda を有効にした OCaml と、JVM 上の通常の Clojure でも測り、傾向が変わらないことを確かめました。
一方、「Difference List は評価戦略も型付けも問わずに効く」とした結論は、計算量の違いにもとづくものです。測定の条件が変わっても、変わりにくいと考えます。
本連載の第5回では、連載全体を通じた自己批判を行う予定です。本節は、その第2回分にあたります。
11-2 測っていないこと
限界の表に加えて、そもそも測っていないことも挙げておきます。
| 測っていないこと | なぜ測っていないか |
|---|---|
| 実際のプログラムでの効果 | 本稿の測定は、特定の書き方に絞ったものである。第7章で引いた報告では、GHC の融合はプログラム全体で平均6.5%であった |
| メモリの使用量(OCaml 以外) | OCaml では確保語数を測ったが、ほかの言語では時間のみを測った |
| 並行処理や並列処理との関わり | 本稿の測定は、すべて単一の処理の流れで行った |
| コンパイルにかかる時間 | 融合や whole-program optimization は、コンパイルの時間を増やす。その大きさは測っていない |
| Clean の一意型による破壊的更新の、実務での効果 | 配列の書き換えという単純な例で測った。実際のプログラムでどれだけ効くかは測っていない |
タロウくん:
先生、1行目が重要ですね。本稿の測定は、特定の書き方に絞ったものなのですね。
専任講師:
そこは、はっきり述べておくべき点です。
本稿では、map を2回書いたコードで4.6倍という数字が出ました。しかし、実際のプログラムで map を2回書いている箇所は、全体のごく一部です。
第7章で引いた報告では、GHC の融合はプログラム全体で平均6.5%でした。
タロウくん:
4.6倍と6.5%では、ずいぶん違います。
専任講師:
測っている対象が違います。どちらも正しい数字です。
特定の書き方に絞れば大きな差が出るが、プログラム全体では、その書き方が現れる箇所は限られる。この2つを、混同しないでください。
タロウくん:
すると、本稿の数字は、どう読めばよいのでしょうか。
専任講師:
「その最適化が効く箇所では、どれだけ効くか」を示すものとして読んでください。
そして、自分のプログラムのどこにその箇所があるかは、自分で測って見つける必要があります。
11-3 第3回への橋渡し
本稿の表Aでは、論理体系の列が、すべての言語で「特に制約はない」となりました。
タロウくん:
表をみると、今回の記事では、関数型言語を分類する4つの観点(4つの分類軸)のうち、論理体系の観点(基準)が、今回取り上げた全ての言語について、問題なしになっていますね。
専任講師:
この観点(分類基準)は、次回の記事で取り上げる予定の定理証明言語を分類するときに、分類機能を発揮します。
タロウくん:
わかりました。
言語が採用する論理体系という特徴は、関数型言語ではどの言語も大差ないが、定理証明言語では、各言語がどの論理体系を採用しているかは大きな違いがあるということですか?
専任講師:
そのとおりです。
ただし、「大差ない」というより、本稿で扱った言語は証明を書くための言語ではない、と言ったほうが正確です。
そのため、本稿で扱った言語では、どの論理体系にもとづいているかが、最適化を使えるかどうかを左右しません。
一方、定理証明言語は、証明を書くための言語です。
どの論理体系を採用しているかで、証明した等式をプログラムの書き換えにそのまま使えるかどうかが変わります。
初回記事で、次の表を示しました。
| 言語 | 論理体系 | 証明した等式の扱い |
|---|---|---|
| Agda、Lean 4 | 直観主義論理 | 証明が計算の手順を与える |
| Isabelle/HOL | 古典論理 | 証明が計算の手順を与えるとは限らない |
| Isabelle/ZF | 集合論にもとづく別の体系 | 扱いがさらに異なる |
タロウくん:
Isabelle では、同じ処理系の中で、論理体系を選べるのでしたね。
専任講師:
そうです。
同じ処理系を使っていても、どの論理体系を選ぶかで、できることが変わります。
次回 は、Agda、Idris 2、Lean 4、Rocq、Isabelle/HOL、Arend を取り上げて、4つ目の軸が最適化の可否をどう左右するのかを見ていきます。
11-4 本稿を振り返って
最後に、本稿が答えた2つの問いを、もう一度示します。
問い1:初回記事で扱った最適化手法は、Haskell 以外の言語でも使えるのか。
答えは、手法によって違いました。
| 手法 | 答え |
|---|---|
| Difference List | 検証した10の関数型言語すべてで使え、桁違いに効いた |
| map の融合 | すべての言語で書けたが、効き方は評価戦略で決まった |
| foldr/build、Codensity | rank-2 type を直接、または代わりの仕組みで表せる言語で使えた |
| Traversable | higher-kinded type を持つ言語、または特定の型に固定すれば使えた |
| 動的型付けの言語での foldr/build、Traversable、Codensity | 書けるが、正しさを言語が保証しない |
問い2:圏論の知識は、誰が持っている必要があるのか。
言語によって、答えが変わりました。コンパイラの作者、ライブラリの作者、言語の設計者、マクロの作者、プログラマ自身、そして第10章で加えた、提案を受け取って判断する人です。
タロウくん:
先生、この連載を読んで、僕は何ができるようになったのでしょうか。
専任講師:
3つあります。
1つ目。自分の使っている言語で、どの最適化が使えるかを、表で確かめられます。
2つ目。使えない場合に、なぜ使えないのかを、4つの軸で説明できます。
3つ目。その最適化を誰が担っているのかが分かるので、コードが遅いときに、どこを見ればよいかが分かります。
タロウくん:
表を覚える必要はないのですね。
専任講師:
ありません。必要になったときに見返してください。
大切なのは、「この書き換えは、この言語で本当に正しいのか」と問えるようになることです。
その問いを立てられれば、表にない言語や手法が出てきても、自分で判断できます。
付録
表Cの再掲:言語ごとの、実機検証した最適化手法とその効果
最後に、本稿で実機検証した最適化と、その効果を、言語ごとにもう一度まとめます。
| 言語 | 実行した最適化手法 | 最適化の効果 |
|---|---|---|
| Haskell(参考) | GHC の書き換え規則(map f (map g xs) を map (f . g) xs に書き換える)map f (map g xs) を、プログラマが自ら map (f . g) xs と記述する(書き換え規則を無効にした場合)Difference List Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すfoldr/build(書き換え規則の有無) |
map f (map g xs) と記述したコードが 49.5 ms から 10.7 ms になった(4.6 倍)1.76 倍速くなった 15,107.8 ms が 0.2 ms になった 0.8968 s が 0.000074 s になった 1.74 倍速くなった 規則を無効にすると 19.8 ms が 26.9 ms になった |
| Miranda |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するDifference List foldMap、bind の再結合、エラーを集める検証を特定の型で書く |
1.05 倍にとどまった 27,219 ms が 23 ms になった(起動時間を含む) いずれも実行に成功した |
| PureScript |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するDifference List Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すfoldr c 0 (build g) を、プログラマが自ら g c 0 と記述する(要素数 10,000) |
2.29 倍速くなった 18,396.5 ms が 9.5 ms になった 1.8351 s が 0.0072 s になった 1.69 倍速くなった 4.3 倍速くなった |
| OCaml |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するDifference List リストの連結を右結合に変える Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すfoldr c 0 (build g) を、プログラマが自ら g c 0 と記述するFlambda を有効にして、 map f (map g xs) と map (f . g) xs を測り直す |
2.03 倍速くなった。確保したメモリは半分になった 23,390.6 ms が 0.8 ms になった 1,307 倍速くなった 0.2297 s が 0.000571 s になった 1.99 倍速くなった 24.5 倍速くなった map (f . g) xs と記述したコードとの差は 2.10 倍で、Flambda なし(2.05 倍)とほぼ同じ。Flambda は map (f . g) xs に書き換えなかった |
| Standard ML |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するDifference List 関数をモジュールやファンクタで包む traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すTraversable をファンクタとして書く |
1.75 倍速くなった 11,989.0 ms が 0.3 ms になった 性能は変わらなかった(差は3パーセント未満) 1.83 倍速くなった コンパイルと実行に成功した |
| Scala |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するview を挟むDifference List リストの連結を右結合に変える Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すfoldr c 0 (build g) を、プログラマが自ら g c 0 と記述するCats の Traverse(Scala 3.3.6) Cats の Chain(Scala 3.3.6) cats-free の Free(左結合の flatMap、Scala 3.3.6) |
4.09 倍速くなった 17.7 倍速くなった 4,024.3 ms が 9.2 ms になった 930 倍速くなった 0.3182 s が 0.000353 s になった 4.89 倍速くなった 6.82 倍速くなった 2.98 倍速くなった 3,350.7 ms が 4.97 ms になった n が倍になってもおよそ 1.5 倍から 1.9 倍の伸びにとどまった |
| F# |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するSeq を使うinline 関数にするDifference List foldr c 0 (build g) を、プログラマが自ら g c 0 と記述する |
1.94 倍速くなった 5.3 倍速くなった 差は出なかった(1.04 倍) 31,680.7 ms が 1.3 ms になった 28.8 倍速くなった |
| Clojure |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するtransducers を使う Difference List JVM 上の通常の Clojure で同じ測定を行う |
1.23 倍速くなった 1.63 倍速くなった 45,795.6 ms が 8.8 ms になった 絶対値はおよそ10分の1になったが、倍率の傾向は変わらなかった(プログラマが自ら map (f . g) xs と記述したコードで 1.19 倍、transducers で 1.85 倍) |
| Erlang |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するリスト内包表記を使う Difference List 型が推論される形で加算を書く |
1.83 倍速くなった 2.02 倍速くなった 3,503.4 ms が 2.2 ms になった 加算の命令が14から5に減り、1.07 倍速くなった |
| Common Lisp |
map f (map g xs) を、プログラマが自ら map (f . g) xs と記述するloop を使うDifference List 型を宣言する |
1.56 倍速くなった 約14倍速くなった(測定の分解能は4ミリ秒) 3,504 ms が4ミリ秒未満になった 10.8 倍速くなった |
| Clean | Clean のコンパイラの融合変換(同じモジュールで定義した map、要素数 10,000,000) Clean のコンパイラの融合変換(標準ライブラリの map) foldr/build と Clean のコンパイラの融合変換 Codensity(n = 12,000) traverse を2回呼び出すコードを、プログラマが自ら1回だけ呼び出すコードに記述し直すDifference List 一意型 による配列の破壊的更新(10 万回) |
199 ms が 99 ms になった(2.0 倍) 効かなかった 70 ms が 18 ms になった 1,060 ms が 1 ms 未満になった 1.12 倍速くなった 12,459 ms が 1 ms 未満になった 1 ms 未満(コピーを伴う書き換えは 614 ms) (Clean は Wine の上の Windows 版で測った。Wine の起動時間を差し引いた値) |
2回の map を1回にまとめる測定は要素数 2,000,000、Difference List は要素数 40,000、Codensity は bind を左結合に重ねる回数 n、Traversable と foldr/build は要素数 1,000,000(PureScript の foldr/build のみ 10,000)で測りました。
倍率は、いずれも最適化しない書き方と比べたものです。
表Cを縦に眺めると、Difference List の行は、どの言語でも数千ミリ秒から数ミリ秒へと、桁が変わっています。
一方、map の融合の効果は、言語によって 1.05 倍から 4.09 倍まで幅があります。
同じ「圏論の知見から導かれた最適化」でも、言語の性質に左右されにくいものと、左右されやすいものがあります。
その違いを見分ける手がかりが、本連載の4軸です。
用語の解説
本稿では、日本語の訳語を、定訳が確認できたものに限って用いています。
定訳を確認できなかった用語は、英語のまま記しています。
初回記事で解説した用語(自由定理、パラメトリシティ、Kan 拡張、Codensity など)については、初回記事の用語ミニ解説をご覧ください。
日本語の定訳を確認できた用語
| 用語 | 意味 |
|---|---|
| 正格(strict) | 関数の本体を評価する前に、引数を評価する性質 |
| 非正格(non-strict) | 引数を、必要になるまで評価しない性質 |
| 遅延評価(lazy evaluation) | 非正格な評価を実現する方式の1つ |
| パラメタ多相(parametric polymorphism) | 対象の型にかかわらず、同じ操作を行う多相性 |
| アドホック多相(ad-hoc polymorphism) | 対象の型によって、実際に行う操作が異なる多相性。型クラスはこれを扱う仕組みである |
| 部分型多相(subtype polymorphism) | 型のあいだの順序(部分型関係)にもとづく多相性 |
| 多相ラムダ計算(polymorphic λ-calculus) | 単純型付きラムダ計算に、多相関数を加えた体系。System F とも呼ばれる |
| 全称型(universal type) | 「任意の型 X について」という形の型。forall で書く型にあたる |
| 代数的エフェクト(algebraic effect) | 計算の効果を、代数の演算として扱う考え方。OCaml 5.0.0 以降では、エフェクトハンドラが導入された |
| エフェクトハンドラ(effect handler) | 代数的エフェクトを扱う仕組み。例外ハンドラを一般化したものである |
| 融合変換(fusion、deforestation) | 複数の関数や繰り返しを1つにまとめて、途中で作られる中間のデータを取り除くプログラム変換。deforestation は Wadler が1990年の論文で作った用語で、中間のデータ構造である「木」を取り除くことに由来する |
| 一意型(uniqueness type) | その値が共有されていないことを型で表す仕組み。Clean が持つ。共有されていない値は、破壊的に更新してよい |
| ファンクタ(ML の functor) | OCaml と Standard ML で、モジュールを受け取ってモジュールを返す、モジュール上の関数。圏論の関手とは別物である |
| 関手(functor) | 圏論で、圏から圏への対応。対象と射の両方を、恒等射と合成を保つように対応させる |
「一意型」は、実務家の記事で一貫して用いられている訳語です。学会論文や大学の講義資料での用例は確かめられていません。
「融合変換」について参照した文献は、いずれも関数型言語のプログラム変換の研究です。圏論の研究者のあいだでの用例は確かめていません。
出典:
五十嵐淳「ソフトウェア基礎論配布資料(7)パラメタ多相と System F」京都大学
https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/sf06w/resume7.pdf
出典:
五十嵐淳「工学部専門科目『計算と論理』配布資料 多相ラムダ計算(System F)」京都大学
https://io.kuis.kyoto-u.ac.jp/~igarashi/class/cal/systemF.pdf
出典:
眞田嵩大「エフェクトハンドラは準同型射である」2022年
https://www.kurims.kyoto-u.ac.jp/~tsanada/papers/handler-is-homomorphism.pdf
出典:
山﨑陽介、川端英之、弘中哲夫「代数的エフェクトハンドラを持つ言語のプログラムに対するエフェクト列の静的な見積り」日本ソフトウェア科学会第41回大会講演論文集、2024年
https://jssst.or.jp/files/user/taikai/2024/papers/6b-1-R.pdf
出典:
P. Wadler, "Deforestation: transforming programs to eliminate trees", Theoretical Computer Science, 73(2), pp. 231–248, 1990
doi: 10.1016/0304-3975(90)90147-A
https://doi.org/10.1016/0304-3975(90)90147-A
出典:
尾上能之、胡振江、岩崎英哉、武市正人「プログラム融合変換の実用的有効性の検証」コンピュータソフトウェア、17巻3号、pp. 273–277、2000年
doi: 10.11309/jssst.17.273
出典:
五十嵐淳、山口和紀「情報システム科学実習 II 第9回 ファンクター」京都大学
https://io.kuis.kyoto-u.ac.jp/~igarashi/class/syslabII01w/chap9.pdf
出典:
OCaml 公式チュートリアル「Functors」
https://github.com/ocaml/ocaml.org/blob/02b11348501cef1699c405c6c97fa61e5c529d2c/data/tutorials/language/1ms_01_functors.md
日本語の定訳を確認できなかったため、英語のまま記した用語
| 用語 | 意味 |
|---|---|
| rank-N polymorphism |
forall を、関数の矢印の左側などの内側に置くことを許す多相性。forall が型の外側にしかないものを rank-1 type、関数の引数の型の中に forall を置けるものを rank-2 type と呼ぶ |
| higher-kinded type | 型を受け取って型を返すもの(List や Maybe など)を、型変数として扱える機能 |
| row polymorphism | レコードが持つフィールドの集合を型変数で表し、「少なくともこのフィールドを持つレコード」を受け付ける多相性。PureScript が持つ |
| type constructor class | 型構築子(List など)を対象とする型クラス。Clean の言語報告書が用いる用語である |
| polymorphic record field | OCaml で、レコードのフィールドに多相型を持たせる機能。rank-2 type を表すために使う |
| polymorphic method | Scala で、型パラメータを持つメソッド。trait の中に置いて、rank-2 type を表すために使う |
| generic method | F# で、型パラメータを持つメソッド。インターフェースの中に置いて、rank-2 type を表すために使う |
| whole-program optimization | プログラム全体を一度に見渡して行う最適化。MLton が行う |
| defunctorization | ファンクタを適用箇所ごとに複製し、モジュールを取り除く変換。MLton が行う |
| monomorphization | 多相関数を、使われる型ごとに複製して多相性を取り除く変換。MLton が行う |
| defunctionalization | 高階関数を、データ構造と1階の関数に置き換える変換。MLton が行う |
| dictionary passing | 型クラスの実装を、関数の隠れた引数として渡す方式 |
| lazy sequence | 要素を必要になったときに1つずつ作る列。Clojure が持つ |
| transducers | Clojure の仕組み。変換を、入出力から切り離して合成できる。中間のコレクションを作らない |
「ランクN多相」「ランク1の型」という片仮名の表記は、有志による GHC ユーザーガイドの日本語訳などに見られます。ただし、教科書や学会論文での用例を確認できなかったため、本稿では英語のまま記しています。
実機検証について
検証した言語
本稿で取り上げた11の関数型言語のうち、歴史的な言及にとどめた Lisp を除く10の言語と、比較のための Haskell を、実機で検証しました。
| 実機検証した言語 | 実機検証していない言語 |
|---|---|
| Haskell、OCaml、Clojure、Standard ML、Common Lisp、Erlang、Scala、F#、PureScript、Miranda、Clean | Lisp |
使用した処理系
| 言語 | 処理系 | バージョン |
|---|---|---|
| Haskell | GHC | 9.4.7 |
| OCaml | ocamlopt | 4.14.1(Flambda なしと、ソースからビルドした Flambda 版の両方) |
| Standard ML | MLton | 20210117 |
| Common Lisp | SBCL | 2.2.9 |
| Erlang | Erlang/OTP | 25 |
| Scala | scalac / scala | 2.11.12、および 3.3.6(Cats の測定) |
| F# | fsharpc(Mono 上) | ── |
| Clojure | babashka(SCI インタプリタ)、および Clojure | 1.12.2-SCI、1.11.1(JVM 上、OpenJDK 21) |
| PureScript | purs | 0.15.16(実行は Node.js v22.22.2) |
| Miranda | mira | 2.066 |
| Clean | Clean(Windows 版、64ビット) | 3.1(Wine 9.0 の上で実行) |
測定の方法
| 項目 | 内容 |
|---|---|
| 測定の回数 | 原則として5回測定し、中央値を示しました。JIT を持つ処理系(Scala、F#、JVM 上の Clojure、Erlang)では、予備実行の後に測定しました |
| 結果の一致 | すべての測定で、書き方どうしの結果が一致することを確かめました |
| Miranda と Clean | 時間を測る組み込みの手段を用いず、プログラム全体の実行時間を外部から測りました。Clean では、Wine の起動時間(57 ms)を差し引いています |
| 測定の時期 | 測定は複数の時期にわたって行いました。時期の異なる値どうしは、直接比べていません |
測定でつまずいた箇所
同じことを試す読者のために、つまずいた箇所を挙げておきます。
| 言語 | つまずいた箇所 | 対処 |
|---|---|---|
| OCaml | 要素数2,000,000のリストを List.map で処理すると、既定のスタック上限で Stack overflow が起きる。List.map が末尾再帰でないため |
実行前に ulimit -s unlimited を実行した |
| Standard ML | MLton の既定の int は32ビット。総和が範囲を超えて Overflow 例外が発生する |
-default-type int64 を指定した |
| F# |
int が32ビットで、同じ桁あふれが起きる |
桁あふれを避ける形に書き換えた |
| PureScript |
Int が32ビット。桁あふれは例外にならず、黙って折り返す |
両方の書き方で同じように折り返すため、結果の一致の比較には影響しないと判断した |
| PureScript | Codensity は、n が12,000を超えると JavaScript のスタックが尽きる | 測定の範囲を n = 12,000 までとした |
| Miranda | ビルド時の最適化指定が高いと、impossible tag (-9) in reduce や BLACK HOLE で異常終了する |
Makefile の最適化指定を -O0 に変更した |
| Miranda |
undef が組み込みの名前として予約されている |
底を表す変数に別の名前を付けた |
| Clean | 融合の設定は、プロジェクト全体の設定だけでなく、モジュールごとの設定も書き換える必要がある | モジュールごとの設定を、最初のビルドの後に書き換えた |
| Haskell | GHC の full laziness が、繰り返しの測定のあいだで計算結果を使い回すことがある |
-fno-full-laziness を指定して測り直した |
訂正一覧
初回記事についての訂正は、該当がありません。
本稿の公開後に訂正が生じた場合は、この節に追記します。
関連記事
本連載
| 回 | 表題 |
|---|---|
| 初回 | Hask 圏は、圏ではない ── それでも GHC が圏論を使って最適化できる理由 |
| 第2回 | 本稿 |
| 第3回 | 定理証明言語を、同じ4軸で見る(予定) |
本稿と関連する筆者の記事
型理論について
- Computational type theory とは何か ── 型は先にあるのではなく、計算の振る舞いがあとから型を成す
https://qiita.com/etale_cohomology/items/a830a5ac5013a298fb97 - なぜ De Morgan cubical type theory には Computational type theory の実装がないのか ── Nuprl から RedPRL・cooltt への系譜
https://qiita.com/etale_cohomology/items/4035a0b3f4d40766437c
論理体系について(第3回の主題につながります)
- 論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学
https://qiita.com/etale_cohomology/items/24858c3bd7c7d6833eaa - 論理公理系の産業応用 全地図 ── 古典・直観主義・線形・様相・時相・記述・量子論理はどこで使われているのか
https://qiita.com/etale_cohomology/items/5206679c2fd02aea9512
圏論が実務で何に効くのかについて
- 圏論は実利的にどう役立つのか ── 「同じ絵が描ける」だけでは足りない、「難しい計算問題」を「簡単な計算問題」に置き換えるための条件
https://qiita.com/etale_cohomology/items/dd4fcc76132abf1c82f9 - 圏論で学習を組み立て直す ── Compositional Learning 入門:Backprop as Functor と「学習を部品から組み立てる」世界へ
https://qiita.com/etale_cohomology/items/bd3d618233da937aac2e
言語ごとの書き方を比べた記事
- 3 表連動・DCF・Monte Carlo を R / Python / Julia で実装する ── 重工業企業の財務モデルを書き比べる
https://qiita.com/etale_cohomology/items/e2daa6f08a1d43ee3144
出典一覧
本稿で参照した文献とウェブページを、本文に登場した順に掲げます。
型システムと論理
- H. P. Barendregt, "Introduction to generalized type systems", Journal of Functional Programming, 1(2), pp. 125–154, 1991. doi: 10.1017/S0956796800020025
- H. P. Barendregt, "Lambda calculi with types", in S. Abramsky, D. M. Gabbay, T. S. E. Maibaum (eds.), Handbook of Logic in Computer Science, Volume 2, Oxford University Press, pp. 117–309, 1992
- B. C. Pierce, Types and Programming Languages, MIT Press, 2002. https://www.cis.upenn.edu/~bcpierce/tapl/
- M. H. Sørensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, Volume 149, Elsevier, 2006
- University of Cambridge, L28: Advanced Functional Programming, Chapter 7 "Parametricity". https://www.cl.cam.ac.uk/teaching/1617/L28/parametricity.pdf
各言語
- PureScript 公式ドキュメント「Differences from Haskell」. https://github.com/purescript/documentation/blob/master/language/Differences-from-Haskell.md
- purescript-partial パッケージ. https://github.com/purescript/purescript-partial
- D. Turner, "An Overview of Miranda". https://www.cs.kent.ac.uk/people/staff/dat/miranda/Overview.html
- Miranda 公式サイト. https://miranda.org.uk
- ncihnegn/miranda(GitHub). https://github.com/ncihnegn/miranda
- OCaml 公式マニュアル「Optimisation with Flambda」. https://ocaml.org/manual/5.4/flambda.html
- Jane Street Blog, "A better inliner for OCaml, and why it matters". https://blog.janestreet.com/flambda/
- ocaml/ocaml(GitHub). https://github.com/ocaml/ocaml
- S. Wehr, M. M. T. Chakravarty, "ML Modules and Haskell Type Classes: A Constructive Comparison", APLAS 2008, LNCS 5356, Springer, pp. 188–204. doi: 10.1007/978-3-540-89330-1_14
- R. Milner, M. Tofte, R. Harper, D. MacQueen, The Definition of Standard ML (Revised), MIT Press, 1997
- MLton 公式サイト「Whole-Program Optimization」. http://mlton.org/WholeProgramOptimization
- "Adding Real-time Capabilities to a SML Compiler". https://arxiv.org/pdf/1601.03116
- Cats(Scala). https://typelevel.org/cats/
- typelevel/cats(GitHub). https://github.com/typelevel/cats
- scala/scala3(GitHub). https://github.com/scala/scala3
- 『F# High Performance』第7章「Language Features and Constructs Optimization」. https://packtpub.com/en-us/product/f-high-performance-9781786468079/
- Clojure 公式ドキュメント「Transducers」. https://clojure.org/reference/transducers
- Erlang/OTP 公式ブログ「More Optimizations in the Compiler and JIT」. https://www.erlang.org/blog/more-optimizations/
- "The Machine that Builds Itself: How the Strengths of Lisp Family Languages Facilitate Building Complex and Flexible Bioinformatic Models". https://arxiv.org/pdf/1608.02621
- A. Alimarine, S. Smetsers, "Improved Fusion for Optimizing Generics", IFL 2002, LNCS 2670, Springer, pp. 51–67. doi: 10.1007/3-540-44854-3_4
- "Clean for Haskell Programmers", 2024年. https://arxiv.org/pdf/2411.00037
- E. Barendsen, S. Smetsers, "Uniqueness Typing for Functional Languages with Graph Rewriting Semantics", Mathematical Structures in Computer Science, 1996
- harcokuppens/CleanIDE-wine-app-MacOS(GitHub). https://github.com/harcokuppens/CleanIDE-wine-app-MacOS
- harcokuppens/clean-classic-helloworld(GitHub). https://github.com/harcokuppens/clean-classic-helloworld
融合と最適化
- P. Wadler, "Deforestation: transforming programs to eliminate trees", Theoretical Computer Science, 73(2), pp. 231–248, 1990. doi: 10.1016/0304-3975(90)90147-A
- Y. Chen, L. Parreaux, "The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures", 2024年. https://arxiv.org/pdf/2410.02232
- HaskellWiki, "Correctness of short cut fusion". https://wiki.haskell.org/Correctness_of_short_cut_fusion
- 尾上能之、胡振江、岩崎英哉、武市正人「プログラム融合変換の実用的有効性の検証」コンピュータソフトウェア、17巻3号、pp. 273–277、2000年. doi: 10.11309/jssst.17.273
用語
- 五十嵐淳「ソフトウェア基礎論配布資料(7)パラメタ多相と System F」京都大学. https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/sf06w/resume7.pdf
- 五十嵐淳「工学部専門科目『計算と論理』配布資料 多相ラムダ計算(System F)」京都大学. https://io.kuis.kyoto-u.ac.jp/~igarashi/class/cal/systemF.pdf
- 五十嵐淳、山口和紀「情報システム科学実習 II 第9回 ファンクター」京都大学. https://io.kuis.kyoto-u.ac.jp/~igarashi/class/syslabII01w/chap9.pdf
- 眞田嵩大「エフェクトハンドラは準同型射である」2022年. https://www.kurims.kyoto-u.ac.jp/~tsanada/papers/handler-is-homomorphism.pdf
- 山﨑陽介、川端英之、弘中哲夫「代数的エフェクトハンドラを持つ言語のプログラムに対するエフェクト列の静的な見積り」日本ソフトウェア科学会第41回大会講演論文集、2024年. https://jssst.or.jp/files/user/taikai/2024/papers/6b-1-R.pdf
- OCaml 公式チュートリアル「Functors」. https://github.com/ocaml/ocaml.org/blob/02b11348501cef1699c405c6c97fa61e5c529d2c/data/tutorials/language/1ms_01_functors.md

