Koji Miyazato

依存型を表せるCombinator calculus(やばい)

drops.dagstuhl.de/storage/00li...

Day convolutionの"双対"みたいなものがありそうだけど、これ何だろ？疑似コードだけどこんな奴

data Day (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDay (exists x y. (C(x ⊗ y, z), f x, g y))

data DualDay (f :: C -> Type) (g :: C -> Type) (z :: C) = MkDualDay (forall x y. C(z, x ⊗ y) -> (f x, g y))

(existsとforallはそれぞれcoend, endのつもり)

親は新PCについて「初めて体験するのSSDからの起動が滅茶苦茶速い！！！」とのこと

親がノートPCを買い替えたので、古いほう(2012年~)を貰った。Windowsは11がインストール不能だったのでXubuntuを入れる。スペックはそこそこ。

Bash詳しくないからChatGPTくんにとあるスクリプトの改善案を出させたら、すごい色々と一般化してくれたけど微妙に元スクリプトのユースケースを外してしまっていた。「そこまで一般化しなくてもいいし、元スクリプトのままの挙動ができないよ」と言ったら、*一般化したケースを残して*元スクリプトの挙動もできるように直してきた。

せっかく書いたから削除したくないってか？

100万回は言われてそうなことだけど、「バニラ」が「何も付け加えられていない」を意味するの、バニラアイスはバニラエッセンスを入れたからバニラなんじゃなかったのかよ！と思ってしまう

floor(r√2) == floor([r] * sqrt(2))
です

有理数rについて[r]をrに一番近いDouble型の値、sqrt(2)を√2に一番近いDouble型の値として、floor(r√2) == floor([r] * √2) が常に成り立つ[r]の範囲ってどの辺だろう
|r| < 2^49 ぐらい？

型クラスのインスタンスはその型のアイデンティティとも言うべき情報であり、異なるインスタンスをもつ同型な型は(同型であるが)異なる型だ。逆に言えば、型クラスは必ずそのようになっていて欲しいときに*だけ*有用である。

型クラス(a la Haskell)とimplicit(a la Scala)は微妙に異なる意味を持っているし、更に「名前のオーバーローディング」であってそのどちらでもない用法や、「型クラスだがオーバーロードしてほしくない」「implicitだがオーバーロードしてほしくない」ケースもある
これら3つは交差部分がほとんどを占めるベン図だけど、ちゃんとどの領域にも実例があって、何かが別の何かを不要にしない

最近、行ベクトルに右から行列を掛けるスタイルの良さがわかりつつある

なるほど〜〜〜

topos.institute/blog/2023-05...

（時系列的にはAも引用できたはずだけど気付いてなかったんだろうなぁ）

あ、ちゃんと参考文献を見たら、Bが引用してるのは論文AじゃなくてAと共通の著者の学会発表資料だ！それでだ！

論文Aを引用している論文Bを読んでるんだけど、Aの主張する定理の一つ(X)を使うとBの主張するメインの定理の一つ(Y)はより強い結果が得られるし、Bの議論のうち数ページを単純化できる。なんで使ってないんだろう？？？

(X)に誤りがあるとBは主張してないし、(Y)が(X)で単純化できることはわりと明らかなんだけど

kitchen-sink-hs/monads-collection/src/Monad/ExoticCont.hs at 8830dbad4e4e7b392b874308cd0a0482699667a3 · viercc/kitchen-sink-hs Kitchen sink project to experiment various Haskell code snippets - viercc/kitchen-sink-hs

A failed attempt:

github.com/viercc/kitch...

【津波警報 発表】
津波警報に切り替えました。ただちに避難してください。
＜津波警報＞北海道太平洋沿岸、東北地方太平洋沿岸、関東地方、伊豆・小笠原諸島、東海地方、和歌山県
weathernews.jp/news/202507/...

投票先どうするかなぁ、選挙区のほうは決まってるが比例の方は「最悪」と「普通にダメ」と「各論ではまあ賛成できるところもあるが・・・」と「表面的にはよさそうだけど不安材料多い」からの選択

Positionが有限のmonomial monadがすべてstate-like monadである証明通った！

github.com/viercc/agda-...

(screenshot of AI chat service, user's input) やった！それは私が意図した通りです。 より読みやすかったり、整理された証明とするために、 * そもそも証明の流れとして整理すべき箇所 * Agdaで記述された証明としてidiomaticでない箇所 を探していただけますか？

唐突に日本語が思いつけなくなって "Yay! That's exactly what I've intended." を直訳した

だから「他者の理解」なんてハナから誤解だよ
たまたまうまく行くことが多いだけ

Xで見たけど「飼い猫は人間のことを大きな猫だと思っている」みたいなやつ、「人間は猫を〇〇という点が違うだけの人間だと思っている」し、そもそも他者の理解というのは「〇〇という点が違う、自分と同じような存在」以外にありえない

"char"をヒャーみたいに発音している人も探せば居そう

プロンプトが悪かった説はある

引用がハルシネーションであっても証明を吐かせれば実は正しかったりするかもと思って「有限ケースの証明を教えて」って言ってみたら、自明にわかることを長々と説明したあと「残りの部分は前層とかトポスの深い理論がいる結果なんだよ〜」で濁しやがった

存在しない引用より悪質度が上がってるよ〜〜〜

そもそも論文のうち1つはずっと前に（ちゃんと理解してなかったけど）目を通したことはあったから、あれ・・・？とは思ったんだよな

チャットAIに数学的な事項を聞く→AIくん「これは難しいけど(有名人)が有限ケースを、(有名人)が無限ケースで反例があることを示してるよ」→おお！凄い！それが書かれた論文どれ？→AIくん「これ(実在の論文, 書誌情報完璧, URL付き)」→読む→全然書いてないじゃねえか！！！

fromIntegerはあってもいいけどね (ℤは環の圏の始対象なので)

というかリテラルのオーバーロード(0, 1, 2 ... :: C a => a)とNumのオーバーロード ((+) :: Num a => a -> a -> a) は分けてくれたほうが結果的に綺麗な構成だった感ある