表現可能関手とRepresentable型クラス

#圏論とプログラミング

表現可能関手とRepresentable型クラスの対応

この辺を知っている前提で書く

表現可能関手とその周辺用語

e.g. 自然変換, 自然同型, Hom関手, etc.

米田の補題

Type Family

概要

https://gyazo.com/0b1d61152481d5d7b2d22827ee298bed

表現可能関手とは、この図の中の$ Xに当たる部分の関手のことを指す

それでいてかつ、ただの関手ではなく、表現が可能な関手である必要がある

ここで、「$ Xの表現」とは、

「対象$ A\in\mathscr{A}」と「自然同型$ \mathrm{Hom}(A,-)\cong X」の選択のこと

のことだった

左側はHask圏なので、対象は型である

$ A,B,Cは、例えばそれぞれInt,Bool,Stringを表す

また、$ \mathrm{Hask}(-, -)をHaskellで書くとtype Hask a b = a -> bなので

右側もまたHask圏である

$ \mathrm{Hask}(A,B)は、例えば(Int -> Bool)のような関数型である

上の表現可能関手の定義表現可能関手とRepresentable型クラス#6117e03e198270000045d92aが言っていることは、

以下の2つが同型である、ということ

関手f型

関手Hask a型

同型であることを示すために、この2つの関手間の自然変換

forall b. Hask a b -> f b

forall b. f b -> Hask a b

を定義して、互いに逆であることを示せばいい

この圏論での表現可能関手の定義から、どのようにしてHaskellでのRepresentable型クラスの定義を構築できるかを考える

着目すべき点は3つある

①$ Xは関手である

②$ Xの表現を考える場合に設定が必要なパラメータは、$ Aと$ Xの2つである

③$ \mathrm{Hask}(A,-)と$ Xが自然同型である

この①~③を満たすようにHaskell上で定義すれば良い

①

$ Xが関手であることを満たすためには、Functorを継承すればいい

②

パラメータが2つ必要なので、Representable型クラスの定義も2つの引数を取りたい

定義の雰囲気は、class Representable X Aのような感じになる

2つ以上の引数を取る型クラスを定義する方法はいくつかあり、いずれもGHC拡張が必要である

ref multi-parameter type class関連のGHC拡張と使い分け

今回はTypeFamiliesを使ってAssociated Type Familyで定義する

この辺あやふやmrsekut.icon #??

選択肢をどういう基準で選択しているのかを知らない

あと単射であることが必要なのかどうか

③

自然同型を言うためには、その間にある自然変換$ \alpha,\betaが、互いに逆になっていればいい

つまり、以下の2つを満たす

$ \alpha\circ\beta = \mathrm{id}

$ \beta\circ \alpha=\mathrm{id}

そのために、まず2つの自然変換をhs上で定義する必要がある

自然変換は関数の族なので、上図のように$ B成分に着目して考える

$ \beta_B:X(B)\to \mathrm{Hask}(A,B)

$ \alpha_B:\mathrm{Hask}(A,B)\to X(B)

Hask圏上の自然変換の表し方はHask圏における自然変換を参照

この辺に注意しておく

$ X(B)も$ \mathrm{Hask}(A,B)も集合なので、$ \alpha_B,\beta_Bは通常の関数である

$ \mathrm{Hask}(-, -)をHaskellで書くとtype Hask a b = a -> bという型である

つまり$ \mathrm{Hask}(A,B)の元は、$ A\to Bとなるような関数である

以上より$ \beta_B,\alpha_Bは以下のように型表現できる

$ \beta_Bの型は、β_B :: X(B) -> Hom A Bとなる

つまり、β_B :: X(B) -> (A -> B)であり

カリー化することで、β_B :: X(B) -> A -> Bと書ける

同様に、$ \alpha_Bの型は、α_B :: (A -> B) -> X(B)となる

それでいてかつ、$ \alpha\circ\beta = \mathrm{id}と$ \beta\circ \alpha=\mathrm{id}を満たしていればいい

ということを踏まえて、実際にHaskellに落とし込む

記号の差異が紛らわしいので、上図を型クラス定義内の記号に書き直す

https://gyazo.com/8630172c652abd09869424841eda0c4f

同じ概念に大文字と小文字が混在するのが紛らわしいが雰囲気で読み取ろうmrsekut.icon

①fは、Functorを継承する

code:hs

class Fnctor f => Representable f ...

②2つのパラメータをAssociated Type Familyで定義する

わかりやすさのため、いったんMultiParamTypeClassesの表記で見れば良いと思う

code:hs

{-# LANGUAGE MultiParamTypeClasses #-}

class Functor f => Representable f a where

Representable型クラスは、関手となる型fと、対象となる型aを取る

kindに注意する

fは、具体型を取って具体型になるので、f :: * -> *

aは対象なので、a :: *

上図を見ればわかりやすい

ちなみにpursではこちらで定義されている ref

ちなみにpursにはTypeFamiliesはない

これをAssociated Type Familyで書き換える

code:hs

{-# LANGUAGE TypeFamilies #-}

class Functor f => Representable f where

type Rep f :: *

対象aを、Rep fとして表示している、と読む

Associated Type Familyを知らないと若干わかりにくい

これはAssociated Type Familyの表記の問題であって、「Rep fだからfに依存している？」とかは深く考えないほうが良いと思うmrsekut.icon

③2つの自然変換をmethodに持てばいい

code:hs

class Functor f => Representable f where

type Rep f :: *

index :: f b -> Rep f -> b

tabulate :: (Rep f -> b) -> f b

それぞれの自然変換$ \alphaをindex、$ \betaをtabluteという名前で定義している

ref indexとtabulateとpositionsの意味

representable則

ref

code:hs

tabulate . index = id

index . tabulate = id

tabulate . return ≡ return

上2つは自然同型によるもの

3番めの条件はなに #??

tabulate . return f = return f

右随伴かmrsekut.icon

米田の補題との関係

Representable型クラスのtabulateとpositionsの同じさは米田の補題に裏付けられる

具体的に見てみる

Representableのinstance例: Stream a

Representableのinstance例: Vector

参考

Representable Functors: Practical Examples | WorksHub

表現可能関手 - bitterharvest’s diary

たまに語彙に引っかかるが、流れがわかりやすい