Koji Miyazato

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) は分けてくれたほうが結果的に綺麗な構成だった感ある

Num a はfromInteger :: Integer -> aではなく

data IntLiteral = IntLiteral { hasNegativeSign :: Bool, radix :: Int, digitsPerElem :: Int, packedDigits :: Vector Word } -- (radix ^ digitsPerElem)進表現
fromIntLiteral :: Num a => IntLiteral -> a

みたいな

「光と影の地平」聴いて絶対に買うべきと判断して遊んだんだよな

BDFFのリマスターまじ？と思ったけどもう10年以上経ってるからそうか・・・

数値リテラルを(それが表す数値ではなく)元の文字列表現に1対1対応する型で表したいことあるよなあ

4oです

ChatGPT、ちょとふわふわした議論（設計のよしあしとか）を自分で明晰に分析してくれない感じがする。「コードを交えて説明して、最後に簡潔に要約して」みたいな指示をすると一気にシャープになるような・・・

「ある証明をtransferした関数が等しいことの証明」が等しいことの証明！やってられるか！！！

Agda-mode output showing "unsolved metas" Agda v2.7.0.1 _355 : ≡.trans (≡.sym (subst-subst-sym eq)) (≡.cong (subst eq) (subst-sym-subst eq)) ≡ ≡.refl

eq : あるequivalence relation x ~ y
subst eq : eq を 関数にtransferしたもの P x -> P y
subst-subst-symなど : subst の性質を≡で表したもの
これ : subst-subst-symなどから組み立てた証明がreflに等しいこと

たとえばsubst-subst-sym, subst-sym-subst から
f = subst eq
g = subst (sym eq)
のときf (g x) ≡ x; g (f y) ≡ yだけど、これだけから(proof : f y ≡ (f ∘ g) (f y) = f ((g ∘ f) y) ≡ f y) が (refl : f y ≡ f y)と等しい(proof ≡ refl)ことは出てこない。

Propositionならその2つは同じだけどさぁ

≡を任意のEquivalenceに置き換えると上手くいかないのはgroupoidを仮定したやつに依存してたからか

あーそっか、EquivalenceってGroupoidじゃないんだ
それはそうだ

eqPD : ≡.subst (D₁ F.∘′ v″) (C.subst-subst eq₁C) (D.subst step₂ (D.subst step₁ pd)) ≡ D.subst (eqV pc) pd eqPD = begin ≡.subst (D₁ F.∘′ v″) (C.subst-subst eq₁C) (D.subst step₂ (D.subst step₁ pd)) ≡⟨ ≡.subst-∘ (C.subst-subst eq₁C) ⟩ ≡.subst D₁ (≡.cong v″ (C.subst-subst eq₁C)) (D.subst step₂ (D.subst step₁ pd)) ≡⟨ props.subst-reflexive D* _ ⟩ D.subst step₃ (D.subst step₂ (D.subst step₁ pd)) -- Proofs written using ≈-syntax have extraneous `refl` at -- the end (to guide type inference) ≡⟨ D.subst-refl ⟩ D.subst D.refl (D.subst step₃ (D.subst step₂ (D.subst step₁ pd))) ≡⟨ D.subst-subst step₃ ⟩ D.subst (D.trans step₃ D.refl) (D.subst step₂ (D.subst step₁ pd)) ≡⟨ D.subst-subst step₂ ⟩ D.subst (D.trans step₂ (D.trans step₃ D.refl)) (D.subst step₁ pd) ≡⟨ D.subst-subst step₁ ⟩ D.subst (D.trans step₁ (D.trans step₂ (D.trans step₃ D.refl))) pd ≡⟨⟩ D.subst (eqV pc) pd ∎ where open ≡.≡-Reasoning

なーんか筋の悪いことをしている気がする・・・

そこまでじゃなかった
(proof1, proof2 : 証明→なんかが等しい証明)が等しい(proof1 ~ proof2)ことの証明

いやぁ・・・

証明が等しいことの証明が等しいことの証明はやだよ〜〜