論文紹介： A Second Look at Overloading 神戸隆行 (1995年 7th International Conference on Functional Programming and Computer Architectureより)

概要 Hindley/Milner型システムの元での多重定義 Type Class Bounded多相とType Classの拡張

型付け 計算対象を演算の種類によって型へ分類 プログラム内の対象の型を通じてそれらの関係を調べ、プログラムの正しさを検証する 型： 値の集合とそれらの関係を表す演算の集合の対で表される構造。関数型言語では複数の値の集合を対応付ける関数自身を値として扱う型が備わる。

強い型付け 型の関係に矛盾がないかどうかを検証する 全ての型が具体的に確定しなくても検査が行える 例）多重定義、継承、総称 変数の型と実行時における実際の型の分離 →多相の実現に利用 例）多重定義、継承、総称

Hindley/Milner型システム 総称型 型変数（パラメータ）を含む型を持つ変数の定義を許す（→principal type） 実行時には型変数の中身は確定している必要あり Hindley/Milner型システムでは型の宣言を省略してもプログラムからprincipal typeを再構成できる →積極的に省略 煩雑な型指定が不要 →指定に起因するミスがなくなる

例：Haskell id :: a -> a id x = x length :: [a] -> Integer length (x:xs) = 1 + length(xs)

多重定義の必要性 算術演算、比較演算、文字列への変換 概念的に共通 →型定義は総称的 しかし・・・ データの表現や計算手続きの構造などの実現は具体的な型毎に大きく異なる →型変数では表現し難い 総称的な定義は不適切（例： リストやツリーなどの等値比較） 総称的な定義は不可能（例: 固定長整数と浮動小数点数の算術演算)

案1：単純な多重定義 単純に多相な関数の多重定義を許すと 完全性が失われる 健全性が失われる Principal　Typeを見つけたと思っても正しくない可能性 健全性が失われる Principal Typeとして複数の「正しい」候補があって決定できない可能性

案2：Type Class 型変数に付けられる「クラス」を宣言 クラスに属する関数の名と型の宣言を含む クラスに属する関数が適用されている変数では、型推論を具体的な型の定義が存在する範囲に制限（呼び出し側） 決定した型に基づいて適切な関数定義を選択（呼び出され側） 例： (レジュメ例1） Haskellで利用されている

案3: 制約されたType Class 多重定義関数の型をa -> t（tはa自身を含んでもよい)の形式に制限 (Parametric Overloading [Kae88]) (+)曖昧さ解消、型宣言の省略が可能になる 健全性 完全性 (-)表現力不足 数値定数 文字列からの変換演算

Bounded多相とType Class type classは型変数を多重定義がなされている一定の範囲に束縛 type classを通常のrecord型のsubtypingに利用 → しかし単相なrecordのみ

Type Classによるsubtyping例 例（レジュメ例2） PointについてもそのsubtypeであるCPointについてもdistanceではtype class Pointedを通じて型付け可 しかし、これは各フィールドが単相型（ここではFloat）を持っていることに依存

案4: 拡張されたType Class Type Classの宣言を廃止 例（レジュメ例3、4） 一群の演算子がクラスに属すると宣言しない ある演算子が多重定義されているとだけ宣言 型については具体例を定義する際に宣言 例（レジュメ例3、4） 例3・・・例2の書き直し 例4・・・多相レコードの記述

拡張されたType Classの得失 (+)bounded 多相型のモデルになりうるほど強力 例4が記述可能 (+)前もってクラスに含まれる演算を決定する必要がない 例： 例４でthirdを追加したいときに追加可能 (-)型推論は煩雑化 多重定義されている全ての演算子に注意が必要

拡張されたType Classとオブジェクト指向 recordを利用して関連した演算を集め、それら全体で共通の識別子を利用可 例（レジュメ例5） オブジェクト指向のデモとしてのSet型

型システムO 以下のような性質を持った型システムOの提案 型宣言を省略されてもprincipal typeを再構成可 型なしの動的なsemanticsを備え、型の健全性に関する定理が成り立つ 型システムOで型付けされたプログラムをHindley/Milner型システムで型付けされたプログラムへ変換するstandard dictionary transformの存在 F-bounded形式に制限された多相record型のモデルに十分な強力さ

型システムOの文法と推論規則 文法はFig.1（[Mil78]のExpと基本的には同じ。） Fig.1の文法に沿った型付け規則はFig.2（[DM82]のHindley/Milner型システムと基本的には同じ。）

型システムOの拡張部分 規則[∀I]では型式とtypothesysの間で（多重定義の）制約が受け渡される 規則[SET]によって制約は引き継がれる このため[∀I]と[∀E]が[→I]と[→E]に対称となることに注意 規則[INST]は [LET]に似ているが多重定義する変数oについては型式σTを明示することが必要

Dictionary Passing変換 型システムOからHindley/Milner型システムへの変換（ Fig.4参照） 変換の基本的なアイディア ∀α.πα⇒τという項はπα内の多重定義の変数を実現する引数列（dictionary）を取る関数に変換（inst→let） この変換はsemanticsを保存するが、証明は自明ではない。同じく整合性も証明はトリッキー[Blo91][Jon92a]

Recordの型付け Fig.1,Fig.2にFig.5の文法と型付け規則を追加して拡張 レコード項とレコード型の“{}” （[Oha92]による。更新と拡張は省略。） レコード項とレコード型の“{}” ラベルと選択関数の定義 部分型を示す述語"≦"定義

型推論アルゴリズム MilnerのアルゴリズムW[Mil78]を以下の2点で拡張 単一化の際に制約Γαを守るように単一化unifyを改良 mkinst（総称に対するインスタンス作成）がそれを行う 型付けtpはインスタンス宣言inst o:σT=e in pを扱うように拡張 多重定義項eから推論されたσT‘が与えられたσTよりも総称的でないことを確認

初期の関連研究 多相なプログラミング言語における多重定義の研究…[Kae88][WB89] 記号代数（計算機代数）分野における研究…[JT81] 多重定義を関数に限るという制約に関して[Kae88]に影響

Haskell関連研究 Haskellのtype classの設計と実装に関連した研究…[NS91][NP93]（型の構成）[Aug93][PJ93]（実装）[HHPW94]（形式的な定義）

type classの拡張関連研究 複数の型変数を伴ったtype class…[WB89][Jon92b] 同上、ただし1変数以外は関数で制約…[CHO92] コンテナやrecordのモデルに利用…[Jon93]

環境関連研究 以上は一般に「開いた世界」で、インスタンスがないような空のtype classを許し、分割コンパイルに向く 空のtype class宣言を許さない「閉じた世界」…[Rou90][Smi91][Kae92] 「閉じた世界」と「開いた世界」の共存…[DO94] 上記の「開いた世界」の多くが健全でないことを証明…[Vol93]（しかし、この論文の型システムOは健全）

異なるアプローチの多重定義関連研究 type caseによる動的な型付けとしての多重定義…[DRW95][HM95] 上記のsemantics…[Tha94] 上記のsemanticsをXML類似の明示的な多相型言語へマップした例…[MH88]

まとめ 多重定義と多相record（F-bounded多相の形式に制限された）をサポートするようにHindley/Milnerの型システムを若干拡張した型システムOの提案。 型システムOは健全性を持つ。 型システムOではprincipal typeを再構成できる。

以上 2000.06.08

型システムOのSemantics Fig.3参照 Wは型エラーを示す値（Wに関数を適応した結果は関数の適用がstrictならばW） ＜健全性の証明は省略。＞