情報更新

last update 03/28 18:49

ツイート検索

 

@shinji_kono
サイトメニュー
Twilogユーザー検索

Twilog

 

@shinji_kono

Shinji Kono@shinji_kono

Stats Twitter歴
6,199日(2007/04/10より)
ツイート数
226,133(36.4件/日)

ツイートの並び順 :

表示するツイート :

2019年08月31日(土)35 tweetssource

8月31日

@shinji_kono

Shinji Kono@shinji_kono

MonadはMeta計算を状態や大域変数を使わずに実現する時の技術。実装と構文がごっちゃになってる現状は良くない。Monad自体は単なるデータ構造なのでListでも配列でも良い。それがどんなメタ計算を表しているのかが一貫していれば問題ない。計算履歴、例外、解析結果などなど。

posted at 03:00:03

8月31日

@shinji_kono

Shinji Kono@shinji_kono

計算のログをListで取るMonadとかを作れるのでListはMonadになれる。Monadのデータ構造は結合律が要求されるのでListが一般的。他には結合律が成立する論理式とか。orがつながってるとか。

posted at 03:03:24

8月31日

@shinji_kono

Shinji Kono@shinji_kono

Monadの射は
a → M b
という型なので関数をつなげる時の入力と出力が合わない。Haskellはそのための構文を持ってるけど、Javaには構文がない。でも、joinを自分でやると煩雑だし見っともない。

posted at 03:07:39

8月31日

@shinji_kono

Shinji Kono@shinji_kono

Monadには、もちろん型がある。ある関数がなんのMonadなのかは型推論で決まるのだが、Monadが組み合わさってるとliftとかで切り替えることに。

posted at 03:10:10

8月31日

@shinji_kono

Shinji Kono@shinji_kono

System callとか破壊代入とかtry/catchはメタ計算なので、メタ計算が欲しいだけなら無理にJava/ScalaでMonadを使う必要はない。既にある。

posted at 03:12:36

8月31日

@shinji_kono

Shinji Kono@shinji_kono

Contextを持ち歩いてるって意味では、MonadはDI Container に近いとも言えるんだよな。構文的には引数一つ増えるだけだし。Joinはどうなのって問題はあるけど。

posted at 03:18:22

8月31日

@shinji_kono

Shinji Kono@shinji_kono

bindやApplicative の構文が見えちゃうのはダサい。そんなこんなで、Monadが既存のプログラミング言語にあうかというとどうかな。Pure Functional にやるってのがHaskell とは相性良かった。

posted at 03:32:20

8月31日

@shinji_kono

Shinji Kono@shinji_kono

構文的には見えなくて、実装がMonad としての意味を持ってるくらいが望ましい。それは今のthread safeなライブラリとほとんど同じ。

posted at 03:33:48

8月31日

@shinji_kono

Shinji Kono@shinji_kono

Mogi 先生のMonadは、メタ計算をMonadで表せるってだけで組み合わせに関しては何も言ってない。世界にMonadは一つで、
f : a → b な圏

f’ : a → T b な圏
は随伴としての双対になってるって話。

posted at 04:49:21

8月31日

@shinji_kono

Shinji Kono@shinji_kono

HaskellではMonad 感染とかいうけど、本来は全部一つのMonadで特別な構文とか要らないはず。どっかで話がおかしくなった。Monadはプログラマががんがん自分用に書いていくというものとは違うらしい。

posted at 04:52:11

8月31日

@shinji_kono

Shinji Kono@shinji_kono

ZFは時間切れだが、濃度と超フィルターは未完って感じで区切りはついた。いや、pairとordered pairまでできたというべきだな。

posted at 05:01:17

8月31日

@shinji_kono

Shinji Kono@shinji_kono

公理の記述から順序数の構築、ODの導入、モデルから公理の証明で、一つ一つ問題出まくりで楽しめた。割とハッピーエンドだし。

posted at 05:03:42

8月31日

@shinji_kono

Shinji Kono@shinji_kono

Ord : Ordinal → OD
Ord x = record { def = λ z → z o< ≈ x }
が推移集合になるので、これが⊇を射とする圏を構成して、Power SetはFunctorになるくらいはやった方が良いかも。まぁ、自明だが。

posted at 05:15:01

8月31日

@shinji_kono

Shinji Kono@shinji_kono

田中先生の本にODについて詳しく書いてあったので助かった。ODすごい。元はゲーデル先生のアイデアらしい。Agdaとの相性も良い。

posted at 05:28:38

8月31日

@shinji_kono

Shinji Kono@shinji_kono

twitter で子宮頸がんワクチンで検索すると反ワクチンが多く引っかかるが人数は少ない。うるさい人が一部いる感じだな。

posted at 09:18:31

8月31日

@shinji_kono

Shinji Kono@shinji_kono

ToposはCCCにsubobject classifier と自然数を付け加えたもの。なので、やっぱり、CCCのpolynomial とかfunctional completeness とかやっておくべきらしい。

posted at 13:40:04

8月31日

@shinji_kono

Shinji Kono@shinji_kono

KVSや非正規形DBを「仕様を決めないで良いDB」とか思ってるなら、まぁ、酷い目にあうよね。DBの仕様決定は依存性の洗い出しだから、正規化と内容は同じ。KVSのKはKeyだから。

posted at 17:55:16

2019年08月30日(金)52 tweetssource

8月30日

@shinji_kono

Shinji Kono@shinji_kono

圏論5年もやってるので難しいと思わなくなってきてる。
可換図とAgdaのReasoning
が対応してるってのは、もっと知られて良い。

f : a → b
↓ ↓
g : c → d

は f ≈ g を使ったReasoning 。

posted at 08:22:15

8月30日

@shinji_kono

Shinji Kono@shinji_kono

この図を斜めに反転すると

t a : a → G b
↓ ↓
t b : b → G b

Monadのηになる。t : 1 → G 。Gが座標変換でtが座標変換でのベクトルの対応を表す。

a → G b で圏になって欲しいと思うとMonad則が必要。

posted at 08:56:27

8月30日

@shinji_kono

Shinji Kono@shinji_kono

a → G b と b → G c が a → G c になって欲しいから

a → G b → G G c
↓ ↓ ↓
a → G b → G c

なので、μ : G G → G が必要なことがわかる。

posted at 09:02:27

8月30日

@shinji_kono

Shinji Kono@shinji_kono

自然変換のある関手はベクトルを保存する座標変換だけど、微分とかのベクトル(の演算)を保存する演算子だと思っても良い。すると、

μ : G G = G

は二階微分方程式に見える。

posted at 09:05:28

8月30日

@shinji_kono

Shinji Kono@shinji_kono

Limit はある決まった接続の形を持つ対象aと射の集まりを代表する対象。形は形を表すグラフ(圏)からの関手Γと自然変換 t : a→Γで指定する。

Iを離散圏つまりidしか射がない圏にするとLimitは直積になる。

Iを一次元鎖 ・→・→ ・・・とすると解析的な極限に見える。この場合はcolimitだけど。

posted at 09:54:49

8月30日

@shinji_kono

Shinji Kono@shinji_kono

複素関数のコーシーリーマンとか、微分幾何のビアンキ恒等式はMonad則なんじゃないのかというのが降ってきたが、そうかどうかは知りません。

posted at 10:04:53

8月30日

@shinji_kono

Shinji Kono@shinji_kono

プログラマの人は関手は型変数を一つ持つデータ構造で、そのデータ型の変換が自然変換だと思えばそれでOk。

posted at 10:17:52

8月30日

@shinji_kono

Shinji Kono@shinji_kono

Setsは必ずLimitがある。構造を表す圏はlocally smallな必要があるけど実用上問題ない。Setsってのは型付λ計算でdataもrecordも入ってるので当然なんだが、なんかすごい。計算できるかどうかとは関係ない。

posted at 10:36:35

8月30日

@shinji_kono

Shinji Kono@shinji_kono

locally smallはHom SetがSet、つまり、I : Set に対して

hom→ : Hom C i j → I
hom← : ( f : I ) → Hom C i j
hom-iso : hom← ( hom→ f ) ≈ f
hom-rev : hom→ ( hom← f ) ≡ f

なんだが…

posted at 10:42:49

8月30日

@shinji_kono

Shinji Kono@shinji_kono

要するに
≡←≈ : f ≈ g → f ≡ g
が成立するかってことなんだけど(逆は自明)、これ、さっきのから導出できそうなんだけど、どうなんだろう。

posted at 10:44:19

8月30日

@shinji_kono

Shinji Kono@shinji_kono

無理ないヴィーガンっての矛盾してるだろ。菜食主義の極端なものをヴィーガンって言ってたはず。いや、まぁ、好きに自称してください。

posted at 11:09:22

8月30日

@shinji_kono

Shinji Kono@shinji_kono

≡←≈ : f ≈ g → f ≡ g から前のが出ることもない。locally small めんどくさいというか、割と大きな仮定で、いろいろ便利。だいたいlocally smallだと思っていて良い。直接的にはcongが使えるのが大きい。

posted at 11:12:14

8月30日

@shinji_kono

Shinji Kono@shinji_kono

SetsのLimitでlocally smallが必要なのは、Hom Sets つまり関数を対象つまり型に落とす必要があるから。locally smallでないとlevelが合わない。これはLimitのパターンに制限があるってこと。

posted at 11:33:23

8月30日

@shinji_kono

Shinji Kono@shinji_kono

米田関手もlocally smallを要求するけど、あまり気にしないはず。
≡←≈ : f ≈ g → f ≡ g
しか使わない。いやfull and faithful で使うのかも。

posted at 11:41:45

8月30日

@shinji_kono

Shinji Kono@shinji_kono

昨日は帰って9時には寝落ちして起きたら9時だった。おととい、例のZFのProductを朝の4時までやってたからなぁ。ああいう簡単そうで行き詰まったのは無理にやらないで寝かせるべき。

posted at 13:02:32

8月30日

@shinji_kono

Shinji Kono@shinji_kono

聞いたことあるなかでは

牛乳と砂糖のみ

ってのがある。これはヴィーガンとは言わない。宗教的なものでもなく自分で選択した結果らしい。

posted at 13:49:39

8月30日

@shinji_kono

Shinji Kono@shinji_kono

Agda/Haskell の変換関数の名前は
out←in : In → Out
みたいにすると使う時に良い感じ。
PutStr ( str←num 1 )
みたいになる。

posted at 18:03:36

8月30日

@shinji_kono

Shinji Kono@shinji_kono

ODな世界で選択公理を仮定する(あるいは排中律を仮定する)と、かならずlocally smallなisoが見つかるの?
ある要素があって、それに等しい要素からなる集合
か。確かに書けそうだな。でも同値類に対応するすべての要素が取れる保証は? 微妙なのか。

posted at 18:56:28

8月30日

@shinji_kono

Shinji Kono@shinji_kono

Functorの定義にはcongが入ってる。それはSetsかあるいは他のFunctorから作るしかない。まあ、だいたい作れる。Productの定義にもcongはあるので、Sets以外から作るには仮定するかしかない。その辺りに文句をつけてるのかもな。

posted at 19:21:04

このページの先頭へ

×