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

Representable型クラスのmethodであるtabulateとpositionsの関係

Naprerianとかで定義されてる

概要

Representable型クラスを定義する際には一般的(?)にはこう書かれる

code:hs

class Functor f => Representable f where

type Rep f :: *

index :: f a -> Rep f -> a

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

しかし、tabulateの代わりにpositionsで定義しても全く同じ意味になる

code:hs

class Functor f => Representable f where

type Rep f :: *

index :: f a -> Rep f -> a

positions :: f (Rep f)

これは、片方があればもう片方を定義できるから

code:hs

tabulate h = fmap h positions

positions = tabulate id

型を見ても分かる通り、定義者目線ではpositionsを定義したほうが楽

この「片方があればもう片方を定義できる」というのは上の定義を見ればわかるが、

この関係を圏論的に見ると米田の補題の裏付けがあることがわかる

表現可能関手と米田の補題を同時に図にしてみる

https://gyazo.com/0f3041974f3da8b8181834c8892bad42

米田の補題は、一般的でない方(?)の共変Hom関手の方の定理を使っている

$ [\mathscr{A},\mathrm{Set}](H^A,F)\cong F(A)

上図の青色の部分の同型性を述べている

圏$ \mathscr{A}内で、$ Aから伸びる射が($ Bとかではなく)$ Aに向かっているのに注意mrsekut.icon

ここで、tabulateとpositionsに当たる部分の型を見てみる

自然変換$ \alpha : H^A\to Fは、

hsで書くと、α :: (A -> a) -> F a

であり、これがtabulateだった

これは、$ H^A から$ F への自然変換の集合$ [\mathscr{A},\mathrm{Set}](H^A,X) の元の1つである

対象$ F Aは、

hsでのpositionsに該当する

登場人物の対応を表にしておく

table:対応

圏論の世界 method名 hsの世界 Associated Type Familyの表記

自然変換α: H^A->F tabulate (A -> a) -> F a (Rep f -> a) -> f a

対象FA positions F A f (Rep f)

参考