Representable型クラスのtabulateとpositionsの同じさは米田の補題に裏付けられる
米田の補題による
Naprerianとかで定義されてる
概要
Representable型クラスを定義する際には一般的(?)にはこう書かれる
hsclass Functor f => Representable f where
type Rep f :: *
index :: f a -> Rep f -> a
tabulate :: (Rep f -> a) -> f aしかし、
tabulate の代わりに positions で定義しても全く同じ意味になるhsclass Functor f => Representable f where
type Rep f :: *
index :: f a -> Rep f -> a
positions :: f (Rep f)これは、片方があればもう片方を定義できるから
hstabulate h = fmap h positions
positions = tabulate id型を見ても分かる通り、定義者目線では
positions を定義したほうが楽この「片方があればもう片方を定義できる」というのは上の定義を見ればわかるが、
この関係を圏論的に見ると米田の補題の裏付けがあることがわかる
表現可能関手と米田の補題を同時に図にしてみる
米田の補題は、一般的でない方(?)の共変Hom関手の方の定理を使っている
[\mathscr{A},\mathrm{Set}](H^A,F)\cong F(A)
上図の青色の部分の同型性を述べている
圏\mathscr{A}内で、Aから伸びる射が(Bとかではなく)Aに向かっているのに注意
ここで、
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 に該当する登場人物の対応を表にしておく
対応
| 圏論の世界 | 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) |
参考