型クラスのご紹介 - molecular coordinates

この記事は型 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におけるリテラルには $\texttt{monospaced}$ の書体を使用する。メタ変数 $x$ が集合 $S$ の上を動くことを $x ::\in S$ と表記する。列 $x_1, \ldots x_n (n \ge 0)$ について、 $n = 0$ のときは空の列とする。また、メタ変数 $x$ の0個以上の列 $x_1...x_n (n \ge 0)$ を $\overline{x}$ と表記し、列 $\overline{x}$ に含まれる要素を元とする集合を $[\overline{x}$ ]と表記する。

二項関係 $R \subseteq S \times T$ と $S$ , $T$ の元 $s \in S$ , $t \in T$ について、 $R \cup{{(s, t)}}$ を $R [ s \mapsto t$ ]と表記する。また $(s, t) \in R$ を $R(s) = t$ と表記する。

その他、集合や関係に関して標準的な記法を用いる。また今後も定義を述べた後にそれに関係する略記や記法を導入することがあり、それについてはその都度記載する。

形式化

class, instance宣言を式中で陽に扱う、高階型クラスの体系を考える。推論規則は[2]や[5]をベースにしている。[5]の形式化とは、class/instanceが式である、型変数のカインドを明示している、の二点で異なっている。

型は[2]の定義をそのまま使う。 $\chi$ は型コンストラクタ名で、intとMaybeとかそういうのです。

f:id:coorde:20191224003647p:plain

え〜 $c^\kappa$ が我々が普段呼ぶところの型なんですが、ここでは[2]に倣って型コンストラクタと呼ぶことにします。待って、型に乗っている $\kappa$ は*8…これは型の種 (kind) です。種とは何かの説明はここではしませんが、直感的な説明としては「型の型」です。[6]の29章に詳しく書いてあると思います。さて、種を以下のように定義します:

f:id:coorde:20191224003703p:plain

$c^*$ を特に型 (type) と呼びます*9。 $c^\kappa$ は種 $\kappa$ を持つ型コンストラクタ、 $\alpha^{* \rightarrow *}$ は型を取って型を返す型コンストラクタ変数、といった具合です。型の定義に内因的に種が含まれている点に注意してください。なお、今後 $\chi^*$ と $\alpha^*$ をそれぞれ単に $\chi$ , $\alpha$ と表記することがあります。また $\rightarrow^{* \rightarrow * \rightarrow *} \, c_1^* \, c_2^*$ を $c^*_1 \rightarrow c^*_2$ と表記します。さらに型 $\tau$ 中の型変数 $\alpha^{\kappa_1}_1, \ldots \alpha^{\kappa_n}_n$ をそれぞれ $c^{\kappa_1}_1, \ldots c^{\kappa_n}_n$ で置き換えた型を $[\alpha^{\kappa_1}_1/c^{\kappa_1}_1, \ldots \alpha^{\kappa_n}_n/c^{\kappa_n}_n]\tau$ と表記します。また $\tau$ の代わりに型を部分に含む別の要素を置く場合があるが、その場合は部分の型に同様に代入したものを表記している(ただし型スキームに対しては定義しない.)*10。

次に型にまつわる様々を定義していきます。

f:id:coorde:20191224003712p:plain

$\phi$ はクラス名、 $\theta$ は述語 (predicate)であり、述語 $\phi \; c^{\kappa_1}_1 \ldots c^{\kappa_n}_n$ は $c^{\kappa_1}_1 \ldots c^{\kappa_n}_n$ とクラス $\phi$ との関連を表しています。

f:id:coorde:20191224003722p:plain

それぞれ型、修飾型 (qualified type)、型スキーム (type scheme)です。型スキームで全称量化されている型コンストラクタ変数 $\alpha^\kappa$ は $*$ だけでなく任意のカインドを取ることができる点に注意してください。なお、 $\overline{\theta} \Rightarrow \tau$ の $\overline{\theta}$ の部分のことを指してコンテキスト (context)と呼びます。

f:id:coorde:20191224002348p:plain

さて、下に今回の言語の文法*11を示します。なお、 $l$ を1, "string"みたいなリテラルの上を動く文字として使用しています。

f:id:coorde:20191224003731p:plain

ここに推論規則を当てていきます。ただし:

$L \subseteq \textbf{Literal} \times \textbf{Type}$ にはリテラルとそれに対応する型が入っています。例えば $L(42) = \texttt{int}$ です。
$A\subseteq \textbf{Variable} \times \textbf{TypeScheme}$ は型環境 (type environment)で、変数と対応する型スキームが入っています。 $A$ は型付けが進むに従って変更されていきます。
$P \subseteq \textbf{Predicate}$ は述語の集合です。後に述べる型付け関係に用いられているとき、これを前提(premise)と呼ぶことにします。前提はコンテキストの置き場で、直感的には述語を除去するときに使えるの前提条件です。実際に $P$ の上で除去できるコンテキストは消せると行った操作があります( $\text{ELIM}$ )。
$E \subseteq \textbf{Context} \times \textbf{Context}$ はclassとinstanceによって定まる、コンテキストの包含を表す二項関係です。この $E$ のもと、 $P \Vdash_E P'$ で $P$ の時 $P'$ が実際に除去可能 (直観的には $P$ ならば $P'$ ) だということを表す二項関係 $\Vdash_E$ を定義します。

f:id:coorde:20191224002501p:plain

これらを用いて型付け規則を定義します。型付け関係は $E \mid P \mid A \vdash e : \sigma$ の形をしており、「 $E$ , $P$ , $A$ のもとで式 $e$ は型スキーム $\sigma$ が付く」と読みます。下に具体的な型付け規則を示します。なお、規則中で、 $\forall \alpha^\kappa_1, \ldots \alpha^\kappa_n. P_1 \rightarrowtail P_2$ を $\{\left([\alpha^{\kappa_1}_1/c^{\kappa_1}_1, \ldots \alpha^{\kappa_n}_n/c^{\kappa_n}_n]P_1, [\alpha^{\kappa_1}_1/c^{\kappa_1}_1, \ldots \alpha^{\kappa_n}_n/c^{\kappa_n}_n]P_2\right) \mid c^{\kappa_1}_1 \in C^{\kappa_1}_1, \ldots c^{\kappa_n}_n \in C^{\kappa_n}_n\}$ の略記として、また $E [\forall \overline{\alpha^\kappa}. P_1 \rightarrowtail P_2$ ]を $E \cup{\left(\forall \overline{\alpha^\kappa}. P_1 \rightarrowtail P_2\right)}$ の略記として用いています。

f:id:coorde:20191224002601p:plain

$\textit{CLASS}$ と $\textit{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、 $\textit{CLASS}$ と $\textit{INSTANCE}$ 、あと $\Vdash_E$ あたりを自分で考えました (👈大丈夫か？)

推論例

この推論規則の適用の様子をいくつか紹介します。まずは一応おさらいとして普通のHMの範囲で型付けの様子を見てみよう:

let id = \x. x in
(id id) 1

f:id:coorde:20191224005303p:plain

ウォウ〜。デカいがまあこんな感じ*14。 $\textit{GEN}$ で束縛前に型スキームにしてやることで、使うときに $\textit{INST}$ で好きな型にインスタンス化してやることができる。よかったね

じゃあ次は型クラスを使った式の推論を見てみる。

class Eq a^* where eq :: a -> a -> bool in
instance Eq int where eq = eqInt in
eq 1 2

f:id:coorde:20191224005246p:plain

$ELIM$ で $Eq \; \texttt{int}$ がしっかり葬り去られているのが見えると思います。

ここからコンテキスト付きのインスタンスとか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:型になんか乗っていますが、 $c^\kappa$ は単にメタ変数として扱います

*9:[6]曰く真の型

*10:このあたり雑で申し訳ない...+型スキームは少なくともそうじゃないので

*11:superclassの表記が左矢印なのはPureScriptの真似

*12:表記を変えたぐらい

*13:[2]ではclassとinstanceはグローバルに宣言されることになっているので、式について議論する分にはこれで十分だったんじゃないかな

*14:居ない環境は省略している