Classical set theory in Agda

Agda歴2週間くらいのザコです。 Agdaで圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。

標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているように見えるだけであんまり使い物にならない。
具体的に言うと和集合の公理がないので(binary cupとindexed bigcupはある)任意個のUnionがとれない。
他にも、そもそも∈の定義が函数適用なので X ∈ B と書いときにXとBでは型が違うのがすごくキモいとか。キモいというかこれのせいでZFの一部の公理は型があわなくて表現できなかったりもする。

そういうわけでまずは集合を使えるようにするというだけ。
コードは一番下に載っけました。

コードについて

二重否定除去

Relation.Nullary.Negation

elem

属するの演算と2つの公理。
elem-∈は(x : A)と(x ∈ A)がcompatibleになるように。
≡-∈は示せなさそうで必要になったから入れたけど本当に必要なんだろうか。よく分からない。

postulate
  _∈_ : Set → Set → Set₁
  elem-∈ : {A : Set} → ∀ x → x ∈ A → A
  ≡-∈ : {A X Y : Set} → X ≡ Y → X ∈ A → Y ∈ A

公理

仮定したのは以下。

• 外延性の公理
• 対の公理
• 和集合の公理
• 無限公理
• 分出公理
• 冪集合の公理

postulate
  extensionality : {A B : Set} → A ≡ B ⇔ Lift {_} {zero} (∀ x → (x ∈ A ⇔ x ∈ B))
  ∃-paring : ∀(A B : Set) → ∃ \(P : Set) → ∀ x → x ∈ P ⇔ (x ≡ A) ∨ (x ≡ B)
  ∃-union : (A : Set) → ∃ \(B : Set) → ∀ X → X ∈ B ⇔ (∃ \C → (C ∈ A) ∧ (X ∈ C))
  infinite : ∃ \A → (∅ ∈ A) ∧ (∀ X → X ∈ A → X ⁺ ∈ A)
  replacement : (A : Set) → (P : Set → Set₁) → ∃ \B → ∀ x → x ∈ B ⇔ (x ∈ A) ∧ P x
  powerset : (A : Set) → ∃ \B → ∀ X → X ∈ B ⇔ X ⊆ A

空集合の存在だけは(Data.Empty.⊥を使って)示せるので示した。

あとは命題の表現に便利そうな函数とか部分集合とか共通部分とか適当な補題を示したりした。
本に載っているままのやり方だけど

-- ``Russellのparadoxを回避"する命題。
cor-1-4 : (A : Set) → ∃ \B → B ∉ A

も示せた。

コメント

これだけのことが検索しても全くヒットしなくてつらかった。誰もAgdaで数学しないのかなって思った。

あと、仮定した公理が適切なものかどうかもよく分からない。なんか変なことしてたら教えてください。
選択公理とかも入れてもう少し綺麗にしてから自分のライブラリに入れて使おうと思います。

参考にした本

たまたま手元にあった。

集合と位相 (岩波基礎数学選書)

コード

https://gist.github.com/myuon/ea11f62f9a9a9fed02b0

Printf実装を通して学ぶGADTs, DataKinds, ConstraintKinds, TypeFamilies

問題

問. Haskellで以下のようなCライクなprintf函数を実装してください。

> printf ["Hello, ", _s, "\n", "an integer:", _d, "\n", "a float:", _f] ["World!", (10 :: Int), (3.1415 :: Float)] 

-- 出力結果:
> Hello, World!
> an integer:10
> a float:3.1415

Cのprinfとは異なり、%dや%fが文字列に直接埋め込まれていません。よって当然型が合わなければ、すなわち printf [_d] [(3.1 :: Float)] などとかくとコンパイルエラーになってほしいわけです。

解答

私が実装したものが以下にあります。

https://gist.github.com/myuon/9084939

以下ではこのコードについて解説していきたいと思います。

解説

まず、printfの第一引数も第二引数もそれぞれの元の型はバラバラです。今はまだ_dや_fの型をどうするかについては考えていませんが、とにかく型が違うということだけ分かればまずはヘテロリストの実装からスタートすることになります。

GADTs, DataKinds

ヘテロリストは全ての型がバラバラなので型を保持するのではなくてカインドを保持するようにします。つまり、普通のリストは型がaのデータを並べたものですが、今回実装するヘテロリストはカインドが*のデータを並べたものと考えます。

data HList (as :: [*]) where
  Nil :: HList '[]
  (:::) :: a -> HList as -> HList (a ': as)
infixr :::

HListの定義にはGADTとDataKindsが使われています。GADTはデータコンストラクタを函数のように定義できる*1もので、確かに上ではdata ... whereという書き方がされています。

DataKindsは定義したデータコンストラクタを型に、型をカインドに同じ名前のまま持ち上げるものです。分かりやすい例を挙げてみましょう。以下は簡単な型レベル自然数の例です。

data Nat = Zero | Succ Nat

-- DataKinds拡張を使うと、以下のようなものも自動で生成される
-- data Zero
-- data Succ (n :: Nat)
-- ただし Zero :: Nat, Succ n :: Nat である

これによって、標準的なリスト型は[]カインドに持ち上げられ、'[], (':)というデータコンストラクタを昇格してできた型が作られ、*カインドをもつ型のリストが使えるようになります。 このことを踏まえれば上のコードは、HListというデータ型の定義であって、asという変数はカインド*をもつ型のリストになっていることが分かります。(:::) :: a -> HList as -> HList (a ': as)によって、与えられた型をそのままリストに追加しているのが分かります。さらに実際に動かして型を調べてみるとよいでしょう。

> :t Nil
Nil :: HList ('[] *)

> :t "100" ::: (10 :: Int) ::: Nil
"100" ::: (10 :: Int) ::: Nil :: HList ((':) * [Char] ((':) * Int ('[] *)))

TypeFamilies, ConstraintKinds

さて、HListはShowのインスタンスにできるでしょうか。HListに登場する全ての型がShowのインスタンスであればできそうです。このように型への制限を表すのがConstraintで、それをカインドのレベルで扱えるようにするのがConstraintKinds拡張です。

import GHC.Prim (Constraint)

type family All (cx :: * -> Constraint) (xs :: [*]) :: Constraint
type instance All cx '[] = ()
type instance All cx (x ': xs) = (cx x, All cx xs)

TypeFamiliesを使えば型を直接扱う函数を定義できます。これによってAllという型への制限を表す函数を定義します。cx :: * -> Constraintの部分に適当な型クラスがきます。例えばAll Showは、カインド*のリストxsに対し、その全ての元がShowのインスタンスになっているという制限を表すことができるわけです。

コレを使ってHListをShowのインスタンスにしてしまいます。

instance (All Show as) => Show (HList as) where
  show Nil = "[]"
  show (x ::: xs) = show x ++ ":" ++ show xs

-- 実行例
-- > "100" ::: 4.2 ::: 10 ::: [1..5] ::: Nil
-- "100":4.2:10:[1,2,3,4,5]:[]

TextFの実装

以上でヘテロリストが実装できました。これを使えば我々の目的であるprintf函数の型も大体見当がつくでしょう。

printf :: HList as -> HList bs -> IO ()
printf x y = undefined

printfは2つのHListxとyを受け取って、もしもxの先頭がString型であれば、それをそのまま出力します。そうでなければ、xの先頭とyの先頭の型があっているか(xの先頭が_dだったらyの先頭はInt型であるか)を判断して、合っていればそれを出力します。このようにprintfは型によって実装が変わるので、型クラスの出番です。

class TextF as bs where
  textf :: HList as -> HList bs -> String

また、printfはIO ()になって少し扱いにくいので、textf :: HList as -> HList bs -> Stringという純粋函数を定義して、それを使ってprintfを実装することにしました。

いよいよ実装です。まずは、それぞれのリストas, bsがともに空である場合。

instance TextF '[] '[] where
  textf _ _ = ""

そして、asの先頭がString型かどうかでパターンマッチを行います。

instance (TextF as bs) => TextF (String ': as) bs where
  textf (x ::: xs) y' = x ++ textf xs y'
 
instance (TextF as bs) => TextF ((x -> String) ': as) (x ': bs) where
  textf (x ::: xs) (y ::: ys) = x y ++ textf xs ys

asはString型のデータか、x -> String型の函数が入っているということにしました。つまり、_dや_fは_d :: Int -> String, _f :: Float -> Stringの型であって、さらに_d 10や_f 3.1415などの値が画面に出力されることになります。 よって、このような_dや_fはshowそのものですから、これを定義してあげることにします。

_d :: Int -> String
_d = show
 
_s :: String -> String
_s = id
 
_f :: Float -> String
_f = show

(String -> Stringだけは、そのままshowするとクォーテーションがついてくるのでそのままにしてあります。)

まとめ

以上で、printfの実装が完全に出来ました。 では実際に動かして遊んでみましょう。

> printf Nil Nil

> printf ("hello!" ::: _s ::: Nil) ("world!" ::: Nil)
hello!world!
> printf ("hoge:" ::: _d ::: Nil) (3.1415 ::: Nil)
*** 型エラー ***
> printf ("hoge:" ::: _d ::: Nil) ((20 :: Int) ::: Nil)
hoge:20
> printf ("hoge:" ::: 10 ::: Nil) (Nil)
*** 型エラー ***

はい、正しく動いているようです。

なお、問ではこれを printf ["hello","world!"] [] のようにリストカッコを用いて書くように言っていましたが、そのようなリストの表記を使えるようにするGHC拡張として、OverloadedListsが提案されているようです。 また、このprintfをCと同じように可変長引数にすることは頑張ればできると思うのでよければやってみてもいいかもしれません。(丸投げ)*2

GADTs, DataKinds, ConstraintKinds, TypeFamiliesなどのGHC拡張を使えば、このような型レベルプログラミングも比較的[要出典]簡単に実装することができます。便利なGHC拡張はドンドン使っていきましょう。

参考

参考にしたページと参考になりそうなページ

• GHC 7.4.1 の型レベル新機能を使い倒す 〜GADTs、型族 と DataKinds、ConstraintKinds の円環〜 - これは圏です
• 7.11. The Constraint kind
• DataKinds 言語拡張を使って Typed Heterogeneous List とその基本操作を実装してみた - hyoneの日記
• Constraint Kinds for GHC | :: (Bloggable a) => a -> IO ()

*1:各データコンストラクタの像を適当な形に制限するために使うものだと思っていますが正確なところは知りません

*2:型クラスを用いた可変長引数の実装はText.Printfが分かりやすいと思います。

Haskellでもできる！実践・オブジェクト指向

Lensにほとんど触れたことのない人にはこちらの記事がオススメです：Lensで行こう！ - Just $ A sandbox

Haskellでもオブジェクト指向をしましょう！
Haskellは直接オブジェクト指向的な機能を提供してはいませんが、我らがLensの力を借りることでオブジェクト指向的な設計を意識したコーディングが可能です。

今回利用するのは主に以下のモジュールです。

• Control.Lens.Lens
• Control.Lens.Getter
• Control.Lens.Setter
• Control.Lens.TH

Lensのおさらい

Lensを使ったことのある人にはおなじみだと思いますので、特に解説はしません。

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t  -- Lens型(GetterやSetterの一般形)
type Lens' s a = Lens s s a a  -- Lensの省略形

(^.) :: s -> Getting a s a -> a  -- 値をgetする
(.~) :: ASetter s t a b -> b -> s -> t  -- 値をsetする
(%~) :: Profunctor p => Setting p s t a b -> p a b -> s -> t  -- 函数を適用したものをsetする
(.=) :: MonadState s m => ASetter s s a b -> b -> m () -- 値をMonadStateの文脈でsetする( (.~)のMonadState版 )
(%=) :: (Profunctor p, MonadState s m) => Setting p s s a b -> p a b -> m () -- 函数を適用したものをMonadStateの文脈でsetする( (%~)のMonadState版 )
(<~) :: MonadState s m => ASetter s s a b -> m b -> m ()  -- アクションを実行した結果をsetする

lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b  -- getterとsetterからLensをbuildする

特に最後のlens函数は重要です。例えば適当なdata型をmakeLensesするとき、何が起こっているかを明示すると

data Hoge a b = Hoge { _foo :: a, _baz :: b }
makeLenses ''Hoge

-- 以下が生成される
foo :: Lens' (Hoge a b) a
foo = lens _foo (\h x -> h { _foo = x })

baz :: Lens' (Hoge a b) b
baz = lens _foo (\h x -> h { _baz = x })

となります。 lensに、getter :: Lens' s a -> aとsetter :: Lens' s a -> a -> Lens' s aを渡すことで、出来上がるlens getter setterは上手くLensとして振る舞ってくれます。

型クラスとオブジェクト

Lensでオブジェクトを定義しましょう。
例として、ブロック崩しゲームのようなものを考えてみましょう。ブロック崩しには当然、ボールやバーが必要ですのでこれを定義してみます。

data Ball = Ball { _posBall :: (Int, Int), _velBall :: (Int, Int), _r :: Int } deriving (Eq, Show)
makeLenses ''Ball

data Bar = Bar { _posBar :: (Int, Int), _velBar :: (Int, Int), _width :: Int, _height :: Int } deriving (Eq, Show)
makeLenses ''Bar

posHogeはオブジェクトの座標にあたります。わざわざ名前を変えているのは、函数の多重定義になってしまうからです。また、オブジェクトは座標を更新して動かしたいので、このようなメソッドを定義します。
Haskellでは、いわゆるメソッドに当たる部分は型クラスのメソッドとして定義します。メソッドはオブジェクトに関する値を戻り値にとる函数というよりもオブジェクト自体を操作する函数であることが多いのでデータ型とは分けて定義するほうが便利です。また、型クラスのメソッドなら、同じ名前でもデータ型によって異なる振る舞いが定義できます。

class Move c where
  update :: State c ()

instance Move Ball where
  update = do
    (vx,vy) <- use velBall
    posBall %= (\(x,y) -> (x+vx, y+vy))

instance Move Bar where
  -- Barは横にしか動けない
  update = do
    (vx,_) <- use velBall
    posBar %= (\(x,y) -> (x+vx,y))

特に意味はないですが、オブジェクトによって函数の振る舞いを変えることが出来ました。
さて、posBallとposBarが同じ座標を表しているのに名前が違うのは何かと面倒なので、これも型クラスを使ってまとめてしまいます。

class HasPos c where
  pos :: Lens' c (Int, Int)

instance HasPos Ball where
  pos = posBall
instance HasPos Bar where
  pos = posBar

はい、これでposBallとposBarを区別する必要はありません。これを使えば、posをもつ任意の要素に対するメソッドが定義できます。

reset :: (HasPos c) => State c ()
reset = do
  pos .= (0,0)

resetはHasPos型クラスのインスタンスならなんでも適用できます。つまり、BallとBarはどちらもresetで操作をすることができるわけです。便利ですね！

Classyとサブクラス

さて、上ではHasPosを定義して名前の衝突を防ぎましたが、これを共通する全ての函数について行わなければならないのは面倒です。そこで、posやvelなどの共通するメンバをもつ抽象クラスを作り、BallやBarはこれらを内部に含む(ある意味ではサブクラス・継承したクラスのようなもの)クラスとして定義することにしましょう。

data GameObj = GameObj { _pos :: (Int, Int), _vel :: (Int, Int) }
makeClassy ''GameObj

-- 以下が自動生成される
class HasGameObj c where
  gameObj :: Lens' c GameObj

instance HasGameObj GameObj where
  gameObj = id

pos :: (HasGameObj c) => Lens' c (Int, Int)
vel :: (HasGameObj c) => Lens' c (Int, Int)

makeClassyはGameObjからHasGameObj型クラスを生成します。これによって、HasGameObjのインスタンスになったものは自由にposとvelを使えるようになります。
どういうことか見てみましょう。

data Ball = Ball { _ballObj :: GameObj, _r :: Int } deriving (Eq, Show)
makeLenses ''Ball

instance HasGameObj Ball where
  gameObj = ballObj

これでBallはHasGameObjのインスタンスになったので、b :: Ballに対してb ^. posとかb & vel .~ (1,0)などとかけるようになったわけです。

また、少しデザインパターン的ですが、自分自身を更新する函数を内部に持つオブジェクトの定義も出来ます。
同じ型を持つオブジェクトの実装を変えられるようにしたい -qiita

これは、例えば変な動きをするボールを作りたいときに、ボールの動きをデータの生成時に指定したいみたいな状況で使えると思います。
(上の記事のAutonomieの実装を参照。autoを例えばBall型で、runAutoをState Ball ()とすればこのような実装も可能。)

ここまででかなりのことはできるようになったと思います。
今回は記事タイトルの通り、「実践」を意識した解説を行いました。例えば私はChimeraという弾幕シューティングゲームを全てHaskellで実装していますが、Lensはこれくらい本格的なプロジェクトになっても通用するレベルの強力さを秘めています。

Lensは(たぶん)他にも使い方があります。あなたもこの強力なライブラリで快適なHaskellコーディングを楽しみましょう！
さあいますぐインストール！ *1

*1:2014/02/02時点でlens-4.0がリリースされています。