Haskell/Polymorphism

訳註: このウィキブックスのページでは、Haskellにおけるポリモーフィズムについて説明されています。ポリモーフィズムは、プログラミング言語において同じコードを複数の型に対して再利用するための技術です。; Haskellでは、ポリモーフィックな関数を定義する方法がいくつかあります。ジェネリック関数は、任意の型に対して機能する関数であり、型変数を使用して宣言されます。また、型クラスは、特定の操作をサポートする型のグループを定義する方法です。; このページでは、ポリモーフィズムの概念を詳しく説明し、Haskellでのポリモーフィズムの実装について説明しています。さらに、Haskellの型クラスシステムについても解説しています。

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.

セクションの目標 = 短く、読者がコード(ParseP)を∀で読み、ライブラリ(ST)を恐怖なく使うことができるようにする。質問 https://en.wikibooks.org/wiki/Talk:Haskell/The_Curry%E2%80%93Howard_isomorphism#Polymorphic_types は、このセクションで解決されるでしょう。

以下の論文にリンクしています。Luca Cardelli: 型、データ抽象化、ポリモーフィズムの理解について (On Understanding Types, Data Abstraction, and Polymorphism).

訳註: この論文は、1985年に発表された計算機サイエンスに関する論文であり、Luca CardelliとPeter Wegnerによって書かれました。この論文では、プログラミング言語における型の概念を理解し、型理論の最近の研究を反映した型付き多相プログラミング言語のモデルを提示し、実用的なプログラミング言語の設計に最近の研究がどのように関連しているかを調べています。; また、オブジェクト指向言語が型、データ抽象、多様性の概念の相互作用を探求するための枠組みと動機を提供しているため、型をデータ抽象に拡張し、型継承が重要な多様性の形態であることを踏まえて、これらの相互作用を探求するためのλ-計算ベースのモデルを開発しています。; この論文では、非型の世界から単相型、そして多相型システムへの言語の進化、多重定義、強制、サブタイプ、パラメータ化などの多様性のメカニズムが調べられ、型理論に基づく多様性の統一的なフレームワークが提供されています。; この論文では、拡張型λ-計算がプログラミング言語として使用され、様々な例を使って説明されています。また、この論文では、Funという名前の新しいプログラミング言語を提案しており、Funは強力で表現力豊かな型付きオブジェクト指向言語の設計のための基盤として役立つことができます。

`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^[1]をもちいる。

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

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

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

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^[3]拡張を使う。

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^[4]

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.

predicative = 型変数が 単一型 にインスタンス化されることを意味する。 impredicative = 多相型 でもある。例： length [id :: forall a. a -> a] または Just (id :: forall a. a -> a)。高階ランクと微妙に異なる。
多相型の関係性は、それらの一般性によって定義される。つまり、 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.

セクションのゴール = 暗黙的な型パラメーターの渡し方による脳ダメージを防ぐために、少しラムダ計算の基礎を学びます。

System F = すべての ∀-ものの基盤。
明示的な型適用、つまり map Int (+1) [1,2,3]。 ∀は関数の矢印 -> に似ています。

項は型に依存します。型引数には大きな Λ、値引数には小さな λ を使用します。

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.

セクションの目的 = 読者が自分自身のコードで∀を使用するかどうかを判断できるようにする。

チャーチ数、任意の再帰型のエンコーディング（陽性条件）： &forall x. (F x -> x) -> x
継続、パターンマッチング： maybe、either、foldr

つまり、∀は、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

セクションの目標 = OOPにおける多態性とそれに関連するものの比較。型クラスの位置づけについて。

ad-hoc polymorphism = 型に応じて異なる振る舞いをすること。 => Haskellの型クラス。
parametric polymorphism = 実際に使用される型に無知。 => ∀
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.

セクションの目標 = 読者が自由定理を考えることができるようにすること。証明するな感じるんだ。

パラメトリック多相性の自由定理について

脚註[編集]

^ forall は Haskell 98 standard には含まれていないのだが、言語拡張ScopedTypeVariables, Rank2Types or RankNTypesのいずれにも含まれている。将来のHaskell標準にもこれらのうちどれかが対応するだろう。
^ 拡張UnicodeSyntaxを利用すれば、forallキーワードの代わりにこの記号を使用できる。
^ もちろん、2階型だけが必要ならRank2Typesで構わない。
^ テンプレート:Cite paper