Haskell/Polymorphism

Parametric Polymorphism (パラメータ多相型)

Section goal = short, enables reader to read code (ParseP) with ∀ and use libraries (ST) without horror. Question Talk:Haskell/The_Curry-Howard_isomorphism#Polymorphic types would be solved by this section.

Link to the following paper: Luca Cardelli: On Understanding Types, Data Abstraction, and Polymorphism.

forall a

ご存知の読者もいるかとは思うが、polymorphic (ポリモーフィック、多相型) 関数とは、多くの異なる型に対して作用する関数である。例えば、length関数

  length :: [a] -> Int

はどの長さのリストに対してもリストの長さを計算することができ、また文字列String = [Char]や整数列[Int]など、どのようなリストに対しても適用できる。length関数の定義にある型変数 a はどのようなelement typeでも指定できることを表している。

他の例を挙げる。

  fst :: (a, b) -> a
  snd :: (a, b) -> b
  map :: (a -> b) -> [a] -> [b]

これらは任意の型からなるペアから値を取り出す関数と、型aから型bへの関数を型aのリストへマップする関数である。

IntやStringのように大文字から始める具象型と異なり、型変数は必ず小文字から始めて記述する。処理系は大文字か小文字かによって具象型と型変数を区別する。型変数であることを特に明示したければ、forallをもちいる。

 length :: forall a. [a] -> Int

この関数シグネチャを日本語に書き下せば、「すべての型 aに対して(for all type a)、length関数は, 型aの元をもつリストを引数にとり、整数を返す。」となる。 前の表記はforallを省略したものとみなせる。

このような、forallのような変数を修飾してすべてのものをさすようにするキーワードを全称量化子と呼ぶ。数学の述語論理の記号∀(forall と読む)と同じものである。

Polymorphism 高階型

forallキーワードを導入したことによって、Polymorphic な引数をとる関数を定義できる。

  foo :: (forall a. a -> a) -> (Char,Bool)
  foo f = (f 'c', f True)

ここで、f は、任意の型を入力できる多相型関数である。特にこの例では、f が文字型定数 'c' および、ブーリアン型定数 True に対して適用でき、同じ型の結果を返す性質を利用している。

forall キーワードが導入されていないHaskell98の環境では、このような関数は定義できない。

似たようなシグネチャをもつ関数bar

  bar :: (a -> a) -> (Char, Bool)

つまり

  bar :: forall a. ((a -> a) -> (Char, Bool))

の定義は、foo と同じではない。この関数 bar は「ある特定の型に対して、それと同じ型を返すような関数ならば、どのような関数fでも（例えば abs :: Num a => a -> a などでも) 入力する」ことを表しており、関数 foo の表す「どのような型でも受け取って同じ型を返すような関数」（たとえば id :: a -> a）ならば入力する、とはまったく異なっている。

bar関数のような単純な多相型関数の型を1階型 (rank-1 type) と呼ぶ。また、fooの型は2階型に属する。さらに、(n-1)階型の引数を1つ以上とる関数をn階型と呼ぶ。

一般の高階型のシステムはSystem Fによって理論的に解析できる。System F は second-order lambda calculus としても知られる。forall の意味と、(foo と bar のように) 置かれる場所の違いによる差異についてより深く理解するために、詳細をSystem Fのセクションで解説する(予定)。

Haskell98 は、System F よりも制約条件の強い Hindley-Milner の型システムに基づいており、forallを使った2階型や、高階型をサポートしていない。これらの制約を外し、System F の強力なシステムを利用するためには、RankNTypes拡張を使う。

Haskell98標準で高階型をサポートしない理由は、System F の型推論は決定不能であり、プログラマがすべての型シグネチャを書く必要があったからである。このことから、初期のHaskellでは高階型が取り扱えない代わりに完全な型推論が可能な Hindley-Milner の型システムを採用したのである。しかし、研究の進歩により、現在のHaskell処理系では型シグネチャを書く負担が軽減され、高階型の関数をつかったプログラミングも実用的なレベルにある。

runST

Haskellで実用的なプログラムを書く人にとっては、ST monadは実際に使う型としては始めてのランク-2型であったといえるだろう。この型は、IO monadと同じように、変更可能な参照と変更可能な配列を与える。

  newSTRef   :: a -> ST s (STRef s a)
  readSTRef  :: STRef s a -> ST s a
  writeSTRef :: STRef s a -> a -> ST s ()

型変数 s はread/writeで変更される状態を表現している。しかし、IOとは異なり、このステートフルな計算を純粋なコードの中で行うことができる。特に、この関数は

  runST :: (forall s. ST s a) -> a

初期状態を設定し、計算を実行し、状態を捨てて計算結果を返す。ご覧のように、これにはランク-2型が使われている。 何故だろうか？

ポイントは、変更可能な参照は一つのrunSTに対してローカルであるべきということだ。具体的には、

  v   = runST (newSTRef "abc")
  foo = runST (readVar v)

これは間違っている。なぜなら、一つ目のrunSTのコンテキスト内で作成した変更可能な参照を、二番目のrunSTで再び使おうとしているからだ。言い換えれば、vの場合、(forall s. ST s a) -> aの結果の型aはSTRef s Stringでないかもしれない。しかし、ランク-2型はまさにそれを保証する！何故なら、引数の型(forall s. ST s a)のsは多相的でなければならず、全てのsに対して、同じ型aを返さなければならない。結果の型aはsに依存することは出来ないのだ。従って、この望ましくないコード片は上記の型エラーを含んでおり、コンパイラはそれを拒否する。

STモナドのオリジナルの論文では、より詳細な解説を見つけることが出来る。 Lazy functional state threads

Impredicativity

• predicative = type variables instantiated to monotypes. impredicative = also polytypes. Example: length [id :: forall a . a -> a] or Just (id :: forall a. a -> a). Subtly different from higher-rank.

• relation of polymorphic types by their generality, i.e. `isInstanceOf`.
• haskell-cafe: RankNTypes short explanation.

System F

Section goal = a little bit lambda calculus foundation to prevent brain damage from implicit type parameter passing.

• System F = Basis for all this ∀-stuff.
• Explicit type applications i.e. map Int (+1) [1,2,3]. ∀ similar to the function arrow ->.
• Terms depend on types. Big Λ for type arguments, small λ for value arguments.

Examples

Section goal = enable reader to judge whether to use data structures with ∀ in his own code.

• Church numerals, Encoding of arbitrary recursive types (positivity conditions): &forall x. (F x -> x) -> x
• Continuations, Pattern-matching: maybe, either and foldr

I.e. ∀ can be put to good use for implementing data types in Haskell.

Other forms of Polymorphism

Section goal = contrast polymorphism in OOP and stuff. how type classes fit in.

• ad-hoc polymorphism = different behavior depending on type s. => Haskell type classes.
• parametric polymorphism = ignorant of the type actually used. => ∀
• subtyping

Free Theorems

Secion goal = enable reader to come up with free theorems. no need to prove them, intuition is enough.

• free theorems for parametric polymorphism.

See also

• Luca Cardelli. On Understanding Types, Data Abstraction, and Polymorphism.

このページ「Haskell/Polymorphism」は、書きかけです。加筆・訂正など、協力いただける皆様の編集を心からお待ちしております。また、ご意見などがありましたら、お気軽にノートへどうぞ。

訳注: この記事は翻訳元が書きかけです。