2021-01-05_#0
ふりかえり用アセット
見てきた範囲
参加者によるメモ
残っている疑問・質問事項
$ \mathrm{Hom}(X, B)から$ \mathrm{Hom}(X, A)への写像も同様に考えられると思うのですが、スライドで提示されている写像との間にどちらか優位性がありますか？
$ f \in \mathrm{Hom}(A, B)が存在するときに$ g \in \mathrm{Hom}(X, A)が存在するならば合成射の存在から$ f \circ g \in \mathrm{Hom}(X, B)が存在することは言えると思いますが、$ f \in \mathrm{Hom}(A, B)が存在するときに$ g \in \mathrm{Hom}(X, B)が存在するからといって$ \mathrm{Hom}(X, A)の要素が存在することは言えないのでは？(合成ではなく分解になる)
Re: 次回にも少し説明する予定ですが、$ \mathrm{Hom}(X, A)から$ \mathrm{Hom}(X, B)には 自然な関数 として$ f \circ -を考えられるというところがミソで、同様な図式を持つのであればいついかなる場合も定義可能です。対して$ \mathrm{Hom}(X, B)から$ \mathrm{Hom}(X, A)への関数も定義はできますが、自然な関数とは言いづらい (なぜなら、$ \mathrm{Hom}(X, A)となんら関連をもたない射が$ \mathrm{Hom}(X, B)には存在しうるため) って感じですね。その意味で、スライドで提示している写像には明らかな優位性があります。
Re:Re: (質問者追記) 質問の記述を間違えた 💦$ \mathrm{Hom}(B, X)の元$ aに対して、右から$ f : A \rightarrow Bを作用させることで$ \mathrm{Hom}(A, X)の元$ a \circ fも考えられるのでは、という質問でした。
Re:Re:Re: 正しいです (後ほどまた説明します，といいつつ途中で漏れてしまったので 2/2 にて 🙏)
定義によると思うが、射が等しいと判定する条件がいまいちのみこめてない。Int を経由して Unit の話と、中身の実装の違いは考えない話から、今回は射の定義域と終域が同じなら同じ射とみなすということなのだろうか？
定義次第だと思いますが、中身の実装は考えないからといって必ずしも定義域と終域が同じなら同じとは限らないのでは。定義域と終域をともに$ \{0, 1\} として$ f(x) = 1 - x と$ g(x) = 1 \oplus x は実装 (計算式) としては違いますが、入出力の対応関係としては同じなので射として同じという定義も可能では？ Unit は 1 要素なので Unit => Unit だと対応関係自体が 1 通りに定まってしまうのでこの場合は定義域と終域だけで確定する、みたいな。
↑を書いていて思ったのですが$ \mathrm{Hom}(A, A)というものも普通に考えるで良いのでしょうか？
Re: 型と関数の圏は、直感的には集合論を前提にしていそうと思うかもしれませんが、実際は 型付きラムダ計算 を前提にしています。なので、ここでの射の等価性は簡約結果の表示が一致する，という趣になってきますね。
$ \forallと$ \existsの順序についてはニュートラルな例として、$ \mathbb{Z}を整数の集合として「$ \forall x \in \mathbb{Z}, \exists y \in \mathbb{Z}, x + y = 0」は正しい (どの整数$ xに対しても足して 0 になる (各$ xに対して特定の) 整数$ yが存在する) 一方、「$ \exists y \in \mathbb{Z}, \forall x \in \mathbb{Z}, x + y = 0」は正しくない (どんな整数$ xに対しても足して 0 になるような特定の整数$ yは存在しない) とかがありかと思いました。
Re: そうですね、その例がまさに順序が逆だとアカン 😇 のわかりやすい例かと思います
$ \exists e \in \mathbb{N}, \forall x \in \mathbb{N}, e + x = xについて真ん中が$ \mathbb{N}である理由ですが、逆に$ \forall x \in Xとしてどういう集合$ Xなら成立してどういう集合$ Xなら成立しないか考えてみるのも面白いんじゃないでしょうか。
まさにですね 👍
うーん、ガチな方々の基準であわせると「圏論，完全に理解した (定型句)」なレベル感ですが、一般的エンジニアのレベルでこれをきちんと理解している場合、型を自在に使いこなせなければ難しいかと思います。その意味では「型システム，なにもわからない (定型句)」なレベル感と言っても良いかもですね 🤔
おっしゃる通り、ジェネリクスって概念は型パラメータ (今回であれば A ) に関する全称量化とみなせるよってことに触れたかっただけですね。それ以外の部分はこの論点において意味は無いですが、おもしろい結果として x => x なる関数の引数と戻り値に同じ型パラメータを付与した場合、副作用を許容しなければ実装が 1 つしかないことが知られているので、それにあわせただけです。e.g. Parametricity