FreeStyleWiki

パラメーター多相

このエントリーをはてなブックマークに追加

[プログラミング,関数型プログラミング]

パラメーター多相

TwitterでフォロワーがJavaのGenericsについて言及しており

「Javaはパラメーター多相はすべての機能が実装されてないのではないか?」

ということを言っていたので調べてみる。

調べた感じ結論としてはJavaはランク1 (冠頭) 多相までしか実装されてないと言えそうだ。

→ Genericsはランク1 (冠頭) 多相だよね?

そして、Ocamlはその辺いろいろ気が利くようだ 高階関数,多相性,多相的関数

さあ、HaskellでもランクK多相やランクN ("高階") 多相は実装されてるけど使い所がよくわからん。見ていきましょう。

  パラメーター多相のそれぞれの種類

全部翻訳するのは辛いので、まず頭出しだけしておこう。

  • Higher-ranked polymorphism
    • Rank-1 (prenex) polymorphism
    • Rank-k polymorphism
    • Rank-n ("higher-rank") polymorphism

それぞれ、WikipediaのParametric polymorphismのページから採集。

Wikipedia - Parametric polymorphism

それぞれ訳語をあてるとすると

  • 高階多相
    • ランク1 (冠頭) 多相
    • ランクK多相
    • ランクN ("高階") 多相

よく考えるとランクK多相はランクN ("高階") 多相の数が少ない版である

となる、次にこれの実例を挙げる。

ランク1 (冠頭) 多相

要は、パラメータ多相とは以下のような疑似コードを実装できるということである;

append :: forall a. ( [a] -> [a] -> [a] )

Haskellでは7.12.1. 明示的な全称量化(forall)に書かれている通り、普段は省略されている量化記号を明示的に記載することが可能で、上記は明示的に記載した例となる。

なんちゃって数式的に書くと以下の通り

\( \forall_a \space append ([a], [a]) \to [a] \)

つまり、すべての型a(型引数)に対して型aの配列を2つとる関数append(a,a)は型aの配列を返す。みたいなもの、ここではappendの実装内容はなんでもいいが、名前からして第1引数の[a]に第2引数の[a]を連結したものを返すと想定される。

Haskellで言うと説明が簡単なのだが、要はこれType Class(型クラス)の簡単な例である

forall a. が左端にしか出てこないので"冠頭"。というか実用的にはこれでよくないか?的な感じはしますね。

ランクN ("高階") 多相

要は、高階多相とは多相的関数を多相型で呼ぶことができ、データ構造に多相的な型をパラメタとして与えることができるということ;

こんな感じ(forall a.がappendの引数に入った); append :: (forall a. [a] -> [a]) -> [a]

これはいったい何が嬉しいのか?

例えば、[a]->Intを引数にとる関数([a]->Int)->Intがあったとする。

func:: ([a]->Int)->Int

func f = f [1,2,3] + f["a","b","c"]

これは型エラーになる。なぜならf[Int]、f[ [Char] ]というfの出現2つにそれぞれ対応して

インスタンス化されることで生成された、f::[Int]->Intとf::[ [ Char ] ] -> Intという

ボトムアップで定まる2つの型制約を、引数としての識別子fの型が同時に満せないからである。

Haskellのforallについて理解したことを書いておく(ランクN多相限定)。 より引用

例を見てわかるように、f [1,2,3], f["a","b","c"] はそれぞれIntegerの配列とStringの配列の呼び出しであるため、func:: ([a]->Int)->Int では表すことができない。不思議なことであるが∀aで表された型というのは関数の外で1回定められるものなので、これを受容できない。その辺Haskellはhindley-milnerの型検査という方式で型を検査しているらしく、詳しくはリンク先参照。

これを回避するために、「型スキーマを取ってきてインスタンス化する」という行為を、

1つの関数の中で何回も行なえるようするための拡張が、GHCのランクN多相(XRankNTypes)である。

Haskellのforallについて理解したことを書いておく(ランクN多相限定)。 より引用

というわけで冒頭で書いた関数のシグネチャに戻る。append :: (forall a. [a] -> [a]) -> [a]

関連
7.12. 型システムへのその他の拡張

ランクK多相

ランクK多相は上記「ランクN ("高階") 多相」の型指定をK個に限定できるだけである。

実際の例は 7.12.5. 任意ランク多相

    f1 :: forall a b. a -> b -> a
    g1 :: forall a b. (Ord a, Eq  b) => a -> b -> a

    f2 :: (forall a. a->a) -> Int -> Int
    g2 :: (forall a. Eq a => [a] -> a -> Bool) -> Int -> Int

    f3 :: ((forall a. a->a) -> Int) -> Bool -> Bool

    f4 :: Int -> (forall a. a -> a)

高階多相が何であるか理解できていれば、これは大したことないですね。

  参考

  • Rank-1 (prenex)のprenexは逐語訳としては冠頭を当てるべきように思う
    • 記号論理学の一階述語論理(FOL)で使われる用語で冠頭標準形というのがある
    • 一階述語論理は量化記号を使って論理をもれなくいい感じに表すための記法である
    • 人類はフレーゲが現れるまで数式+自然言語を矛盾なしに表すことができなかったが、フレーゲが述語論理を発明し、続く数学者たちがそれらを発展させて今の形におちついた