MonadはMeta計算を状態や大域変数を使わずに実現する時の技術。実装と構文がごっちゃになってる現状は良くない。Monad自体は単なるデータ構造なのでListでも配列でも良い。それがどんなメタ計算を表しているのかが一貫していれば問題ない。計算履歴、例外、解析結果などなど。
posted at 03:00:03
Stats | Twitter歴 6,199日(2007/04/10より) |
ツイート数 226,133(36.4件/日) |
表示するツイート :
MonadはMeta計算を状態や大域変数を使わずに実現する時の技術。実装と構文がごっちゃになってる現状は良くない。Monad自体は単なるデータ構造なのでListでも配列でも良い。それがどんなメタ計算を表しているのかが一貫していれば問題ない。計算履歴、例外、解析結果などなど。
posted at 03:00:03
計算のログをListで取るMonadとかを作れるのでListはMonadになれる。Monadのデータ構造は結合律が要求されるのでListが一般的。他には結合律が成立する論理式とか。orがつながってるとか。
posted at 03:03:24
Monadの射は
a → M b
という型なので関数をつなげる時の入力と出力が合わない。Haskellはそのための構文を持ってるけど、Javaには構文がない。でも、joinを自分でやると煩雑だし見っともない。
posted at 03:07:39
Monadには、もちろん型がある。ある関数がなんのMonadなのかは型推論で決まるのだが、Monadが組み合わさってるとliftとかで切り替えることに。
posted at 03:10:10
System callとか破壊代入とかtry/catchはメタ計算なので、メタ計算が欲しいだけなら無理にJava/ScalaでMonadを使う必要はない。既にある。
posted at 03:12:36
ただ、Javaのthrowは重いので、Optionalの方が軽くて良いってのはある。Pure functionalになるし。
posted at 03:15:25
Contextを持ち歩いてるって意味では、MonadはDI Container に近いとも言えるんだよな。構文的には引数一つ増えるだけだし。Joinはどうなのって問題はあるけど。
posted at 03:18:22
bindやApplicative の構文が見えちゃうのはダサい。そんなこんなで、Monadが既存のプログラミング言語にあうかというとどうかな。Pure Functional にやるってのがHaskell とは相性良かった。
posted at 03:32:20
構文的には見えなくて、実装がMonad としての意味を持ってるくらいが望ましい。それは今のthread safeなライブラリとほとんど同じ。
posted at 03:33:48
Mogi 先生のMonadは、メタ計算をMonadで表せるってだけで組み合わせに関しては何も言ってない。世界にMonadは一つで、
f : a → b な圏
と
f’ : a → T b な圏
は随伴としての双対になってるって話。
posted at 04:49:21
HaskellではMonad 感染とかいうけど、本来は全部一つのMonadで特別な構文とか要らないはず。どっかで話がおかしくなった。Monadはプログラマががんがん自分用に書いていくというものとは違うらしい。
posted at 04:52:11
Haskell で欲しいMonad/メタ計算は、
メモリ管理
遅延評価操作
だが、その辺りはライブラリでは無力。
posted at 04:53:36
ZFは時間切れだが、濃度と超フィルターは未完って感じで区切りはついた。いや、pairとordered pairまでできたというべきだな。
posted at 05:01:17
公理の記述から順序数の構築、ODの導入、モデルから公理の証明で、一つ一つ問題出まくりで楽しめた。割とハッピーエンドだし。
posted at 05:03:42
集合論の理解も深まった。圏と集合論の関連論文も理解したし。選択公理と排中律の関係とか。
posted at 05:06:02
圏論の方は圏論から一歩もはみ出さなかったが、集合論の方はだいぶはみ出た。それが面白かった。
posted at 05:07:14
Ord : Ordinal → OD
Ord x = record { def = λ z → z o< ≈ x }
が推移集合になるので、これが⊇を射とする圏を構成して、Power SetはFunctorになるくらいはやった方が良いかも。まぁ、自明だが。
posted at 05:15:01
田中先生の本にODについて詳しく書いてあったので助かった。ODすごい。元はゲーデル先生のアイデアらしい。Agdaとの相性も良い。
posted at 05:28:38
これと同じことが日本やアジアでも起きてるとすれば、森林の維持は日本でも重要。
QT またアマゾンは、南米の降雨サイクルの安定化に重要な役割を果たしている
https://natgeo.nikkeibp.co.jp/atcl/news/19/083000504…
posted at 08:28:06
これはマルチクラウドというよりはCloud Bigtsbleの宣伝だな… 「コストのアラートは適切に設定しておくことをおすすめします」ここら辺が怖いが…
https://tech.plaid.co.jp/aws_gcp_multicloud_1…
posted at 08:32:10
はっきりNHKが反ワクチンに加担してるように読める。 NHKが人を殺してると言って良い。
QT ワクチンを接種すれば10万人当たりで最大209人が子宮頸がんで死亡するのを防ぐ効果…おととし8月までに副反応が出た疑いのある人が、3130人
https://www3.nhk.or.jp/news/html/20190831/k10012057921000.html…
posted at 08:35:14
日本のワクチン接種中止の効果が出てくるのはこれかららしい。すでに増えているのは別な原因。成人は検診による早期発見の効果が高い。HPVワクチンの効果は高いのだが、わかりやすい資料が検索で引っかからないのが残念。
http://idsc.nih.go.jp/training/22kanri/22pdf/sep16_04.pdf…
posted at 09:16:34
twitter で子宮頸がんワクチンで検索すると反ワクチンが多く引っかかるが人数は少ない。うるさい人が一部いる感じだな。
posted at 09:18:31
交通事故の人口10万人当たりで見ると、全年齢の死者数が2.79人。子宮頸癌で救える10万人あたり200人の意味するものを考えるとなぁ。
https://www.jiji.com/jc/graphics?p=ve_soc_tyosa-jikokoutsu…
posted at 09:21:26
HPVワクチンの副作用は、普通にしても20/10万人くらいは何か出るってな主張なのか。ワクチン自体も結構痛いので半数は痛いと訴えるらしい。
http://www.jsog.or.jp/modules/jsogpolicy/index.php?content_id=4…
posted at 10:47:07
Lambek先生の本にもTopos with choice rule は排中律を導くとあるな。
posted at 13:36:00
まあ、当然。はっきりとは書いてないけど、Toposは集合論を置き換えるものなのだな。
posted at 13:37:45
ToposはCCCにsubobject classifier と自然数を付け加えたもの。なので、やっぱり、CCCのpolynomial とかfunctional completeness とかやっておくべきらしい。
posted at 13:40:04
Agdaと違って
∀A∋x → f x ≡ g x → f ≡ g
らしい。Agdaではfunctional extensionalityといって仮定する必要がある。
posted at 13:41:43
ToposにはPower Setはないんだけど。
posted at 13:43:44
日本割り当てのIPv4はもうないから、こういうことになる。IPv6だとどうなんだろ。
https://nekonko2.com/nurohikari-demerit/…
posted at 14:59:07
BBQの安い肉はつけ汁が勝負。焼く前に勝負は付いてる。
posted at 15:09:19
E.E.スミスのスカイラークにも、フェンタニールは魔法の薬として出てくる。M.ジャクソンもおそらくはそんな薬。米国の医療はおかしい。
https://www3.nhk.or.jp/news/html/20190831/k10012058321000.html…
posted at 17:46:12
KVSや非正規形DBを「仕様を決めないで良いDB」とか思ってるなら、まぁ、酷い目にあうよね。DBの仕様決定は依存性の洗い出しだから、正規化と内容は同じ。KVSのKはKeyだから。
posted at 17:55:16
香港で戦って得た民主主義は日本とかイギリスとかアメリカのそれになってしまうと思うと残念なのだが…
posted at 23:49:28
ぜんぜんメール読んでなかった...
posted at 07:51:53
今年は圏論はあまりやってないとか思ったら4月はCCCとdeduction theoremやってたのだった。
posted at 07:56:00
圏論5年もやってるので難しいと思わなくなってきてる。
可換図とAgdaのReasoning
が対応してるってのは、もっと知られて良い。
f : a → b
↓ ↓
g : c → d
は f ≈ g を使ったReasoning 。
posted at 08:22:15
Reasoning だと戻れるのが普通だからこうか。
f : a → b
↕︎ ↕︎
g : c → d
posted at 08:25:04
物理な人は可換図は座標変換だと考えると良いかも。
posted at 08:29:06
自然変換も
f : F a → F b
↓ ↓
g : G a → G b
という推論。
posted at 08:34:44
F=1なら
f : a → b
↓ ↓
g : G a → G b
となるので座標変換に見える。fとgはベクトルに見える。
posted at 08:37:00
この図を斜めに反転すると
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
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
自然変換のある関手はベクトルを保存する座標変換だけど、微分とかのベクトル(の演算)を保存する演算子だと思っても良い。すると、
μ : G G = G
は二階微分方程式に見える。
posted at 09:05:28
ちょっと誤植った
posted at 09:16:49
Limit はある決まった接続の形を持つ対象aと射の集まりを代表する対象。形は形を表すグラフ(圏)からの関手Γと自然変換 t : a→Γで指定する。
Iを離散圏つまりidしか射がない圏にするとLimitは直積になる。
Iを一次元鎖 ・→・→ ・・・とすると解析的な極限に見える。この場合はcolimitだけど。
posted at 09:54:49
n 0 1 ∞
・→・→ ・・・
↓ ↙︎
limit a(n)
→ は < だな。この場合。
posted at 09:57:16
複素関数のコーシーリーマンとか、微分幾何のビアンキ恒等式はMonad則なんじゃないのかというのが降ってきたが、そうかどうかは知りません。
posted at 10:04:53
プログラマの人は関手は型変数を一つ持つデータ構造で、そのデータ型の変換が自然変換だと思えばそれでOk。
posted at 10:17:52
Setsは必ずLimitがある。構造を表す圏はlocally smallな必要があるけど実用上問題ない。Setsってのは型付λ計算でdataもrecordも入ってるので当然なんだが、なんかすごい。計算できるかどうかとは関係ない。
posted at 10:36:35
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
要するに
≡←≈ : f ≈ g → f ≡ g
が成立するかってことなんだけど(逆は自明)、これ、さっきのから導出できそうなんだけど、どうなんだろう。
posted at 10:44:19
≈のcongがあればいける。Setsにはあるけど、一般的にはないのでだめだな。
posted at 10:49:04
Basic incomeって税金納めてる人には減税だし、納めてない人には単なる生活保護費なので、大したものじゃない。所得税減税と生活保護費をけちったことで日本が失ったものは大きい。日本民族の未来を断ち切った。
https://gigazine.net/news/20170622-basic-income-in-finland/…
posted at 11:02:43
これからどんな少子化対策しても手遅れで増えるのは日本民族以外になる。日本の中で少数民族になるわけね。
https://youtu.be/oECIkV2SrOM
posted at 11:06:16
無理ないヴィーガンっての矛盾してるだろ。菜食主義の極端なものをヴィーガンって言ってたはず。いや、まぁ、好きに自称してください。
posted at 11:09:22
≡←≈ : f ≈ g → f ≡ g から前のが出ることもない。locally small めんどくさいというか、割と大きな仮定で、いろいろ便利。だいたいlocally smallだと思っていて良い。直接的にはcongが使えるのが大きい。
posted at 11:12:14
SetsのLimitでlocally smallが必要なのは、Hom Sets つまり関数を対象つまり型に落とす必要があるから。locally smallでないとlevelが合わない。これはLimitのパターンに制限があるってこと。
posted at 11:33:23
米田関手もlocally smallを要求するけど、あまり気にしないはず。
≡←≈ : f ≈ g → f ≡ g
しか使わない。いやfull and faithful で使うのかも。
posted at 11:41:45
locally small と cong の関係はこれ。当たり前といえば当たり前。 https://twitter.com/shinji_kono/status/1140263809535246337…
posted at 11:47:10
随伴関手定理もlocally smallを仮定してる。相手はSetsなので変換しないとSets側の≈が出ないから。
posted at 11:54:56
初期に圏論勉強してた頃はlocally smallとか気にしてませんでした。すみません。
posted at 11:56:10
要するに射の等号による同値類を用意できるってのがlocally smallってことだと思えばよい。
posted at 11:58:37
逆にそういう同値類を用意できない場合ってあるのか?
posted at 11:58:55
選択公理がないと代表元を取れない場合があるのか。深いな。選択公理があれば必ず取れる。
posted at 12:04:21
これね。圏論は基本的に選択公理を仮定しない学問だってことがわかる。その代わり、locally smallっていう。
https://math.stackexchange.com/questions/1655923/axiom-of-choice-equivalence-relation-representatives…
posted at 12:08:16
@naltoma それは無理な要求です
posted at 12:41:59
こんなのもあるが、何が書かれてるのかよくわからん。
https://www.math.uni-hamburg.de/home/schreiber/anafun2.pdf…
posted at 12:50:24
昨日は帰って9時には寝落ちして起きたら9時だった。おととい、例のZFのProductを朝の4時までやってたからなぁ。ああいう簡単そうで行き詰まったのは無理にやらないで寝かせるべき。
posted at 13:02:32
聞いたことあるなかでは
牛乳と砂糖のみ
ってのがある。これはヴィーガンとは言わない。宗教的なものでもなく自分で選択した結果らしい。
posted at 13:49:39
ordered pair のあの教科書通りの証明は
ZFProduct ∋ < x , y >→ π1 p ≡ x
で役に立った。
posted at 15:46:11
Cloud内のCDNに頼るのって、やっぱり危険だと思うんだよな… 囲い込みの弊害なんだが…
posted at 15:51:26
電池切れ休憩中
posted at 15:51:59
生産性が十分に上がって、人口をそれに釣り合うように調整すれば、人類は永続的に生きながらえるのか?
posted at 15:54:21
まぁ、だめそうだよな。
posted at 15:54:32
Agdaで証明を追うと、locally smallを使っているところは厳密に特定される。それは良いところだな。
posted at 16:40:47
きたー https://pic.twitter.com/cdVZFsUdBQ
posted at 17:43:14
Agda/Haskell の変換関数の名前は
out←in : In → Out
みたいにすると使う時に良い感じ。
PutStr ( str←num 1 )
みたいになる。
posted at 18:03:36
facebook のYou may knowにくそじじいしか出てこないのも残念だが、まぁ、そんなもん。
posted at 18:33:07
Monoidal Functorではlocally smallは使わない。Applicative はSets上の話なので、やっぱり使わない。
posted at 18:35:43
Equivalence class ってAgdaで書けんの? いや、それが locally small つまり、isomorphic なSetがあるってことなのか。
posted at 18:47:54
ODな世界で選択公理を仮定する(あるいは排中律を仮定する)と、かならずlocally smallなisoが見つかるの?
ある要素があって、それに等しい要素からなる集合
か。確かに書けそうだな。でも同値類に対応するすべての要素が取れる保証は? 微妙なのか。
posted at 18:56:28
ああでも、non empty はどうやって示すんだ?
posted at 19:12:12
Functorの定義にはcongが入ってる。それはSetsかあるいは他のFunctorから作るしかない。まあ、だいたい作れる。Productの定義にもcongはあるので、Sets以外から作るには仮定するかしかない。その辺りに文句をつけてるのかもな。
posted at 19:21:04
バスの時間まで2分で準備しろ状態
posted at 20:54:54
Mojaveでusb serialが動かん問題
posted at 20:55:49