導入

算術演算、等値比較演算、値の文字列表示演算は言語設計上の難問
→何らかの形式の多重定義が利用される
→最良の方式は何か？

前提

Hindley/Milner型システム（型推論が利用できる総称型）に限定

現状の例

l 1つの言語でも演算子ごとに取り扱いが異なる。
例: Miranda: 算術演算を行う型は１種、等値演算は全ての型で多態､show関数は新しい型毎にユーザーによって多重定義される。

l 同一の演算子でも言語によって扱いが異なる。

l 1つの言語でも時に応じて同一の演算子の扱いが異なる。
例: SMLは全ての単態な型ごとに多重定義だったが、第2版では等値型の変数を導入

Haskellでの解決策: Type Class

l 多重定義に対する統一的な枠組み

→ 多くの改良と幾つかの批判があった。

批判

l principal typeに関する結果（完全性）が弱い形でしか成り立たない。（完全性: 型付けが可能な式については、principal typeが見つけられる。）

l 型のsemanticに関する健全性が失われる。（健全性:　型付けが見つかったらそれは正しい型付け）

Hindeley/Milner型システム

l 型付けできるプログラムは最も一般的な型（Principal Type）を持つ。

l 型付け可能なプログラムから型宣言を取り除いても型付け可能
→ 型宣言不要（型推論の根拠）
← 型付けできないプログラムには意味がない。

Type ClassとHindley/Milner型システム

l 型宣言を取り除くと曖昧になって型付けできないことがある。
← プログラムに対して意味がある型付けが多すぎる。

制限されたType Class

例1(Haskell):

class (Num a) where

(+) :: a -> a -> a

(*) :: a -> a -> a

neg :: a -> a

fromInteger :: Integer -> a

class (Eq a) where

(==) :: (Eq a) => a -> a -> Bool

class (Text a) where

show :: a -> String

showList :: [a] -> String

read :: String -> a

制約

型変数aのType Classについて多重定義された演算子の型をa -> t（ここでtはa自身を含んでもよい）の形式に制限する。

（例：class Numの+, *, neg）（[Kae88]で提案されたParametric Overloadingはこの形式の多重定義を指す。）

得失

l 曖昧さがなくなり、型宣言の省略が可能になる。

l → 健全性が復活し、principal typeが元の強力さ（完全性）を取り戻す。

l ただし以下の用途には力不足

l 数値定数の取り扱い

l 文字列を値として読み込む演算の取り扱い（例：class Textのread演算）

l 前者に比べて後者はあまり本質的な問題ではない（MirandaもSMLもサポートしていない。）

[]==[]の取り扱いとundef

一般化されたType Class

例2(Haskell):

Class (Pointed a) where

xcoord :: a -> Float

data Point = MkPoint Float Float

data Cpoint = MkCPoint Float Float Colour

instance Pointed Point where

xcoord (MkPoint x y) = x

ycoord (MkPoint x y) = y

instance Pointed Cpoint where

xcoord (MkCPoint x y c) = x

ycoord (MkCPoint x y c) = y

distance :: (Pointed a) => a -> Float

distance p = sqrt (sqr (xcoord p) + sqr (ycoord p))

bounded 多相との関係

l type classは型変数を多重定義がなされている一定の範囲に束縛する。
→ 型変数を、与えられた型の部分型に束縛するbounded 多相と深い関係がある。
→ type classを通常のrecord型のsubtypingに利用することができる。しかし単相なrecordにしか通用しない。

l ↑の例で、PointについてもそのsubtypeであるCPointについてもdistanceではtype class Pointedを通じて型付け（type signatureなしで）できる。しかし、これは各フィールドが単相型（ここではFloat）を持っていることに依存している。
→ type classの宣言を廃止する。一群の演算子がクラスに属するとする代わりに、単に多重定義されているとだけ宣言する（演算子の型については宣言しない。）。

例3(Haskellもどき)

over xcoord

over ycoord

data Point = MkPoint Float Float

data Cpoint = MkCPoint Float Float Colour

inst xcoord :: Point -> Float

xcoord (MkPoint x y) = x

inst xcoord :: Point -> Float

ycoord (MkPoint x y) = y

inst xcoord :: CPoint -> Float

xcoord (MkCPoint x y c) = x

inst xcoord :: CPoint -> Float

ycoord (MkCPoint x y c) = y

distance :: (xcoord, ycoord::a -> Float) => a -> Float

distance p = sqrt (sqr (xcoord p) + sqr (ycoord p))

例4(Haskellもどき)

over first

over second

over third

inst first :: (a, b) -> a

first (x, y) = x

inst second :: (a, b) -> b

second (x, y) = y

inst first :: (a, b, c) -> a

first (x, y, z) = x

inst second :: (a, b, c) -> b

second (x, y, z) = y

inst third :: (a, b, c) -> b

third (x, y, z) = z

demo :: (first :: a -> b, second :: a -> c) => a -> (c, b)

demo r = (second r, first r)

型宣言の廃止によって・・・

l bounded 多相型のモデルになりうるほど強力になった。
（従来のtype classでは書けなかった↑の例4が記述できるようになる。）

l 前もってクラスに含まれる演算を決定する必要がなくなった。
（例：例４でthirdを前もってではなく、追加したいときに追加できるようになった。またHaskellのNumが備える+や*は環ringが備えるべきかもしれないという議論もある。）

l 型の推論はより煩雑になった。（多重定義されている全ての演算子の型に注意を払う必要がある。recordを利用して関連した演算を集め、それら全体で共通の識別子を利用できる。詳しくは後述。）

contribution

以上のtype classの制限版と一般化を踏まえて、以下のような性質を持った型システムOを提案する。

l 型なしの動的なsemanticsを備え、型の健全性に関する定理が成り立つ。

l 型宣言を省略されてもprincipal typeを見つけることができる。

l 型システムOで正しく型付けされたプログラムをHindley/Milner型システムで正しく型付けされたプログラムへ変換するstandard dictionary transformが存在する。

l F-bounded形式に制限されたrecordの多相型（多相なrecordを含む）のモデルに十分なほど強力

型システムO

文法はFig.1（[Mil78]のExpと基本的には同じ。）

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

拡張部分

l 規則[∀I]では型式とtypothesysの間で（多重定義の）制約が受け渡される規則[∀E]は制約が除去されていることを前提にしている。規則[SET]によって制約は引き継がれる。このため[∀I]と[∀E]が[→I]と[→E]に対称となることに注意。

l 規則[INST]は [LET]に似ているが多重定義する変数oについては型式σTを明示することが必要。

例5（オブジェクト指向的デモ「集合クラス」）

type Set a aa = {union, inters, diff :: aa-> aa, member :: a-> Bool}

inst set :: ((==)::a->a->Bool)=> [a] -> Set a [a]

set xs =

{

union = \ys -> xs ++ ys,

inters = \ys -> [y | y <- ys | y 'elem' xs],

diff = \ys -> xs \\ ys,

member = \ y -> y 'elem' xs

}

inst set :: ((==)::a->a->Bool)=> Tree a -> Set a (Tree a)

set = …

union :: (set: sa -> Set a aa) => sa -> sa -> sa

union xs ys = #union (set xs) ys

diff :: (set: sa -> Set a aa) => sa -> sa -> sa

diff xs ys = #diff (set xs) ys

simdiff :: (set: sa -> Set a aa) => sa -> sa -> sa

simdiff xs ys = union (diff xs ys) (diff ys xs)

Semantics

Fig.3参照。

Wは型エラーを示す値（Wに関数を適応した結果は関数の適用がstrictならばW）。

＜健全性の証明は省略。＞

変換

型システムOからHindley/Milner型システムへの"Dictionary Passing"変換。

変換の基本的なアイディア

Fig.4参照。

∀α.πα⇒τという項→πα内の多重定義の変数を実現する引数列（dictionary）を取る関数（instはletに変換される。）

型と型式の変換

τ* = τ

（∀α.ε⇒σ）* = ∀α.σ*

（∀α.o:α→τ, πα⇒σ）* = ∀α(α→τ)→,（∀πα⇒σ）*

束縛、typothesysの変換

(u:σ)* = u:σ*

(o:σ)* = uoσ:σ* （新たな変数の導入）

(o1:σ1, … ,on:σn)* = (o1:σ1)*, … ,(on:σn)*

semanticsの保存

この変換はsemanticsを保存することは正しい要求だが、証明は自明ではない。同じく整合性も証明はトリッキーである[Blo91][Jon92a]。

Recordの型付けとの関係

Fig.1,Fig.2にFig.5の文法と型付け規則を追加して拡張。

（[Oha92]による。更新と拡張は簡単のため省略。）

l レコード項とレコード型の"{}"とラベル、選択関数の定義(文法と型付け規則)

l 部分型を示す述語"≦"定義（文法と型付け規則）。

型の再構成（型推論）

MilnerのアルゴリズムW[Mil78]を以下の2点で拡張

l 単一化の際に制約Γαを守るように単一化unifyを改良。mkinst（総称に対するインスタンス作成）がそれを行う。

l 型付けtpはインスタンス宣言inst o:σT=e in pを扱うように拡張されている。この場合、多重定義項eから推論されたσT'が与えられたσTよりも総称的でないことを確かめねばならない。

unifyとmkinstの停止性はσTの形状に依存する。

結論

l 多重定義と多相record（F-bounded多相の形式に制限された）をサポートするようにHindley/Milnerの型システムを若干拡張した型システムOの提案。

l 型システムOは健全性を持つ（証明）。

l 型システムOではprincipal typeを再構成できる（証明とアルゴリズム）。

将来の課題

l 型システムO内での多相recordの取り扱いからF-bounded多相と多重定義は深い関係にあることが示された。（bounded多相型に対してのtype classの辞書変換とPenn変換の類似からも同じことが言える。）

導入

前提