Type Classes with Functional Dependencies
multi-parameter type classを定義する際に生じる問題点と、それを解決するためのFunctional Dependenciesについて
複数の型引数間の関係性をどう表現するか
2000/3
大まかな流れ
1 Introduction
普通のHaskellの型クラスの概要
multi-parameter type classの概要と、それが一般的であるにも関わらず標準仕様に含まれていないということについて
なぜなら、型引数間の依存関係をcaputureできないから、という問題提議
2 Preliminaries: Type Classes in Haskell
型クラスの定義、型クラス制約、型クラスの継承、インスタンスなど基本的なことについて
3 Example: Building a Library of Collection Types
Collects型クラスを例に取って、実際にどういう問題が生じるのかを具体的に見る
hsclass Collects e ce where
empty :: ce -- 空のcollectionを作成
insert :: e -> ce -> ce -- 追加
member :: e -> ce -> Bool -- 存在確認このクラス宣言には3つの問題が存在する
①
empty の型が曖昧②型推論が正しくできないために、Collectsが異なる型の要素を持ててしまう
③コンパイルエラーは生じないが、実行時エラーが生じる
上述の①~③の問題を解決できる3つの解決案の提示
1つ目: Collectsの型引数を
e と c にするhsclass Collects e c where
empty :: c e
insert :: e -> c e -> c e
member :: e -> c e -> Boolしかし、これは最初の定義ほど抽象的ではないため、最初の定義ではインスタンスにできた型のいくつかがインスタンスに取れなくなる
2つ目: パラメトリック多相な型クラスにする
hsclass ce ∈ Collects e where
empty :: ce
insert :: e -> ce -> ce
member :: e -> ce -> Bool「
ce が、 Collects e のmemberである」という制限を設ける構文がキモいからか、何故か知らんがスルーされたらしい
3つ目: functional dependenciesを使う(本題)
hsclass Collects e c | c -> e where
empty :: c
insert :: e -> c -> c
member :: e -> c -> Bool拡張構文としても良い感じ
4 Further Examples
標準の
(*) をもっと柔軟にする例の紹介有限集合の例の紹介
5 Relations and Functional Dependencies
6 Typing with Functional Dependencie
Functional Dependenciesに関する型推論の理論
7 utting a Name to Functional Dependencies
Functional Dependenciesした型クラスを継承した時とかの話
8 Conclusions and Future Work
将来の作業
面白そうな関連論文
Functional Dependenciesの理論は、RDBのためのアイディアが元にあるとのことで、RDBに関する論文等が引用されていた
参考
この論文を軽く読んだっぽい人のブログ記事
>読みメモ
>A particular novelty of this paper is the application of ideasfrom the theory of relational databases to the design of type systems.
RDBとどう関係してくるのか気になる
1 Introduction
More generally, functions in Haskell have types ofthe formP⇒τ, wherePis some list of predicates andτis a monotype. IfPis empty, then we usually abbreviateP⇒τasτ.
型クラス制約
=> を型クラスもカリー化できる
ということは複数の型引数を取りうる
For example, what might a predicate of the form
R a b mean, where two parameters a and b have been provided? The obvious answer is to interpret R as a two-place relation between types, and to read R a b as the assertion that a and b are related by R .位置引数のときがa \in \mathrm{Eq}なので、
2引数になったら「 集合SとT上の二項関係Rに対して、(s,t) \in Rのことをs R tと記述する」的な話
という意味で、自然な一般化
So it is perhaps surprising that support for multiple parametertype classes is still not included in the Haskell standard, even in the most recentrevision . One explanation for this reticence is that some of the proposed applications have not worked particularly well in practice. These problems oftenoccur because the relations on types that we can specify using simple extensionsof Haskell are too general for practical applications. In particular, they fail tocapture important dependencies between parameters.
More concretely, the useof multiple parameter classes can often result in ambiguities and inaccuracies ininferred types, and in delayed detection of type errors
multi-parameter type classが色々使われているのに標準には含まれていない
その理由は、これまでに提案されてきたアプリケーションのいくつかがちゃんと機能してないから
この型の関係は実際のアプリケーションには一般的すぎる
特に型引数間の依存関係をキャプチャできない
まさにFunctional Dependenciesが無いことに対する問題意識
2 Preliminaries: Type Classes in Haskell
型クラスの定義、型クラス制約、型クラスの継承、インスタンスなど基本的なことについて
3 Example: Building a Library of Collection Types
Collection型クラスで複数引数の型クラスの問題を見る
Collectionを扱う型クラス
hsclass Collects e ce where
empty :: ce -- 空のcollectionを作成
insert :: e -> ce -> ce -- 追加
member :: e -> ce -> Bool -- 存在確認ちなみに、この定義は拡張なしではコンパイルエラーになる
例えば、List, characteristic functions, BitSet, hash tableとかが、インスタンスになる
hsinstance Eq e => Collects e [e] where
empty = []
insert = (:)
member = elemこのクラス宣言には3つの問題が存在する
①
empty の型が曖昧型クラス制約を用いて書けば
empty :: Collects e ce => ce となるが、 => の左辺にある e が、右辺に出てこない右辺に出てこない型が左辺に存在することを「曖昧」と読んでいる
無理やり解決する方法は、emptyの定義をCollectsの定義から消すこと
>The problem with this is that, accordingto the theoretical foundations of Haskell overloading, we cannot guarantee a well-defined semantics for any term with an ambiguous type
何でこれが問題なのかわからん #??
この辺に書いてるらしい
②Collectsが異なる型の要素を持ててしまう
Collectsの
insert を用いてこういう2つの関数を定義するhsf x y coll = insert x $ insert y coll
g coll = f True 'a' coll insert の型定義的に、 f の引数 x , y は同じ型のはず g を見ると、BoolとCharをcollに追加しているこれは以下のように推論されて型検査を通過してしまう
hsf :: (Collects a c, Collects b c) => a -> b -> c -> c
g :: (Collects Bool c, Collects Char c) => c -> c f の要素は別々の型 a , b でも良い、と推論されるCollectsは同じ型のCollectionがほしかったはずなのにこれでは都合が悪い
③これらの関数は定義時には型エラーが出ないが、実行時に都合がわるいことになる
よって、どうにかして
型の曖昧さの排除
正しい型推論
型エラーの早期検出
つまり、定義時に間違いにきづけるように
したい
1詰めの解決法
Collectsの型引数を
e と c にするhsclass Collects e c where
empty :: c e
insert :: e -> c e -> c e
member :: e -> c e -> Bool型引数が、
e と c になっているリストで言えば、
元々
e と [e] だったものが、 e と [] に変わってる感じこれで上の3つの問題は解決する
①emptyの型は、
empty :: Collects e c => c e になり「曖昧」ではなくなった②上の関数
f は、 f :: (Collects e c) => e -> e -> c e -> c e と適切に型推論されるなぜ #??
Hindley-Milner型推論ちゃんと理解していないと、この辺は完全に理解できないな
③上の関数
g は型エラーになる②の結果により、
f は異なる型の値を受け付けないから定義時にエラーを検出できる
しかし、これまた問題がある
先の4つの例の内、Listしかinstanceにできない
2つ目の解決法
パラメトリック多相な型クラスにする
PTCと呼んでる
parametric type classes
hsclass ce ∈ Collects e where
empty :: ce
insert :: e -> ce -> ce
member :: e -> ce -> Bool「
ce が、 Collects e のmemberである」という制限を設けるmemberってなに #??
e が決まるごとに、 Collects e という型クラスが決まる感じType Classes with Functional Dependencies#60982e901982700000fa5c8dのときと同じ様に4つの型のインスタンスを取れる
What makes it different from the two parameter class in Sec-tion 3 is the implied assumption that the element type e is uniquely determinedby the collection type ce.
上の①~③のような問題も起きない
定義の構文の問題などでスルーされたらしい
In part, this may be because it was seen,incorrectly, as an alternative to constructor classes and not, more accurately,as an orthogonal extension.
functional dependenciesを使う
本題
parametric type classesの一般化、として見るのか
hsclass Collects e c | c -> e where
empty :: c
insert :: e -> c -> c
member :: e -> c -> Bool c -> e という注釈をつける拡張構文としてもマシ
型クラスの定義のみの変更であって、instance宣言や型クラス制約には影響がない
一般的には
c も e も複数の型を指定できる(x_1,\cdots, x_n) \to (y_1,\cdots,y_m)
yが、xによって一意に決定される
この定義は、\{a\to b , b\to a\}などのような相互依存関係も表現できるのでPTCよりも厳密に一般的
やっぱこれで相互だよな
どこかの記事で全射っぽい説明してたけどあれなんだったんだ
例
hsclass C a b where ..
class D a b | a -> b where ..
class E a b | a -> b, b -> a where ..Cは二項関係
Dは、(部分)関数であることを示す
ただの二項関係ではない
それよりも制限がかかっている
Eは、全単射であることを示す
こうすれば、以下の様に書くとエラーになる
なる、というか、コンパイラはエラーにしないといけない
hsinstance D Bool Int where ...
instance D Bool Char where ...どちらか片方の定義なら許容するが、両方の定義は許容されない
D Bool なんか の なんか の部分は一意的でないといけないこれもエラー
hsinstance D [a] b where ... a , b には何かの具体型を入れている時の話をしているThe problem here is that this instance would allow one particular choice of
[a] to be associated with more than one choice for b , which contradicts the dependency specified in the definition of D . wakaran
section4
さらなる例
標準の
(*) をもっと柔軟にする今は
(*) :: Num a => a -> a -> a という型なので、Int * Floatみたいなことはできないhsclass Mul a b c | a b -> c where
(*) :: a -> b -> c
instance Mul Int Int Int where ..
instance Mul Int Float Float where ..
instance Mul Float Int Float where ..
instance Mul Float Float Float where ..この型クラスは、fun depがなかったら
(1 * 2) * 3 のような単純な式でも型推論似失敗する (1 * 2) * 3 :: (Mul Int Int a, Mul a Int b) => b fun depsの情報があるおかけでちゃんと推論される
有限集合の例など
section5
fun depsの基本理論
RDBのためのアイディアが元
section6
型推論の理論の話
section7
we describe some further opportunities for using dependency information
さらなるお話
fun depsした型クラスを継承した時とかの話
section8
将来の作業