型クラスのご紹介
この記事は型 Advent Calendar 2019の23日目です。
おはようございます!!!coord_eです、よろしくどうぞ。
はじめに
この記事ではOCamlみたいなML系言語が登場します。関数型プログラミング言語と呼ばれる何かしらに触れたことがある人ならお気持ちで読み取れると思います。そうでない人はこちらからOCamlに入門してみると楽しいと思います。楽しいと思いますって何ですか...
また、私は正直なところこの記事を書くにあたって関連する十分な量の文献を読みこむことができたわけではなく、誤りが存在することは容易に想像できます。誤字や誤謬を発見された方は@coord_eまでご連絡ください。
概要
型クラス (type class)はWadlerによって[1]で提案された言語機能だ。本記事では型クラスを導入する動機をオーバーローディングの観点から紹介した後、Wadlerの型クラスを発展させたJonesのconstructor class[2]をベースにした本記事独自の体系の形式化を試みる。
型クラスの紹介
オーバーロードの必要性 *1
int
型の値が二つあって、等しいのか調べたいですね。コードを書きます
let rec eq_int a b = match a, b with | 0, 0 -> true | _, 0 -> false | 0, _ -> false | n, m -> eq_int (n - 1) (m - 1)
なるほど*2。じゃあstring
は*3?標準ライブラリにいい関数があったので借りてくる。
let eq_string = String.equal
いいね。使ってみる。*4
# eq_int 1 2 ;; - : bool = false # eq_string "abc" "abc" ;; - : bool = true
正しい感じがする。ところでOCamlには=
という演算子があって...同じ型であればこの演算子を使って値の比較ができる:
# (=) ;; - : 'a -> 'a -> bool = <fun> # 1 = 2 ;; - : bool = false # "abc" = "abc" ;; - : bool = true
お〜すごい。ところで文字列と数値は内部表現がかなり違いそうな気がしますが...
前の記事でちょっと書いた話と関連するんですが、OCamlはランタイムの値にメタな情報を埋め込んで、それを見ながら=
の実装内で実行時に分岐して比較しています。
でもちょっと待って、1 = 1
ではint
の値に適用しているんだからeq_int
を、"abc" = "abc"
ではstring
の値に適用しているんだからeq_string
を呼べばいいってことはコンパイル時に分かるのでは?整数含む全オブジェクトに共通の内部表現を持たせるのはなかなか厳しいものがあるので*5、コンパイル時に呼び分けることができたらかなり嬉しいですね。
おっとそれだけではない!!'a -> 'a -> bool
というハイパワーな型を持っているので、例えば関数同士の比較といった``ない''操作*6も型チェックを通ってしまう。
# eq_int = eq_int ;; (* runtime error *) Exception: Invalid_argument "compare: function value".
おぅ...これはしんどいわね。
別の例を見てみます。OCamlでも+
は見た目に違わず、加算の演算子です。使ってみましょう:
# 1 + 2 ;; - : int = 3 # 1.1 + 1.2 ;; Error: This expression has type float but an expression was expected of type int
なんか言ってますね。型を見てみます
# (+) ;; - : int -> int -> int = <fun>
なるほど+
はint
にしか使えないらしい。じゃあfloat
はどうすれば...+.
があります
# (+.) ;; - : float -> float -> float = <fun> # 1.1 +. 1.2 ;; - : float = 2.3
おお〜よかったですね。なんで使う型ごとに演算子を変えなきゃいけないんですか?(逆ギレ)
この時点でわかったしんどさをまとめてみます。=
と+
の例に共通していたのは、「同じ記号に型によって違う意味を持たせたい」という点でした。その上で:
- 型ごとに別名を作りたくない
+.
のようにユーザーに呼び分けを要求したくない
- 取れる型を、意味が存在する型のみに制限したい
(=) :: ('a -> 'a) -> ('a -> 'a) -> bool
は許容したくない(+) :: bool -> bool -> bool
も許容したくない
ここで登場するのが、一般にオーバーロード (overloading)と呼ばれる機能です。直感的な説明としては同じ名前に対して複数の意味を与えられる言語機能になります。下にC++での例を示します*7。
int add(int a, int b) { return add_int(a, b); } float add(float a, float b) { return add_float(a, b); }
ここで、add
には二つの実装があり、引数がint
かfloat
かによって呼び分けることができます。=
についても同様で、実際にC++の標準ライブラリではoperator==
が比較関数として様々な型にオーバーロードされています。
なお、今後の記事中で二項演算子(+
とか)は二引数関数として扱います。すなわち a + b
は (+) a b
としてパースされるイメージです。
多相性について
さて話は変わりますが、多相性 (polymorphism) について、お話しします。直観的には多相性は同じ値に複数の型をつけることが可能になる型システムの機能のことを言います。とある世界線ではジェネリクスと呼ばれたりします。なお複数の型が付くとはいえ候補が無限にある必要はない点に注意してください。 多相性には大きく分けて二種類あって、
- パラメトリック多相 (parametric polymorphism) 一つの名前に複数の型が付く。付く型によらず同一のオブジェクトを示す。
- アドホック多相 (ad-hoc polymorphism) 一つの名前が複数の型を持つ。付く型によって異なるオブジェクトを示す。
があります。パラメトリック多相のわかりやすい例としてはリストの長さを返す関数len :: 'a list -> int
があります。これは任意の'a
について'a list
型のリストの長さを求める一つの関数です。アドホック多相は先ほど紹介したオーバーロードですね。何もかもがパラメトリック多相で済めばいいんですがそんなことはなく、特にプリミティヴなオブジェクトに対する操作にアドホック多相が要請されることはよくあります。
型クラスあらわる
ではオーバーロードによるアドホック多相が先ほどの問題の解決策だとわかったところで、実際に実装することを考えてみましょう。先ほどの例で、=
は'a -> 'a -> bool
では弱すぎることがわかりました。+
ではその問題がよりはっきりしていて、'a -> 'a -> 'a'
ではたまったもんじゃない。じゃあ、名前に対して取れる型の集合を与えてあげてはどうだろう?int
, float
, bool
、そして関数型しかないと仮定すると、こう:
(=) :: { int -> int -> bool, float -> float -> bool, bool -> bool -> bool }
(+) :: { int -> int -> int, float -> float -> float }
オ〜良さそうだ。こういうやつを交差型と呼ぶが、しかしfetburnerさんの15日目の記事に
とあるように、何も考えずに交差型を導入するわけにもいきません。
そこで型クラス (type class) だ。Kaesが[3]でparametric overloadingと呼んだこの言語機能は、先ほどの完全なオーバーロードに制限を加え、オーバーロードされた名前が取りうる型を制限された型スキームの形で表現する。
(=) :: ∀'a. Eq 'a => 'a -> 'a -> bool
(+) :: ∀'a. Num 'a => 'a -> 'a -> 'a
無限に存在する型の集合に対して有限な表現が与えられている!いいじゃないですか、これを使えばオーバーロード解決ができるかはインスタンスかどうかを見ればいいので一発で判定できます。
さて、型クラスには次のような特徴がある[4]:
- 多相性: 関数につく型が一つに制限されない
- オーバーロード: 実装がつく型によって決定する
- 拡張可能: 定義を追加できる
多相性とオーバーロードについてはこれまで話した通り。"拡張可能性"は、あるクラスのインスタンスを、クラス側の再コンパイルなしに後から追加できる特徴をいい、これはthe expression problemの一つの解決策となりうる。
高階型を含むシステムでの型クラス
話は変わるがmap
関数を知っていますか?僕は知っています:
List.map :: ('a -> 'b) -> 'a list -> 'b list
さて、'a option
にもmap
は定義されている。
Option.map :: ('a -> 'b) -> 'a option -> 'b option
え〜、list
もoption
もFunctor
と呼ばれる共通の構造を持っており、Functor
に対する操作としてmap
は抽象化することができる。なら、map
もオーバーロードできまいか。
map :: ∀'a 'b 'f. Functor 'f => ('a -> 'b) -> 'a 'f -> 'b 'f
ムッ、Functor
になっている'f
は型ではなく型コンストラクタだ。型コンストラクタのような、型を受けとって型を返すようなものを高階型(higher order types)と呼んだりするが、これの上の型クラスも許すことができたら嬉しいです。この記事では型の概念を拡張し、こういったクラスも許容する体系を扱います。型クラスと高階型を組み合わせた体系はconstructor classという名前で[2]で提示されました。
高階型に対する型クラスがあると様々な抽象を表現することができて、例えば先ほどのFunctor
の他にもMonad
というのがあります。Monad
は手続きを抽象化した構造で、Haskellにような純粋関数型のプログラミング言語で手続きを構造として扱う上で欠かせないものとなっています。[2]にモナドを紹介している節があるのでそれを見るとよく解ると思います。
型クラスを含む型システム
では先ほどふわふわとお話しした型クラスを形式化していきましょう!
記法
構文の定義には BNF記法 (Backus-Naur Notation)を使用する。ただしBNFにおけるリテラルにはの書体を使用する。メタ変数が集合の上を動くことをと表記する。列について、のときは空の列とする。また、メタ変数 の0個以上の列をと表記し、列に含まれる要素を元とする集合を]と表記する。
二項関係と, の元, について、を]と表記する。またをと表記する。
その他、集合や関係に関して標準的な記法を用いる。また今後も定義を述べた後にそれに関係する略記や記法を導入することがあり、それについてはその都度記載する。
形式化
class
, instance
宣言を式中で陽に扱う、高階型クラスの体系を考える。推論規則は[2]や[5]をベースにしている。[5]の形式化とは、class
/instance
が式である、型変数のカインドを明示している、の二点で異なっている。
型は[2]の定義をそのまま使う。は型コンストラクタ名で、int
とMaybe
とかそういうのです。
え〜 が我々が普段呼ぶところの型なんですが、ここでは[2]に倣って型コンストラクタと呼ぶことにします。待って、型に乗っている は*8…これは型の種 (kind) です。種とは何かの説明はここではしませんが、直感的な説明としては「型の型」です。[6]の29章に詳しく書いてあると思います。さて、種を以下のように定義します:
を特に型 (type) と呼びます*9。は種 を持つ型コンストラクタ、 は型を取って型を返す型コンストラクタ変数、といった具合です。型の定義に内因的に種が含まれている点に注意してください。なお、今後とをそれぞれ単に, と表記することがあります。またをと表記します。さらに型中の型変数をそれぞれで置き換えた型をと表記します。また の代わりに型を部分に含む別の要素を置く場合があるが、その場合は部分の型に同様に代入したものを表記している(ただし型スキームに対しては定義しない.)*10。
次に型にまつわる様々を定義していきます。
はクラス名、は述語 (predicate)であり、述語はとクラス との関連を表しています。
それぞれ型、修飾型 (qualified type)、型スキーム (type scheme)です。型スキームで全称量化されている型コンストラクタ変数 はだけでなく任意のカインドを取ることができる点に注意してください。なお、のの部分のことを指してコンテキスト (context)と呼びます。
さて、下に今回の言語の文法*11を示します。なお、 を1
, "string"
みたいなリテラルの上を動く文字として使用しています。
ここに推論規則を当てていきます。ただし:
- にはリテラルとそれに対応する型が入っています。例えばです。
- は型環境 (type environment)で、変数と対応する型スキームが入っています。は型付けが進むに従って変更されていきます。
- は述語の集合です。後に述べる型付け関係に用いられているとき、これを前提(premise)と呼ぶことにします。前提はコンテキストの置き場で、直感的には述語を除去するときに使えるの前提条件です。実際にの上で除去できるコンテキストは消せると行った操作があります()。
- は
class
とinstance
によって定まる、コンテキストの包含を表す二項関係です。この のもと、での時が実際に除去可能 (直観的にはならば) だということを表す二項関係を定義します。
これらを用いて型付け規則を定義します。型付け関係はの形をしており、「, , のもとで式 は型スキームが付く」と読みます。下に具体的な型付け規則を示します。なお、規則中で、をの略記として、また]をの略記として用いています。
と 以外はほとんど[2]からの引用です*12。 一方でclass
とinstance
については[2]の中で
The precise definition of entailment is determined by the class and instance declarations that appear in a given program.
としか言及されていないので*13、 と 、あとあたりを自分で考えました (👈大丈夫か?)
推論例
この推論規則の適用の様子をいくつか紹介します。まずは一応おさらいとして普通のHMの範囲で型付けの様子を見てみよう:
let id = \x. x in (id id) 1
ウォウ〜。デカいがまあこんな感じ*14。 で束縛前に型スキームにしてやることで、使うときに で好きな型にインスタンス化してやることができる。よかったね
じゃあ次は型クラスを使った式の推論を見てみる。
class Eq a^* where eq :: a -> a -> bool in instance Eq int where eq = eqInt in eq 1 2
でがしっかり葬り去られているのが見えると思います。
ここからコンテキスト付きのインスタンスとかsuperclassとかを含んだ例についても推論例を示したほうがいいと思うんですが2つ書いてみてあまりにも面倒だったのでやめます。各自、紙と鉛筆でお試しください。
型クラスの実装 (未完)
実装は間に合いませんでした!!!が主要なアルゴリズムは実装されていて、あとはハンドラを書いていく感じですね。extensible effects最高!!一番好きなAn Alternative to Monad Transformersです
実装が完成したらアルゴリズムと実装について記事を書きます...いち早く知りたい人は[1]と[7]、そして[8]をチェック...!
おわりに
本記事ではWadlerによって提示された言語機能である型クラスについて、高階型を含む体系での応用にも触れつつ紹介した。また、型クラスを含む型システムの推論規則を紹介した。
参考文献
- [1] Wadler, Philip, and Stephen Blott. "How to make ad-hoc polymorphism less ad hoc." Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1989.
- [2] Jones, Mark P. "A system of constructor classes: overloading and implicit higher-order polymorphism." Journal of functional programming 5.1 (1995): 1-35.
- [3] Kaes, Stefan. "Parametric overloading in polymorphic programming languages." European Symposium on Programming. Springer, Berlin, Heidelberg, 1988.
- [4] Peterson, John, and Mark Jones. "Implementing type classes." ACM SIGPLAN Notices. Vol. 28. No. 6. ACM, 1993.
- [5] Hall, Cordelia V., et al. "Type classes in Haskell." ACM Transactions on Programming Languages and Systems (TOPLAS) 18.2 (1996): 109-138.
- [6] Pierce, Benjamin C. 型システム入門 プログラミング言語と型の理論. 株式会社 オーム社, 2013.
- [7] Jones, Mark P. "Typing haskell in haskell." Haskell workshop. Vol. 7. 1999.
- [8] Demystifying Type Classes - http://okmij.org/ftp/Computation/typeclass.html
*1:OCamlをdisるみたいな構図になっていて本当に申し訳ない、OCamlでもファンクタを使えば似たようなことはできると思うのでOCamlのことは嫌いにならないでください、お願いしましたよ。
*2:負の数のこと忘れてたけど面倒だからこれでええか?いいよ
*3:構造的等値の話しかしない
*4: #はsuperuserとは全く関係なくてocamlのトップレベルに打ってねって意味なのでsuperuserで実行したことによるいかなる事態についても責任は負えません
*5:しんどかった.
*6:や、∀a. f a = g a ↔ f = g なのかもしれませんがそんなことを決定する能力は一般的なプログラミング言語に備わっていないので...
*7:実はこれのせいでfloatで呼び出そうとするとambigousって怒られるんだが本質とは関係ないので無視してくれよな...
*8:型になんか乗っていますが、は単にメタ変数として扱います
*10:このあたり雑で申し訳ない...+型スキームは少なくともそうじゃないので
*11:superclassの表記が左矢印なのはPureScriptの真似
*12:表記を変えたぐらい
*13:[2]ではclassとinstanceはグローバルに宣言されることになっているので、式について議論する分にはこれで十分だったんじゃないかな
*14:居ない環境は省略している