私はあなたにParametricityについて紹介しようと思います

#前書き
この記事は「IQが1 Advent Calendar 2017 - Adventar」(https://adventar.org/calendars/2377 )の5日目の記事になります.

概要

• Parametricityの紹介をします
• Philip Wadler:"Theorems for free!", Proceeding FPCA '89, pp.347-359
• Parametricityとは 多相な関数に関する定理
• 論文の方がはるかにわかりやすいので，詳しい話は論文を読んでください．この記事では概要しか触れません．
• Parametricityを使ってChurch表現について考えます
• やってみただけで結論はありません :)

前提知識

そんなに難しい話はできないので，そこまで身構えなくても大丈夫なはずです．
一応，以下の知識がある方向けに書きます．

• 単純な$\lambda$計算を見たことがる
• パラメータ多相(ジェネリクス)を使ったことがある or 知ってる

リファレンス

• Philip Wadler:"Theorems for free!", Proceeding FPCA '89, pp.347-359
  • 今回の話のメインです．事前知識もあまりいらずに読めるのおすすめです．
• 型システム入門(TaPL) https://estore.ohmsha.co.jp/titles/978427406911P
• ラムダ計算の記法とかはこの本に準拠しているはずです．この本も面白いのでおすすめです．

アウトライン

• 論文の紹介
• Introduction
• Parametricity
• 例
• チャーチ表現に適用
• チャーチブール表現
• チャーチ数

論文の紹介

Introduction

多相な型を持つ関数について，型だけからわかる情報について考えてみます．
関数$r_X$が

  r_X : \forall X. X^* \to X^*

という型をもつことを考えます．ここで，$X^ * $は$X$型のリスト型を表します．
つまり，上記の$r_X$の型は，任意の型$X$に対して，$X^* $型を受け取って$X^*$型を返す関数の型です．
このとき，$r_X$について以下の性質が成り立ちます．

 a^* \circ r_A = r_A' \circ a^* .

ここで，$a^* : A^* \to A'^* $(ある関数$a: A \to A'$をリストの要素に作用させる関数$\mathrm{map}, a$)です．
つまり，上の性質は以下の二つの関数が同値であることを示しています．

• 左辺: $r_A$を適用してから，関数$a^*$を適用する関数
• 右辺: 関数$a^*$を適用してから，$r_A$を適用する関数

関数$r_X$は，任意のリスト型$X^*$について定義されています．よって，$r_X$は型$X$に依存しない関数でなければならず，すべてのリスト型に共通の操作しかできない，というのが直感的な理解です．
(注記: 純粋な二階ラムダ計算を仮定しています．また，fixpoint operatorはないものとしています．fixpointがある場合の議論は論文を参照してください．)

例えば，リストの要素を並び替える関数を$r_X$としてとると，上記の性質を満たすことがわかります．
上記の観察を定式化したものがparametricityです．

例

Parametricityの定式化の前に，もう少し論文で取り上げられている例を見てみます．
$a: A \to A'$，$b: B \to B'$，$-^* : \forall A. A \to A^* $，$-^* : \forall A \forall B .((A \to B) \to (A^* \to B^* ))$とします．ここで，$-^* $は型に対しての操作と関数に対しての操作のどちらに対しても定義されています．

リストの結合

リストの結合関数を，$(++): \forall X . X^* \to X^* \to X^*$とします．すると，以下の等式が成り立ちます．

  a^* \, (xs ++_A ys) = (a^* \, xs) ++_{A'} (a^* \, xs)

つまり，1)リストの結合後に関数を適用して得られたリストと，2)関数を適用してからリストを結合して得られたリストの二つが等しいことを主張しています．

リストのフィルタリング

リストのフィルタリングをする関数$filter: \forall X. (X \to Bool) \to X^* \to X^*$と，述語$p' : A' \to Bool$について以下の等式が成り立ちます．

 a^* \circ filter_A (p' \circ a) = filter_A' p' \circ a^*

フィルタリングと関数$a^*$の適用順序を入れ替えても結果が等しいという主張です．(右辺の述語$(p' \circ a)$は型を合わせるために関数合成を使用しています)

Parametricity

今まで直感的な例を見てきました．ここから上記の直感を定式化していきます．
定式化に際して，違った視点から型を見る必要があります．

型を関係としてみる

普通，型を見るときは集合として見ることが多いと思います．例えば，Int型は整数の集合，$\mathrm{Int} \to \mathrm{Int}$型は関数の集合，$\forall X . A(X)$型はある集合$B$を受け取って集合$A(B)$の要素を返す関数の集合，のような見方です．

違った視点として，型を関係(relation)としてみることもできます．集合$A, A'$として，集合$A$と$A'$の関係$\mathcal{A}$を，$\mathcal{A} : A \Leftrightarrow A'$と書くことにします．このとき$\mathcal{A} \subset A \times A'$ です．
また，要素$x \in A, x' \in A'$が$\mathcal{A}$によって関係しているとき，$(x, x') \in \mathcal{A}$と書くことにします．

関係の特別なケースとして，恒等関係(identity relation)$I_A: A \Leftrightarrow A$があります．これは，$I_A = \{(x, x) \mid x \in A\}$で定義されます．また，関数も関係として見ることができます．要素$x \in A$について，関数$a: A \to A'$を関係$\{(x, a,x) \mid x \in A\}$と見ることもできます．またこのとき，$x' = a , x$として，$(x, x') \in a$と書くこともできます．

以上の記法を用いて，型を関係として捉えていきます．
先ほどまでの議論ででてきた型の種類は，

1. 基本型($Int, Bool$等)
2. リスト型($A^*$)
3. 関数型($A \to B$，前述の関係としての関数と関数型に対応する関係は別ものです)
4. 全称型($\forall X . A(X)$)
   があります．
   以下で，これらそれぞれの型について考えてみます．

基本型

基本型は単純に恒等関係として考えます．
$I_{Int}: Int \Leftrightarrow Int$や，$I_{Bool}: Bool \Leftrightarrow Bool$など．

リスト型

任意の関係$\mathcal{A}: A \Leftrightarrow A'$について，関係$\mathcal{A}^* : A^* \Leftrightarrow A'^* $は，

 ([x_1, \dots, x_n], [x_1', \dots, x_n']) \in \mathcal{A}^* \, \iff \, (x_1, x_1') \in \mathcal{A} \land\,\dots, (x_n, x_n') \in \mathcal{A}

で定義されます．
つまり，1)同じ長さを持ち，かつ2)各要素が関係しているときに，リストが関係します．
関係の特別なケースとして，関数がありました．それを用いて，関係$\mathcal{A}$として関数$a$を考えると，これはリストのマッピング関数に相当します．

関数型

任意の関係$\mathcal{A}: A \Leftrightarrow A', \mathcal{B}: B \Leftrightarrow B'$について，関係$\mathcal{A \to B}: (A \to B) \Leftrightarrow (A' \to B')$は，

  (f, f') \in \mathcal{A \to B} \, \iff \, \forall (x, x') \in \mathcal{A}, (f\, x, f'\, x') \in \mathcal{B}

で定義される．
特殊な例として，関係$\mathcal{A}, , \mathcal{B}$として関数$a, b$を取ることを考えます．
このとき，1)関係$a \to b$は関数である必要はない，2) $(f, f') \in a \to b \implies f' \circ a = b \circ f$，の2つが成り立ちます．
2)を導出してみます．
まず，関数$a, , b$の関係としての定義より，$\forall (x, x') \in a. x' = a,x$，かつ$\forall (y, y') \in b . y' = b , y$(ここで，$a,, b$は関数としての意味と関係としての意味があることに注意)．
関係$a \to b$の定義より，

  (f, f') \in a \to b \,  \iff \, \forall (x, a \, x) \in a . (f\, x, f'\,(a\, x) ) \in b.

ここで，$(f, x, f', (a, x)) \in b$のとき，関係$b$の定義より，$b, (f, x) = f',(a,x)$が成り立つことがわかります．
よって，2)の式が成り立つこともわかります．

全称型

関係$\mathcal{X}$に依存する関係$\mathcal{F(X)}$を考えます．このとき$\mathcal{F}$は，関係$\mathcal{A}: A \Leftrightarrow A'$を取り関係$\mathcal{F(A)}: F(A) \Leftrightarrow F(A')$を返す関数のようにみなすことができます．

以上の直感を用いて，関係$\mathcal{\forall X., F(X)}: \forall X., F(X) \Leftrightarrow \forall X'., F(X')$を，

  (g, g') \in \mathcal{\forall X.\, F(X)} \iff \mathcal{\forall A}: A \Leftrightarrow A'. \, (g_A, g'_{A'}) \in \mathcal{F(A)}

と定義します．

つまり，多相的な関数$g, g'$が関係を持つとき，$g, g'$は関係のある型の組$A, A'$を関係のある結果$(g_A, g_{A'})$に移します．

Paramtricity

上記の関係を用いることで，任意の閉じた型$T$を関係$\mathcal{T} : T \Leftrightarrow T$とみなすことができます．
これを用いて，Parametricityを説明することができます．

Parametricity
$t$を型$T$の閉じた項とする．
このとき型$T$に対応する関係$\mathcal{T}$について，$(t, t) \in \mathcal{T}$．

つまり，ある項の型から，その型に対応する関係の性質を用いて，項の振る舞いについて考えることができるということです．

注記:
この命題の証明は省略します:)
論文ではこの命題のより形式的な定義，及び証明のスケッチに触れているので気になる方は論文を読んでください．

Parametricityを使ってみる

この節では，論文に取り上げられているfold関数の例を紹介します．

Fold関数

fold関数はリストの畳込みを行う関数で，型は$\forall X. \forall Y. (X \to Y \to Y) \to Y \to X^* \to Y$です．

parametricityから，

 (fold, fold) \in \mathcal{\forall X. \forall Y. (X \to Y \to Y) \to Y \to X^* \to Y} 

がいえます．
ここで，関数$a: A \to A',, b: B \to B'$を使って，上記のパラメータ$\mathcal{X,,Y}$を具体化します．全称型$\forall$の定義を２回適用することで，

  (fold_{AB}, fold_{A'B'}) \in (a \to b \to b) \to b \to a^* \to b

が得られます(ここでは，関数が関係の一種であることを用いています)．$(a \to b \to b) \to b \to a^* \to b$の表記に違和感がありますが，パラメータ$\mathcal{X,, Y}$は関係の上を動くことと，関数は関係であることを考えると正しいことがわかります．

得られた式について，関数型に対応する関係の定義を適用することで，

\begin{align}
& \forall (f, f') \in (a \to b \to b). \\
& \quad \forall (u, u') \in b. \\
& \quad \quad (fold_{AB} \,f\, u, fold_{A'B'}\, f'\, u') \in a^* \to b
\end{align}

が得られます．

ここで，$(f, f') \in a \to b \to b$である関数$f,f'$について

\begin{align}
& \forall x \in A,\, x' \in A',\, y \in B',\,y'\in B'. \\
 & ((x, x') \in a \land (y, y') \in b \iff x' = a\,x \land y' = b\,y) \\
 \implies & (f\,x\,y, f'\, x' \, y') \in b \\
 \iff & b (f\, x\, y) = f\,x'\,y'
\end{align}

が成り立つことが関数型に対応する関係の定義からわかります．

またリスト型に対応する関係と関数型に対応する関係の定義より，

\begin{align}
 &(fold_{AB} \,f\, u, fold_{A'B'}\, f'\, u') \in a^* \to b\\
\iff & \forall (x_i, \, a\,x_i) \in a . \\
& \quad \Bigl(\bigl(fold_{AB} \,f\, u [x], fold_{A'B'}\, f'\, u' (a^* \,[x])\bigr) \in b \iff b\,(fold_{AB} \, f\, u\, [x]) = fold_{A'B'} \, f' \, u' \, (a^*\,[x])\Bigr)
\end{align}

が成り立ちます．ここで，$[x] = [x_1, \dots, x_n]$です．

したがって，foldに対する関係は以下のように言い換えることができます．

\begin{align}
&\forall a: A \to A',\,b: B \to B'. \\
& \quad \forall x \in A,\,y \in B.\,b\,(f\, x\, y) = f'\,(a\,x)\,(b\,y) \land b\,u = u'\\
& \implies b \circ fold_{AB}\,f\,u = fold_{A'B'} \,f'\,u' \circ a^*.
\end{align}

この式は，$(f, f') \in (a \to b \to b)$かつ$(u, u') \in b$であるような$f, , f', ,u, ,u'$について，

1.畳込みをしてから関数$b$を作用させたもの
2.関数$a$をリストに適用してから畳み込みをしたもの

の2つが等しいことを主張しています．

別の視点から見ると，代数的構造に関する言明のように見ることもできます．
詳しくはここでは触れませんが，構造$(A, B, f, u)$と$(A', B', f', u')$の準同型射$a, b$について，関数$a^* , b$が構造$(A^* , B, fold_{AB} ,f,u)$と$(A'^* ,, B',,fold_{A'B'},f',u')$の準同型射になります．
論文ではさらに詳しい説明があるので，そちらを参照してください．

チャーチ表現に適用

以上のparametricityを用いて，チャーチ表現について考えてみます．この記事で取り扱うチャーチ表現は型システム入門(https://estore.ohmsha.co.jp/titles/978427406911P )と同様のものです．

チャーチブール表現

型無しラムダ計算のチャーチブール表現は以下の形で定義することができます．

\begin{align}
 true &= \lambda x. \lambda y . x,\\
 false &= \lambda x. \lambda y. y.
\end{align}

直感的には$true = \lambda x., \lambda y. \mathrm{if} ,true, \mathrm{then}, x, \mathrm{else}, y$のような，if式の一種として捉えることができます．

この型無しラムダ項に型をつけていきます．当然ながら1)$true, ,false$に同じ型を付けたいです．この型を$Bool$とします．このとき$Bool$型は，項の形から，2)関数型$hoge \to fuga \to poyo$のようになるはずです．
1)，2)を満たすためには，$true, ,false$の引数$x,y$の型が等しくなければならないことがわかります．
したがって，

\begin{align}
  Bool &= \forall X. X \to X \to X, \\
  true &= \lambda X . \lambda x: X . \lambda y: X. x,\\
  false &= \lambda X. \lambda x: X. \lambda y: X. y,
\end{align}

となります．ここで，$\lambda X. t$は型を取るラムダ抽象で，$\lambda x:X. t $は型$X$を引数に取るラムダ抽象としています．項$\lambda X. t$に型$X$を適用するときは，$(\lambda X. t),[Y]$と書くことにします．

parametricity

ではparametricityを使って考えてみます．任意の$Bool$型の項$t$について，

  (t, t) \in \mathcal{\forall X. X \to X \to X}

が成り立ちます．
このとき，関数$a: A \to A'$について，

\begin{align}
 & (t_A, t_{A'}) \in a \to a \to a \\
\iff & \forall x \in A,\, y \in A. x' = a\, x \land y' = a\,y \\
\implies & \bigl((t_A \, x\, y, t_{A'} \, x' \, y') \in a \\
& \iff a(t_A\,x\,y) = t_{A'}\,x'\,y' \\
& \iff a(t_A\,x\,y) = t_{A'} \, (a\,x)\, (a\,y)\bigr)
\end{align}

が成り立ちます．
つまり，$Bool$型の項$t$は，任意の関数$a: A \to A'$について，引数$x, ,y$のどちらかを返す操作しかしないことがわかります．

実際，$Bool$型の項は他にも，

 true' = \lambda X. \lambda x: X. \lambda y:X. (\lambda f: X \to X. \lambda z: X. f\,x) (\lambda z: X. z) 

などが考えられますが，これらの項が引数に対して何もしないことが確かめられます．

チャーチ数

型無しラムダ計算のチャーチ数を以下のように定義します．

\begin{align}
 \bar{0} &= \lambda f . \lambda x. x,\\
 \bar{1} &= \lambda f. \lambda x. f(x),\\
 \bar{2} &= \lambda f . \lambda x. f(f(x)),\\
  &\vdots
\end{align}

よく見慣れた形だと思います．これに型をつけることを考えます．項の形から，$x$と$f(x)$の型が等しいことがわかります．
つまり，$x: X$とすると，$f: X \to X$．
よって，チャーチ数の型$Nat$は，$Nat = \forall X. (X \to X) \to X \to X$になります．

parametricity

では，parametricityを$Nat$型に適用してみます．

\begin{align}
  & (t, t) \in \mathcal{\forall X. (X \to X) \to X \to X} \\
\implies & \forall a: A \to A'. (t_A, t_A') \in (a \to a) \to a \\
\iff & \Bigl( \forall f : A \to A. a \circ f = f' \circ a \\
& \qquad \implies a \circ (t_A\, f) = (t_A' \, f') \circ a \Bigr).
\end{align}

ここで，$t_A,f: A \to A$であることに着目すると，$t_A,f$を関数と見ることができます．
つまり，任意の関数$a$と，$a \circ f = f' \circ a$を満たす関数$f,,f'$について，$t_A, f, t_A',f'$も$f,,f'$と同様の制限を満たす関数になります．
$a \circ f = f' \circ a$より，$a \circ f \circ f \dots \circ f = f' \circ f' \dots \circ f' \circ a$ですから，$Nat$型の項は，受け取った関数$f$を$n$回($n \leq 0$)適用する関数だということがわかります．

まとめ

• Parametricityを紹介しました
• それをChurch表現に適用してみました
• "Theorems for free!"とTaPLはすごく面白いので読んで欲しいです