2021-02-16_#3
ふりかえり用アセット
見てきた範囲
参加者によるメモ
型とプログラムの圏を考えたとき、型$ \mathrm{T}と型$ \mathrm{U}に対して、プログラムである射$ f : \mathrm{T} \rightarrow \mathrm{U}の ”あつまり” であるような別の型$ \mathrm{T} \Rightarrow \mathrm{U}が再び型とプログラムの圏のひとつの対象として含まれている。ということは、次のような議論が可能だろうか？
型とプログラムの圏$ \mathbb{C}の自己函手$ \mathbf{F}:\mathbb{C} \rightarrow \mathbb{C}を考えたとき、対象$ \mathrm{T}, \mathrm{U} \in \mathbb{C}、射$ f : \mathrm{T} \rightarrow \mathrm{U}に対して、$ \mathbf{F}(\mathrm{T}), \mathbf{F}(\mathrm{U})と射$ \mathrm{map}_\mathbf{F}(f) : \mathbf{F}(\mathrm{T}) \rightarrow \mathbf{F}(\mathrm{U})が定義から得られる
上記に加えて、$ \mathrm{T}\Rightarrow\mathrm{U}という対象の函手$ \mathbf{F}による像$ \mathbf{F}(\mathrm{T}\Rightarrow\mathrm{U})と、函手によって移された対象から導かれる型（＝対象）$ \mathbf{F}(\mathrm{T})\Rightarrow\mathbf{F}(\mathrm{U})を考えることができる。これらは一致するか？
Re: 結論から言えば、函手$ \mathbf{F}が Strict Closed Functor というもので無い限り、一致はしません
なお、一致するという性質を取り除けば、函手$ \mathbf{F}は関数プログラミングの世界で Applicative Functor (Lax Closed Functor) という名称で知られています 👨🏫
数学的な集合論の圏も集合$ Aから集合$ Bに対する写像$ f : A \rightarrow Bの "あつまり"$ B^Aがやはり集合になり、再び集合論の圏の対象として現れるので、似たような現象に遭遇している感じがする
集合の圏$ \mathbf{Sets}はその意味で特殊ですね (通常、Hom 集合がその圏内部にそのまま埋め込まれることは無いので)
集合の圏での函手の例として、対象（＝集合）$ Xに対して、その部分集合全体からなる集合$ \mathfrak{P}(X)を与えて、射（＝写像）$ f : X \rightarrow Yに対して、部分集合の$ fによる像を与える写像$ \mathrm{map}_{\mathfrak{P}}(f) : \mathfrak{P}(X) \rightarrow \mathfrak{P}(Y)\ (A \subset X \mapsto f(A) \subset Y)を考える函手$ \mathfrak{P}を考えると
$ \mathfrak{P}(Y^X)は、$ Xから$ Yへの写像の集合の、部分集合全体
$ \mathfrak{P}(Y)^{\mathfrak{P}(X)}は、$ Xの部分集合全体から$ Yの部分集合全体への、写像の集合
両者が一致しないことは明らか
型とプログラムの圏では$ \mathrm{T} \Rightarrow \mathrm{U}のようないかにも函手$ \mathbf{F}が ”分配” できそうな記号が使われているだけだった。
圏$ \mathbb{C}の対象$ X,\ A,\ Bと、$ Aから$ Bへの射$ f : A \rightarrow Bがあったときに、p.15 で自明な写像$ f \circ \_ : \mathrm{Hom}(X, A) \rightarrow \mathrm{Hom}(X, B)が得られていたが、型とプログラムの圏では型$ \mathrm{T}と$ \mathrm{U}から別の型$ \mathrm{T} \Rightarrow \mathrm{U}が得られることに注目して、似たようなことが考えられないだろうか
型$ \mathrm{X}を固定したときに任意の型$ \mathrm{T}から$ \mathrm{X} \Rightarrow \mathrm{T}を得る操作もひとつの自己函手となっているのではないか
型$ \mathrm{T}から$ \mathrm{U}への射(=プログラム)$ a : \mathrm{T} \rightarrow \mathrm{U}に対して、$ \mathrm{map}_{\mathbf{F}}(a) : (\mathrm{X} \Rightarrow \mathrm{T}) \rightarrow (\mathrm{X} \Rightarrow \mathrm{U})を$ \mathrm{map}_{\mathbf{F}}(a)(f) = a \circ fと定める
このような式に妥当性はあるか？
$ \mathrm{map}_{\mathbf{F}}(a)はある種の高階関数の存在を主張しているので、前提条件が不足しているか？
Re: そうですね、ご指摘のものは 共変 Hom 函手の、型とプログラムの圏に閉じる実装 として正しいです
ただし、これが成立するためには Hom 集合が型とプログラムの圏の内部に埋め込めるという性質が必要です
加えて、函手における射のマッピング自体もプログラム (＝ 射) として表せるという意味で、非常に強い性質が背景にはありますね
残っている疑問・質問事項
本当にスミマセン 😇
code:scala
// 正しくはこう
object EndoFunctor {
def apply[F_](implicit instance: EndoFunctorF): EndoFunctorF = instance }
そろそろ復習用の用語集とかあると良さそうですかねー
😐 < ちょっと何言ってるか分からないっす
code:scala
def mapX, Y(f: X => Y): FX => FY }
object EndoFunctor {
// implicit という修飾が引数につくと、これはデフォルト引数を埋め込むような効果を持つ
// この場合、同一スコープ内から EndoFunctorF であるインスタンスを探索し、引数として埋め込んでくれる //
// なお、これ自体は恒等関数なので、型を指定して EndoFunctor のインスタンスを楽に引き当てるためだけのもの
def apply[F_](implicit instance: EndoFunctorF): EndoFunctorF = instance }
implicit val seqFunctor = new EndoFunctorSeq { // map メソッドの戻り値は FX => FY 型の関数だが、いま F には Seq が割り当てられている // よって、SeqX => SeqY 型の関数が戻り値になれば良い //
// ここで _ はラムダ関数の引数プレースホルダを意味する (C++ の boost::lambda::_N と同じ効果)
// 戻り値の型より、_ は SeqX 型の値であるから、map メソッドによって SeqY 型の値を返却できる def mapX, Y(f: X => Y): SeqX => SeqY = _.map(f) }
// Scala において、apply メソッドはインスタンスを呼び出し可能にする
// (C++ の operator() を実装するのと同じ効果)
// よって、次の記述は EndoFunctor.apply(seqFunctor) と同じ意味となる
EndoFunctor(seqFunctor)
// EndoFunctor の apply メソッドは implicit 修飾によって引数をとるから、
// 明示的に引数を渡さなくても呼び出しができる
// そのような時、Scala では呼び出しの () すら省略ができるので、
// 結果的に以下の記述で seqFunctor インスタンスを引き当てることができる
// (※ 型引数が不定になるため、明示的に指定する必要がある)