論文紹介：
A Second Look at Overloading
神戸隆行
(1995年 7th International Conference on
Functional Programming and Computer
Architectureより)
概要
Hindley/Milner型システムの元での多重
定義
Type Class
Bounded多相とType Classの拡張
型システムO
Oの多相レコード拡張
型付け
1. 計算対象を演算の種類によって型へ分類
2. プログラム内の対象の型を通じてそれらの
関係を調べ、プログラムの正しさを検証す
る
型：
値の集合とそれらの関係を表す演算の集合の対で表さ
れる構造。関数型言語では複数の値の集合を対応付け
る関数自身を値として扱う型が備わる。
強い型付け
型の関係に矛盾がないかどうかを検証す
る
全ての型が具体的に確定しなくても検査が
行える
変数の型と実行時における実際の型の分離
→多相の実現に利用
例）多重定義、継承、総称
Hindley/Milner型システム
総称型
型変数（パラメータ）を含む型を持つ変数の定義を許
す（→principal type）
実行時には型変数の中身は確定している必要あり
Hindley/Milner型システムでは型の宣言を省略
してもプログラムからprincipal typeを再構成でき
る →積極的に省略
煩雑な型指定が不要 →指定に起因するミスがなくな
る
例：Haskell
id :: a -> a
id x = x
length :: [a] -> Integer
length [] = 0
length (x:xs) = 1 + length(xs)
多重定義の必要性
算術演算、比較演算、文字列への変換
概念的に共通 →型定義は総称的
しかし・・・
データの表現や計算手続きの構造などの実現は具体
的な型毎に大きく異なる →型変数では表現し難い
総称的な定義は不適切（例： リストやツリーなどの
等値比較）
総称的な定義は不可能（例: 固定長整数と浮動小
数点数の算術演算)
案1：単純な多重定義
単純に多相な関数の多重定義を許すと
完全性が失われる
Principal Typeを見つけたと思っても正しくない可
能性
健全性が失われる
Principal Typeとして複数の「正しい」候補があって
決定できない可能性
案2：Type Class
1.
型変数に付けられる「クラス」を宣言
クラスに属する関数の名と型の宣言を含む
クラスに属する関数が適用されている変数で
は、型推論を具体的な型の定義が存在する範
囲に制限（呼び出し側）
3. 決定した型に基づいて適切な関数定義を選択
（呼び出され側）
例： (レジュメ例1）
Haskellで利用されている
2.
案3: 制約されたType Class
多重定義関数の型をa -> t（tはa自身
を含んでもよい)の形式に制限
(Parametric Overloading [Kae88])
(+)曖昧さ解消、型宣言の省略が可能になる
健全性
完全性
(-)表現力不足
数値定数
文字列からの変換演算
Bounded多相とType Class
type classは型変数を多重定義がなされ
ている一定の範囲に束縛
型変数を、与えられた型の部分型に束縛す
るbounded 多相と深い関係がある
2. type classを通常のrecord型のsubtypingに
利用 → しかし単相なrecordのみ
1.
Type Classによるsubtyping例
例（レジュメ例2）
PointについてもそのsubtypeであるCPointに
ついてもdistanceではtype class Pointedを通
じて型付け可
しかし、これは各フィールドが単相型（ここでは
Float）を持っていることに依存
案4: 拡張されたType Class
Type Classの宣言を廃止
一群の演算子がクラスに属すると宣言しない
ある演算子が多重定義されているとだけ宣言
型については具体例を定義する際に宣言
例（レジュメ例3、4）
例3・・・例2の書き直し
例4・・・多相レコードの記述
拡張されたType Classの得失
(+)bounded 多相型のモデルになりうるほど強
力
(+)前もってクラスに含まれる演算を決定する必
要がない
例4が記述可能
例： 例４でthirdを追加したいときに追加可能
(-)型推論は煩雑化
多重定義されている全ての演算子に注意が必要
拡張されたType Classとオブジェ
クト指向
拡張された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の間で（多重定
義の）制約が受け渡される
規則[∀E]は制約が除去されていることを前提に
している
規則[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）
＜健全性の証明は省略。＞
© Copyright 2024 ExpyDoc
