haskell-jp / mokumoku-online #89

@村上豪 has joined the channel

前半は Project Euler を Haskell で解いて　後半は The Hitchhiker's Guide to Logical Verification (2025 edition) の Part II Functional–Logic Programming / Chapter 5 Functional Programming をヤリます (いよいよ Part II なんか少し面白くなってきた)

S.K.です。お世話になっております。
参加の申し込みをしていましたが、用事ができまして、今日のもくもく会はお休みさせていただきます。
また次回以降参加させていただこうと思います。よろしくお願いいたします。
末筆ながら、参加者の皆様の本日のご健闘をお祈り申し上げます。

山本悠滋です。遅くなりましたが github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます

相変わらずShared Workerとmain thread間のやり取りがうまく行ってませんが、Wasm版GHCにHaskellのソースコードを渡してみたらちゃんと動いているらしいことが確認できました。やっぱShared Workerを諦める、が正解な気がして来ました...

Project Euler #150 Sub-triangle Sums　まったく歯が立たない　Kadane's Algorithm を３方向に適用する方策かも
The Hitchhiker's Guide to Logical Verification (2025 edition)　ともかく 5.4 Pattern Matching Expressions まで読む　午睡してしまい報告が遅れました

前半は Project Euler を Haskell で解いて　後半は The Hitchhiker's Guide to Logical Verification (2025 edition) の Chapter 6 Inductive Predicates をヤリます

S.K.です。お世話になっております。
先週とは別の用事がありまして、今日のもくもく会もお休みさせていただきます。
また参加になりましたら、よろしくお願いいたします。
末筆ながら、参加者の皆様の本日のご健闘をお祈り申し上げます。

山本悠滋です。遅くなりましたが github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます。昼寝しないでどこまでいけるかな～？

AIにお願いしてShared WorkerからWorkerに切り替えてみたけど、問題直らず。そう言えば以前AIにデバッグをお願いしたときにタイミングの問題で届かない、みたいなのを聞いたし、見直すべきはそういう所か。

Project Euler #151 A Preference for A5　割と平易　Finite state transitions を Memoization を使って解く
The Hitchhiker's Guide to Logical Verification (2025 edition)　ねむいがともかく 6.4 Linear Arithmetic Tactic まで読む
Lean には Prolog-style logic programming の発展形があると賜っているいる　実際のところ標語的に
"Lean = functional programming + logic programming + more logic" と自画自賛しているのは好き　まだ実感無いけど

山本悠滋です。例の如く github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます。

クライスリ圏 / 表現可能関手 を Agda で形式化して、
米田の補題の証明を調べようと思います。

単純な関数の米田の補題だと、

forall x . (r -> x) -> f x ≅ f r

みたいな感じで、
右から左への変換で、
Haskell の単純な fmap が利用できます。

しかし、クライスリ圏が前提だと、
Rep x = r -> x　(表現可能関手)
が、実質的に、
Rep x = r -> m x
なので、 Haskell でいう fmap ではなくなります。

具体的には、こんな感じの命題の証明を調べる予定です。

前半は Project Euler を Haskell で解いて　後半は The Hitchhiker's Guide to Logical Verification (2025 edition) の Chapter 7 Effectful Programming をヤリます

Discord のボイスチャンネルの Functor に入ってみた

S.K.です。お世話になっております。
先週と同じ用事が終わらず、今日のもくもく会もお休みさせていただきます。
また参加可能になりましたら、よろしくお願いいたします。
末筆ながら、参加者の皆様の本日のご健闘をお祈り申し上げます。

やっぱこの通りだったー！ :joy:
https://haskell-jp.slack.com/archives/CUPBC8WCE/p1790500154151469

こんにちは〜。今日は bundler-hs の README を書き直します

AI 感を減らすことができました。お先に失礼します。また来週！ :muscle:

Project Euler #152 Sums of Square Reciprocals　まったく歯が立たずトホホ　ナイーブ（馬鹿正直）解法では n = 20 までで力尽きる n = 80 なんて夢のまた夢
The Hitchhiker's Guide to Logical Verification (2025 edition)　ともかく 7.6 Mutable State まで読み進むも　なんか「五里霧中」感が抜けない　あ～もできる　こ～もできる　いろいろな出来るのは良いが　何で決定版に絞らないの？　あっちこっち（数学とか論理学とか）からの要望を入れ過ぎたのかなあ　変な言語だなあ　との印象を持つのは当方が劣等生故か？

ようやくmainスレッドとworkerスレッド間でメッセージを1往復したのを確認できました。ここまで長かった... :weary:
github.com/haskell-jp/makeMistakesToLearnHaskell/commit/1a7bf42c3ee3…
github.com/haskell-jp/makeMistakesToLearnHaskell/commit/179f62f5455d…
もう1往復である、Wasm版GHCの初期化が終わったことを通知するメッセージがなぜかmainスレッドに届いてませんが、まあ多分単純なミスをどこかでしているんでしょう :upside_down_face:

Agda で、
圏と圏の間の関手を形式化して、
表現可能関手を定義し、
Yoneda の補題の同型変換(の難しい方)を証明しました。
Kleisli 圏とその表現可能関手に適用して、証明の型が通ることも確認しました。

前半は Project Euler を Haskell で解いて　後半は The Hitchhiker's Guide to Logical Verification (2025 edition) の Chapter 8 Metaprogramming をヤリます

S.K.です。ちょっと遅くなってしまいましたが、今週は参加できそうなので、よろしくお願いいたします。
「Implementing Functional Languages: a tutorial」のやり残した部分の続きを進めようと思います。

今日は簡単に bundler-hs の紹介記事を書いて公開したいと思います

山本悠滋です。遅くなりましたが例の如く github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます。

bundler-hs の を公開しました :serval:

「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
3週間くらい間が空いてしまったので、まずは内容を思い出すことから始めて、その後は設定した二つの補題の下位の補題の定義見直しの続きを進めていました。
上位の補題で必要とする形に定義を修正した場合について、証明をどうするかを確認中です。
今週もまだ終わりませんでしたが、可能なペースで進めて行こうと思います。

数学ボーイZの動画 定理を証明するプログラミング言語Leanって？環境構築、入門教材の紹介も！ を見始めらたら面白くて LEAN 4 がどのように使われるかよく分かった　数学的利用例がほとんどであるが
それで今週の Project Euler / Haskell 演習は中止　
The Hitchhiker's Guide to Logical Verification (2025 edition)　眠いがともかく 8.4 First Example: An Assumption Tactic まで読む

先週終わってから気付いた https://haskell-jp.slack.com/archives/CUPBC8WCE/p1791108472003009?thread_ts=1791104799.685939&cid=CUPBC8WCE に基づき、古典的なイベントハンドラーに書き換えてました。眠くて余り捗らず。