haskell-jp / mokumoku-online #87

キリがいいのでここまでで。まだ主要な節が残ってるけど、果たして何パーセント終わったんだろう。半分は終わったと思うけど...

ちなみに例はJavaScript風の構文の疑似言語で書いているので、Haskellは出なさそう :sweat:
言及する機会は多少あるけど

Project Euler #138 Pythagorean triples の Euclid's formula を用いて | b - h | == 1 その近くを２次方程式で近似して全探索　一発 OK 　Lean の文法書ばかり読むのはホント退屈で飽きてきた　いろいろと Haskell 似なところは良いとして　それで？という疑問が去らない　実用的にどこが良いのかもっと入門者に訴えてくるものが欲しい

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
depthFirstSearch 関数に渡す頂点のリストが空でない場合について、リストの先頭要素が訪問済み頂点集合に含まれる/含まれないの場合分けを行い、とりあえず含まれる場合から進めていますが、
<訪問済み頂点の集合> ∪ <これから訪問する頂点の集合> ⊆ <depthFirstSearch 関数が返す頂点の集合>
となっていることを想定して証明を書いていたので、遅まきながら本当にそうなのかを確認中です。
今週も終わりませんでしたが、またほんの少しは進んだかなという感じです。

前半は Project Euler を Haskell で解いて　後半は Lean の 5. Functors, Applicative Functors, and Monads をヤリます

山本悠滋です。関数型まつりでHaskellが名前だけ出てくる発表をします！

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

Project Euler #139 Pythagorean triples の Euclid's formula 等を用いて既約の３角形を求め　それらの周長の倍数が範囲内の和　GHCi でヤッテも遅いがかろうじて有効　さて Lean であるが Functor, Monad, Applicative が長々と例えを用いて説明されるていて　Haskell を知る者には笑える　お手並み拝見とばかり余裕で読み進める　inheritance の挙動がフツーの OO と異なるのは異様　つまり何のためなのかワカラン　これもタダタダ黙って読み進める　コーユー息の長い説明が独学者の悲しみなのよね

無事発表終えました。よい反応が大半の中で、確かにな、と思う指摘も頂き反省。

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
trace を組み込んだ depthFirstSearch 関数の非常に簡単な単体テストプログラムを作成し、入力頂点列や有効辺の情報や初期状態を色々変更して動作を確認してみました。最初にこれを行っておくべきでした。
確認結果を踏まえて、任意の初期状態ではなく、問題文通りの初期状態 ({}, []) に戻して証明を作成中です。
今週も終わりませんでしたが、またほんの少しは進んだかなという感じです。自分にとってはまだ先は長いですが、可能なペースで進めて行こうと思います。

前半は Project Euler を Haskell で解いて　後半は Lean の 6. Monad Transformers をヤリます

山本悠滋です。久々に github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます。例の如く昼寝しながらほどほどに。

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

進捗ゼロでしたのでもうちょっと頑張ります

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
depthFirstSearch 関数の2重の再帰構造に合わせて、外側の再帰(処理対象の頂点リストをたどる)と内側の再帰(開始頂点から辺をたどる)を分けて証明しようとしています。
今週も終わりませんでしたが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。

Project Euler #140 Modified Fibonacci Golden Nuggets 解いた　Pell の方程式にして　その recurrence formula を用いて集計する
後半は Lean4 のやや退屈なドキュメント読みに終始する　まだ章末にまで達してイナイ　もう少し読んでみようかな

これまでにやってきたことを思い出しつつ、GHC版Wasmをビルドするスクリプトにバグがあったので直しました。
次回はGHC版Wasmを動かすときにハングする問題に、ひとまずprintデバッグで挑もうと思います。

前半は Project Euler を Haskell で解いて　後半は Lean の 7. Programming with Dependent Types をヤリます

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

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

toyboot4e です。 AI に競プロ用の bundler-hs を作ってもらいます

ghc-lib-parser を使ったベース部分ができました。 CPP 言語拡張と (AI が) 格闘しています。

地道にデバッグコードを仕込んだところ、どうも何故かエラーが握りつぶされているようでした

握りつぶしているのは自分だった... :weary: 。`Promise`の挙動を誤解していました。

ビルドしたtarファイルの中身がおかしいらしいことまで分かりました。

tarファイルの中身見たら直ぐ分かりました。ディレクトリーの構成がおかしい。tarコマンドの時にカレントディレクトリー変えなきゃダメかー

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
depthFirstSearch 関数の外側の再帰(処理対象の頂点リストをたどる)と内側の再帰(開始頂点から辺をたどる)に関する補題を立てて、それらを使って主定理の証明の骨組みを考えています。
まだどちらも証明できてないですが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。

Project Euler #141 Square Progressive Numbers 解けず　a naïve solution では例題の "10^5" も有限時間内計算できない　とりあえず今日はギヴアップ
後半は Lean4 の退屈なドキュメント読みに終始するが　だいたい Haskell でも Dependent Types がよく分かってナイため　カタツムリの歩みで苦戦中　トホホ

前半は Project Euler を Haskell で解いて　後半は Lean の Interlude: Tactics, Induction, and Proofs をヤリます

AtCoder 用の bundler-hs を AI に生成してもらいます

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

山本悠滋です。昼寝が長引いて遅くなってしまいましたが、引き続き github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます

@ has joined the channel

途中参加かつ40分くらいだけですが、もくもくさせていただきます！
「はじめての圏論」を読み進めます！

もくもく終わります！
お邪魔しました！

はじめての圏論2章
圏論の理解に役立つらしい、最大公約数の話を読み進めました！
準備編なのでまだ圏論には到達できず…:melting_face:

プログラマのための圏論をチラ見しても前提知識が足らずに挫折したので、早いとこ雰囲気だけでも理解すべく引き続き読んでいきたいと思います！

ようやくWasm版GHCを読み込むのに成功しました（まだ呼び出せてはいないので本当かどうかは怪しい）。次どうするか、ちょっと忘れてるので思い出そうとしています。
ここ2週間の成果: https://github.com/haskell-jp/makeMistakesToLearnHaskell/commits/57a9e7cc9aeeb65ff92c945150b700a148c568ca/?since=2026-08-02&until=2026-08-02

bundler-hs の大枠ができたみたいなので、実戦投入してみます。安定したらブログにします！

Project Euler #142 Perfect Square Collection 解けた　変数変換で候補を構造的に絞るのがミソ
後半で Lean4 のこの「幕間」の章は今までで一番納得のゆくものだった　定理とその算譜の手法をどのように結びつけるのか（つまりプログラミングそのもの）　また対話的支援がどのように使えるか（つまり LEAN の repl たち）　などが良く解説されている　何だろうこの本題が分からず閑話休題だけ分かるという本は？　圏論の時もあったような....　何冊も実践・格闘・挫折・積読するうちに何となくじわっと沁みていたアレ　独学者の悲しみ

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
depthFirstSearch 関数の二重再帰に関する補題を立てて、それらを使って問題文の主張の証明を試みていました。
証明中に、「トポロジカルにソートされた列」の定義とグラフに循環があった場合との整合がうまくとれていないことに気づいたり、問題文の頂点集合 V の条件と関数 outs の定義に違和感を感じたりして、それらを解消すべく見直し中です。
今週もまだ終わりませんでしたが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。