haskell-jp / math #9

Coalgebra の方ってレンズとかライフゲームだっけ。
なんか、レンズの有用性とかあまり知らないので、ちゃんとやりたいな。
Traversable とは、横断検索ができる形のデータ型の型クラス?
実用例としては、主にツリー型への適用だろうか。
Hom(BxC,D) == Hom(B,Hom(C,D))

これは、
g (b,c) = curry g b c
のカリー化を端的に表しているものだと思いましたが、
(>>=) を用いて何をしようとしているのでしょうか。
f : A -> B 
g : B -> A -> C 
に対して、

自然に考えられる A -> C の要素は、
λa. (g (f a) a) 
でしょうか。
元記事をよんでみたが、
class Category の定義に id でなく、idA があるのが謎すぎる(読むのをやめた)
そうであろうと思いながら、実際に例を見つけられていなくてモヤモヤしていることなのですが:

1. 圏 C と圏 D を用意
2. 函手 F: C → D と函手 G: C → D を用意
3. 任意に FG を選んだとき、自然変換は必ずしも構成できない
(函手圏として捉えれば、任意の2対象間に必ずしも射が存在するとは限らない、の意)

これは自明だと思っているのですが、どうしても型と関数の圏に閉じる場合、
適当な自然変換を構成できてしまうようにも思えてしまい… 何か身近な反例って無いでしょうか? :thinking_face:
(もしくは、CCCだと任意の2自己函手間に自然変換を構成できてしまう、などあったりするのか)
CやDは一般の圏でもOKですか?(型と関数の圏にはこだわらない?)
一般の圏でも良いです :slightly_smiling_face:
Cを空でない適当な圏として、D={:smile:,:thinking_face:}を対象が2個の離散圏(射が恒等射しかない圏)とします。Fを、対象をすべて:smile:に送り、射もすべてid:smile:に送る自明な関手とします。Gは対象をすべて:thinking_face:に送り、射をすべてid:thinking_face:に送る自明な関手とします。FからGへの自然変換を作るにはCのそれぞれの対象(仮にaとします)について射Fa→Gaを用意しないといけませんが、Fa=:smile:とGa=:thinking_face:の間には射は存在しないのでそのような自然変換は存在しません。
あー、それはめちゃわかりやすいですね!ありがとうございます :bow:
@me1 has joined the channel
続くCoqでの証明はわからんけど、すごくおもしろい https://qiita.com/nekonibox/items/c1c7f4d1ad1695967e39
半順序でのソートってつまりトポロジカルソートなのでは(まだ記事を読んでいないけど)
そこで、O(n log n)の全順序におけるソートアルゴリズムが流用できないかを考察していきます。
とあるとおり、既存のソートアルゴリズムを再利用できないか、という試みです。
読みました。その通りですね。最悪計算量が O(n log n) であるアルゴリズムが全滅しているのは偶然なのかな?
@as_capabl「同型があることが前提で」と書いたのは間違いでした。 
law を満たすと以下のような随伴関係が成り立つので自然な同型になり、
随伴関手からモナドはできる、となるようです。
左随伴関手
F(X) = (X, C)
F(f) = pure((f, id))
右随伴関手
G(Y) = Hom_α(C, Y) (Hom_α(C, Y) は本でいえば α C Y のこと)
G(g) = (>>> g)
単位 η = mkPair
余単位 ε = app
随伴関手 (F,G,η,ε)
ε の自然性が合成則
余単位-単位恒等式
εF ・ Fη = 1_F が簡約則
Gε ・ ηG = 1_G が外延性則
なるほど。ちょっとMerlyのケースにあてはめてみます
G(Y) = C -> Y と書いてしまいましたが G(Y) = α C Y だったので修正しました。
Haskell と圏論との関連性を追求したいならば、(個人的意見(要望にあたるのかな)ですが、)

Awodey "Category Theory"

を読んでおいたほうがいいように思います。
重要な具体例のオンパレードで、
滑らかに議論が進むと思います。
ざっと思いつくのだと、

• Free Monad
• Free Category
• Group as an category
• the category of logic
随伴などでは

• 随伴の構成的な定義
• product -| exponential
• Free (Monoid) -| Forgetful
• Free (Category) -| Forgetful
くらいかなあ。
あんましでてこないや,,,
Awodey わかりやすいですよね!
英語版ならPDFもあるし
(PDF 注意)
邦訳も出ているし(訳があまり良くないという話もありますが :sweat_smile: )
https://www.kyoritsu-pub.co.jp/bookdetail/9784320111158
あと,ついでに
随伴 -> モナドは、
F -| G -> GF ですが、

モナド -> 随伴は、
MacLane (邦訳は圏論の基礎?だったかな?)に記述があります。(Chapter VI. Monads and Algebras の Theorem I )
Monad T をT-algebra とみたとき、
随伴が確か構成できたと記憶しています。
うーん、あんまり活発な議論にならんわりに無駄に時間取られるので、退出します...
@shin1hi has left the channel
なるほどそうか、随伴のHomの関係式

Hom(F(X), Y) <-> Hom(X, G(Y))

は両辺同じ圏のHomである必要はないんだ、
だから

k (a, b) c === (a -> k b c)

は、ちゃんと随伴の関係式なんですね
引用元のスレッドに挙げたのですが、冪対象の定義だと、この関係は両辺ともHom_Cだったので https://ja.wikipedia.org/wiki/%E5%86%AA%E5%AF%BE%E8%B1%A1#%E5%AE%9A%E7%BE%A9
例のAwodeyの邦訳の質の悪さは焚書ものだという評判ですね
邦訳なら『ベーシック圏論』が良いと聞きますよね
僕はまだ読めてないんですが今度Zoomでの輪講が企画されてるので参加してみようと思ってます :eyes:
https://haskell-jp.slack.com/archives/C4NDY2TF1/p1585019424018000
@addokoda has joined the channel
@kiyotakatheblack has joined the channel
行列演算からフィボナッチ数を求める方法があるとはしらなんだ
http://www.haskellforall.com/2020/04/blazing-fast-fibonacci-numbers-using.html
私の記事でも扱っているネタですね。英訳を用意しておくべきだったか… https://blog.miz-ar.info/2019/01/fast-fibonacci/
あれ、ホントだ、すごいよく似た内容でしたね... :cold_sweat:
当時はまだ購読してなかったか...
SICPにもありますね.問題1.19
@tomoya0229 has joined the channel
@claude0803sz has joined the channel
@biacco42 has joined the channel
数学に本質的じゃない、興味本位の質問ですみません。
profunctorパッケージのドキュメントを読んでたらTambara http://hackage.haskell.org/package/profunctors-5.5.2/docs/Data-Profunctor-Strong.html#t:Tambara という型に出会ったのですが、この名前はYonedaのように日本人の名前由来なんでしょうか?
Tambara functor
丹原 大介 、らしいです。ググった結果によると。
ありがとうございます!
@noahzark2525 has joined the channel
@kawai.natsuo has joined the channel
@kanshu.yokoo has joined the channel