「アドホック多相」「パラメトリック多相」という言葉は、ハッキリとした定義がないままに使われることが多いようです。その実情を追認、あるいは実情に迎合して「どうせ定義がイイカゲンなんだから、イイカゲンに使えばいいよね」と述べたのが「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない」です。とはいえ、同じ記事の最後のほう「「アドホック多相 vs パラメトリック多相」をマジメに考えてはいけない // それでもマジメに考えたいのなら」と、昨日の記事「蒸し返し： アドホック多相 vs パラメトリック多相」では、定義をハッキリさせる試みをしました。
もともとが曖昧な概念を明確化すると、それは（広く合意を得られないので）俺流定義になってしまいます。昨日の記事で述べた「パラメトリック性 ＝ 自然性」も、「オレの思っているパラメトリック性と違う」という人はいるでしょう。僕も、「パラメトリック性」が持つ“雰囲気”は、自然性だけでは言い尽くせない気がしています。
自然性では汲み取れない性質を「満足性〈satisfaction property〉」として定式化してみます。例題は、昨日と同じlength関数です。
内容：
続きの記事：
とりあえずパラメトリックなlength関数
多相関数のパラメトリック性〈parametricity property〉とは、関数のインデックス族〈indexed family of functions〉の自然性〈naturality〉だと定義する（そう決めて話をする）と、length関数のパラメトリック性＝自然性は次の図式の可換性として記述できます。
図式の可換性の成立は、Setの部分圏Cに依存します。ある部分圏Cに関してlengthが自然であることを、次のように書きます（昨日の記事での約束）。
- length is-natural-on C
昨日の記事で述べた、A君、B君、C君が書いた３つのlengthをまとめた多相関数lengthは、圏S1に関して自然にはなりません。
自然に〈パラメトリックに〉ならなかった理由は、C君が「長さ」に関してA君、B君とは異なる連想をしていたからです。そこで、上司のXさんは次のように言います。
- 3人でちゃんと相談して、それぞれが書いた関数達をまとめた多相関数が、圏S1に関して自然〈パラメトリック〉になるようにしなさい。
3人は相談して、「めんどくせーから、これでいいことにしようぜ」と、次の関数を書きました。
function lengthByA = lambda(x : List<Int>){ 0 } function lengthByB = lambda(x : List<Char>){ 0 } function lengthByC = lambda(x : List<Real>){ 0 }
あらゆるリストの長さは0です。これらをまとめた多相関数lengthは、圏S1に関して自然になります。
Xさんは、内心不満を感じながらも3人を叱るわけにもいきません。3人は言われたことをちゃんとやってますからね。
満足性とは何か
Xさんが内心不満を感じるのは、lengthへの期待があり、それを裏切られたからです。lengthへの期待は「lengthらしさ」と言ってもいいでしょう。常に値が0ではlengthらしくないのです。
「lengthらしさ」を持っていることをパラメトリック性とは呼ばないでしょうが、雰囲気としては、パラメトリックなら「らしさ」も持っているだろうと期待します。実情としては、暗黙に（あくまで暗黙にですが）パラメトリック性が「らしさ」を持つことも含意してるかも知れません -- Xさんの内心の期待と、それを裏切られた不満のように。
さて、「らしさ」の定式化として満足性〈satisfaction property〉を定義しましょう。満足性の定義には、インスティチューション理論の道具立てを使います。が、インスティチューション理論を知っている必要はありません。
Xさんは「lengthらしさ」を内心期待してましたが、3人に伝えてません。「lengthらしさ」を何個かの文として言語化しなくてはなりません。実際の関数fが、文sで記述された性質を実際に持つとき、次のように書きます。
- f |= s
記号'|='（TeXだと \vDash ''）は、満足関係〈充足関係 | satisfaction relation〉の記号です。「関数fは文sを満足する」と読みます。
文sが、Xさんの思う「lengthらしさ」を記述しているとして、A君、B君、C君が書いた実際の関数が実際に「lengthらしい」ことは次のように書けます。
- lengthByA |= s
- lengthByB |= s
- lengthByC |= s
Xさんの思いが単一の文ではなくて2つの文 s1, s2 で記述されているなら：
- lengthByA |= s1, lengthByA |= s2
- lengthByB |= s1, lengthByB |= s2
- lengthByC |= s1, lengthByC |= s2
このように、なんらかの文（の集まり）で記述された条件を満たすことが満足性です。
思いを正確に伝える
Xさんの思う「lengthらしさ」を、A君、B君、C君に自然言語（日本語）の文で伝えてもいいですが（多くの場合はそうするでしょう）、「length〈長さ〉という言葉からの連想が人により違う」ことによる失敗は既に経験済みです（昨日の記事）。自然言語の曖昧さや連想の豊かさによるトラブルを避けるには人工的な論理言語を使うほうがいいでしょう。ここでは、常識的な（古典論理の）論理式を使うことにします。
論理式の文法は知られていますが、「lengthらしさ」を記述するための基本語彙〈ボキャブラリー〉が必要です。基本語彙の定義には指標〈signature〉と呼ばれる形式が使われます。以下が、「lengthらしさ」を記述するための基本語彙を定義する指標です*1。
signature ListAndLength{
type X in Set
function nilX : 1 -> List(X) in Set
function consX : X×List(X) -> List(X) in Set
function lengthX : List(X) -> Z in Set
}
指標〈signature〉はインスティチューション理論の用語ですが、プログラミング用語ならインターフェイス〈interface〉です。length以外に、nil, cons という名前も宣言しています。下付きのXは省略してもかまいません。
上記指標によって準備された基本語彙（nil, cons, length）を使って「lengthらしさ」を記述する文を書いてみます。
- 文1： length(nil(1)) = 0
- 文2： ∀x∈X.∀z∈List(X).( length(cons(x, z)) = lengt(z) + 1 )
1 = {1} として、nil : 1 → List(X) なので nil(1) と書いてますが、単に nil() あるいは nil だけでもかまいません。
文1, 文2 に出てくるlengthはプレースホルダーなので、A君が書いた実際の関数lengthByAが文1を満たすことは、次が成立することです。
- lengthByA(nil(1)) = 0
ここで出てくるnilはプレースホルダーではなくて、事前に実装済みの実際の関数を指します。事前に実装済みの nil, cons が変な挙動をしたりすると話がややこしくなるので、常識的意味で nil, cons は“正しく”動くとします*2
文2の満足性ならば、次が成立することです。
- ∀x∈Z.∀z∈List(Z).( lengthByA(cons(x, z)) = lengtByA(z) + 1 )
成立の確認には無限回のテストが必要なので、現実世界ではテストで完全な確認はできません。
もし、Xさんが文1と文2を満足させることを3人に要求していれば、「内心不満を感じながらも3人を叱るわけにもいきません」とはならなかったでしょう。
パラメトリック性と満足性
パラメトリック性＝自然性だとして、満足性は前節で説明した意味だとします。形式上は、パラメトリック性と満足性は別な性質です。しかし、「パラメトリック性が満足性も含意している」ような雰囲気があります。これは何故でしょう？
多相関数がパラメトリックであることの定義として「単一のプログラムコードで書ける」というのがあります。僕は、書くプログラミング言語／書き方によりけりなので、これは定義として使えないと思っています。が、ともかくも単一のプログラムコードで書いた多相関数があったとしましょう。その多相関数が、特定の型に対して（条件文で記述された）ある性質を持つとき、他の型に対しても同じ性質を持つことが期待できるでしょう。少なくとも、型ごとの複数のプログラムコードを寄せ集めた場合よりは期待できます。
この期待できる感じが、「パラメトリック性は満足性を含意する」雰囲気を作り出しているのではないでしょうか。
いずれにしても、「感じ」と「雰囲気」なので、正確な議論にはなりません。正確に議論するには、パラメトリック性＝自然性と満足性を別に定義して、その相互関係を調べることになります。
