Skip to content

Instantly share code, notes, and snippets.

@yhara
Created April 17, 2013 02:52
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save yhara/5401423 to your computer and use it in GitHub Desktop.
Save yhara/5401423 to your computer and use it in GitHub Desktop.

参照:http://route477.net/d/?date=20130417#p01

Reading: How to make ad-hoc polymorphism less ad hoc

Haskellの型クラスに関する論文を読みます。 自分のためのメモや写経であって、要約ではありません(興味のないところは省いたりしています)。

わりと分かりやすい内容なので、Haskellのclassとinstanceの書き方を分かってる人なら上から順に読んでいけば読めると思います。実装にだけ興味あるなら3章から読めばいいです。

メモ

  • メソッドを保持する型を定義する
    • 例:numDInt = NumDict addInt mulInt negInt
  • 任意のNumについて振る舞う関数(例:square)は、このメソッド一覧を第一引数にとる補助関数を経由して呼び出すように変換する

Abstract

Philip Wadler and Stephen Blott University of Galsgow

October 1988 (発表は1989/01)

http://homepages.inf.ed.ac.uk/wadler/topics/type-classes.html

  • この論文ではad-hoc多相を実現する新しい方法、型クラスを提案するよ
  • 型クラスのinformalな紹介をしたあと、推論規則でformalに規定するよ

1 Introduction

  • ad-hocとparametricという用語は[Str67]で命名された。

    • ad-hoc多相: 33 と 3.143.14 とか。(= 実装が違う)
    • parametric多相: length [1,2,3] と length [1.1, 2.2, 3.3] とか。 (= 実装は同じ)
  • parametric多相はHM型システムでいける。SML, Miranda等 一方ad-hoc多相に関しては一般的な方法がない(88年当時)。

  • この論文ではHM型システムを拡張して型クラスを導入する ad-hocとparametricを共存させる

  • このシステムは、HM型システムの拡張 型は推論されるので省略することができる オーバーロードを使わない、HM型システムで推論可能なプログラムに変換できる (なので、プリプロセッサで既存の言語に落とすとかが可能)

  • 本体:型クラスの説明と変換規則 付録:formalな推論規則 (= 型クラスのsematics)

  • ad-hocの問題が持ち上がった2つの点:arithmeticとequality

  • 型クラスは、OOPやbounded qualification、抽象データ型の問題と関連している

  • よく似たシステムが[Kae88]で提案されているが、いくつか改善している

  • 2: MLとMirandaのad-hoc多相の制限を紹介する(motivation)

  • 3: 型クラスを簡単な例で紹介

  • 4: 3の例がどう変換されるか

  • 5: ふたつめの例、equality

  • 6: subclassについて

  • 7: 関連情報と結論

  • 付録A: 推論規則と変換規則

2 ad-hoc多相のlimitation

SMLとMirandaの算術とequalityを例に取る

Arithmetic

  • 掛け算の演算子()がintとfloatにオーバーロードされていれば、 「33」「3.14*3.14」と書くことができる

  • が、両方に対応した「square x = xx」のような関数は書けない (IntIntなのか、Float*Floatなのかわからない)

  • 案1: オーバーロードされたInt版squareとFloat版squareを宣言したものと見なす

    • これは (squares x, square y, square z)みたいな式の型の可能性が爆発する
  • 案2: 算術演算子のオーバーロードをやめる(Miranda)

Equality

  • overloaded
    • 初期のSML
    • 1 == 2や'a' == 'b'を許すが、「==が使える任意の型」のような書き方はできない
  • fully polymorphic
    • Miranda
    • ==をa -> a -> Boolとする
    • しかしfunc1 == func2みたいなのが実行時エラーに
    • abstract typeを比較しようとした場合も良くないことになる
  • partly polymorphic
    • a(==) みたいな型を考え、==をa(==) -> a(==) -> Boolとする
    • a(==)は「==が使えるようなある型」の意
    • memberは[a(==)] -> a(==) -> Boolという型になる
    • SMLで使われているアプローチ
      • ''aと書く (eqtype variable)
      • 実装上の必要性から導入された?

OOP

からヒントを得たらしい。

3 An introductory example

例。

  • (+), (*), negateをIntとFloatに対して多重定義したい
    • Numという型クラスを定義
class Num a  where
  (+), (*) :: a -> a -> a
  negate :: a -> a
instance Num Int where
  (+) = addInt
  (*) = mulInt
  negate = negInt
instance Num Float where
  (+) = addFloat
  (*) = mulFloat
  negate = negFloat

square :: Num a =>  a -> a
square x = x * x

squares :: Num a, Num b, Num c =>  (a,b,c) -> (a,b,c)
squares (x, y, z) = (square x, square y, square z)

(まあまんまHaskellですね)

addIntはInt -> Int -> Intとか、そういう型だと思いねぇ。

4 Translation

このNumを、型クラスのない世界に変換します。

data NumD a = NumDict (a -> a -> a) (a -> a -> a) (a -> a)

add (NumDict a m n) = a
mul (NumDict a m n) = m
neg (NumDict a m n) = n

numDInt :: NumD Int
numDInt = NumDict addInt mulInt negInt
numDFloat :: NumD Float
numDFloat = NumDict addFloat mulFloat negFloat

-- square :: Num a =>  a -> a
-- square x = x * x
square' :: NumD a -> a -> a
square' numD x = mul numD x x

squares' :: (NumD a, NumD b, NumD c) -> (a,b,c) -> (a,b,c)
squares' (numDa, numDb, numDc) (x, y, z)
  = (square' numDa x, square' numDb y, square' numDc z)
  • 個々の型クラス(例:Num)に対して新しい型(例:NumD)を定義する
    • NumDは、OOPでいう「メソッド一覧」を保持するもの
    • 関数add, mul, negは、NumDから実際のメソッド(関数)を取り出して返す
  • instance宣言は、NumDを生成するコードに置き換えられる
    • NumDict addInt mulInt negInt とか、NumDict addFloat mulFloat negFloat みたいにして生成する
  • メソッドを使ったコード、例えば「x*x」は、「mul x x」に置き換えられる。
    • の部分には、適切なNumDが入る
    • 例:「3*3」なら「mul numDInt 3 3」
    • 例:「3.14*3.14」なら「mul numDFloat 3.14 3.14」
      • (これはコンパイル時に「mulFloat 3.14 3.14」に最適化することができる)
  • squareのように、Numの任意のインスタンスについて書かれた関数の場合は:
    • 引数を一つ増やした補助関数、square'を定義する(第一引数にNumDをとる)
    • squareの呼び出しを、square'の呼び出しに置き換える
    • 例:「square 3」なら「square' numDInt 3」
    • 例:「square 3.2」なら「square' numDFloat 3.2」

5 equalityの例

今度はequalityを型クラスで実現するよ。

-- 型クラスEqを宣言。Eqは、(==)が定義されているもの
class Eq a  where
  (==) :: a -> a -> bool

-- IntとCharはEqのインスタンスだよと宣言する
-- (eqIntとeqCharは既にどっかにあるとする)
instance Eq Int   where (==) = eqInt
instance Eq Char  where (==) = eqChar

-- 任意のEqな値を扱うような関数memberを定義してみるよ
-- (\/って見たことない演算子だけどorかな?)
member :: Eq a =>  [a] -> a -> Bool
member [] y = False
member (x:xs) y = (x == y) \/ member xs y

-- 2つ組の同値性を定義するよ
-- (instance宣言にも=>が使えるという例。言い換えれば、
-- 「もしa,bに同値性が定義されていれば、(a,b)にも同値性が定義できる」ということ)
instance Eq a, Eq b =>  Eq (a, b) where
  (u, v) == (x, y)  = (u == x ) & (v == y)

-- リストの同値性を定義するよ
-- (「もしaに同値性が定義されていれば、[a]の同値性も定義できるよ」)
isntance Eq a =>  Eq [a] where
  [] == []  = True
  [] == y:ys = False
  x:xs == [] = False
  x:xs == y:ys = (x == y) & (xs == ys)

-- ユーザ定義の型に対して同値性を定義してみるよ
-- ・Set自身は任意の型aをとれるけど、
--   Setの同値性が定義できるのは、aの同値性が定義されているときに限るよ!
-- ・aに同値性が定義されてるという条件下だから、member関数が使えるよ
data Set a = MkSet [a]
instance Eq a =>  Eq (Set a) where
  MkSet xs == MkSet ys  = and (map (member xs) ys)
                        & and (map (member ys) xs)

5.1 変換後

-- 型クラスEqのメソッド群を保持するデータ型(EqD)を定義するよ
data EqD a  = EqDict (a -> a -> Bool)
-- EqDからメソッドを取り出すアクセサ関数を定義するよ
eq (EqDict e) = e
-- Int用とChar用のメソッド群を定義するよ
-- (これは変換前のinstance宣言に相当)
eqDInt  = EqDict eqInt
eqDChar = EqDict eqChar

-- member用の補助関数を定義するよ
-- 第一引数にメソッド群を渡すようになっているよ。
-- member関数の呼び出しは、member'の呼び出しに置き換えるよ
member' :: EqD a  -> [a] -> a -> Bool
member' eqDa []     y = False
member' eqDa (x:xs) y = eq eqDa x y \/ member' eqDa xs y

-- (a,b)用のメソッド群を定義するよ。a,b用のメソッド群をeqDa,eqDbとするよ
-- (a,b)を比較するメソッドは、eqPair関数に部分適用して作るよ
eqDPair (eqDa,eqDb) = EqDict (eqPair (eqDa,eqDb))
-- (a,b)の比較関数の定義だよ。
-- もとがEq (a,b)のインスタンス宣言なので、第一引数が(eqDa,eqDb)になってるよ
eqPair (eqDa,eqDb) (x,y) (u,v) = (eq eqDa x u) & (eq eqDb y v)

-- [a]用のメソッド群を定義するよ。
-- これも、実際のメソッドはeqListに部分適用して作るよ
eqDList eqDa = eqDict (eqList eqDa)
-- [a]の比較関数の定義だよ。
eqList eqDa [] [] = True
eqList eqDa [] (y:ys) = False
eqList eqDa (x:xs) [] = False
eqList eqDa (x:xs) (y:ys) = (eq eqDa x y) & (eq (eqList eqDa) xs ys)
  -- ここの (eq (eqList eqDa) xs ys) は、対象がリストだと分かっているので、コンパイル時に
  -- (eqList eqDa xs ys) に最適化できる

6 サブクラス

  • Numのインスタンスは必ずEqでもあるようにしたい
  • class宣言にも「=>」を使えるようにする
class Eq a =>  Num a where
  (+) :: a -> a -> a
  (*) :: a -> a -> a
  negate :: a -> a
  • 「Numなら必ずEq」が成り立つので、NumはEqのサブクラス・EqはNumのスーパークラスという

  • Num Intを宣言したいなら、Eq Intも宣言する必要がある

  • このとき、「Eq a, Num a =>」と書くのは冗長なので

    memsq :: Eq a, Num a => [a]->a->Bool -- 以下のように書いてもよいことにする memsq :: Num a => [a]->a->Bool

型クラスは、スーパークラス・サブクラスをそれぞれいくつでも持てる

   Top
  /   \
Left Right
  \   /
  Bottom

class           Top a   where fun1 :: a -> a
class Top a =>  Left a  where fun2 :: a -> a
class Top a =>  Right a where fun3 :: a -> a
class Left a, Right a => Bottom a where fun4 :: a -> a

多重継承はOOPだと問題の種になったりするけど、 今回のような型クラスシステムでは特に問題にならない

7 Conclusion

  • インスタンスメソッドが満たすべき性質を記述できるような拡張も考えられるよね
  • 定数のオーバーロードも考えられる(Numにzero, one :: aを追加するとか)
    • が、zeroと書いただけではIntなのかFloatなのか分からなくなることも
    • このへんをうまくやるにはcoersionが要りそう
  • 型クラスは複数の型をとってもいい(class Foo a bみたいな)
    • これは、型クラスとbounded quantificationやsubtypeの関係を示唆している(?)
    • 型クラスはbounded quantifierの一種と考えられるが、暗黙の型変換はしない
  • 型クラスはabstract data typeの一種とも考えられる
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment