Free モナドについて考えたこと　メモ

なんかはてなブログ重くないですか？タスクマネージャを開いて確かめたので間違いない

Free モナド

こういうやつです 1 (ただし、fはFunctorのインスタンスであるとする)

data Free f a = Pure a
              | Join (f (Free f a))

JoinじゃなくてFreeと書かれていることもあるけど、今回はJoinで行きます

これを GADTs で書くと、以下のようになる:

data Free f a where
  Pure :: a -> Free f a
  Join :: f (Free f a) -> Free f a

なんてこった！これではまるでMonadのreturn(Applicativeのpure)やjoinにそっくりではないか！ということで、なんとなくモナドっぽいデータ構造になっていることがわかる

実際、以下のようにしてMonadのインスタンスになるらしい

instance  (Functor f) => Monad (Free f) where
  return = Pure

  Pure a >>= f = f a
  Join x >>= f = Join $ fmap (>>= f) x

だけど、本当か？「モナドっぽい見た目だからモナドです」なんて小学生の屁理屈の亜種みたいなものが、本当にモナド則を満たすのか？というお気持ちが発生してしまう

モナド則

return x >>= f == f x -- (1)

m >>= return == m -- (2)

(m >>= f) >>= g == m >>= (\n -> f n >>= g) -- (3)

確かめてみましょう！

return x >>= f
  == Pure x >>= f -- `return`の定義
  == f x -- `(>>=)`の定義

Pure a >>= return
  == return a -- `(>>=)`の定義
  == Pure a -- `return`の定義

Join x >>= return
  == Join $ fmap (>>= return) x -- `(>>=)`の定義
  == Join $ fmap id x -- 帰納的に (2) が成り立つ (*)
  == Join x -- ファンクタ則

(Pure a >>= f) >>= g
  == f a >>= g -- `(>>=)`の定義
  == (\n -> f n >>= g) a -- ベータ変換
  == Pure a >>= (\n -> f n >>= g) -- `(>>=)` の定義

(Join x >>= f) >>= g
  == (Join $ fmap (>>= f) x) >>= g -- `(>>=)` の定義
  == Join $ fmap (>>= g) (fmap (>>= f) x) -- `(>>=)` の定義
  == Join $ fmap (>>= g) . fmap (>>= f) $ x -- 関数合成
  == Join $ fmap ((>>= g) . (>>= f)) x -- ファンクタ則
  == Join $ fmap (\a -> (a >>= f) >>= g) x -- 関数合成の展開
  == Join $ fmap (\a -> a >>= (\n -> f n >>= g)) x -- 帰納的に (3) が成り立つ (*)
  == Join $ fmap (>>= (\n -> f n >>= g)) x -- セクション
  == Join x >>= (\n -> f n >>= g) -- `(>>=)`の定義

(*) ここは私が厳密性に確信を持てていない (多分大丈夫だけど) (わかる人は教えてください)

というわけで、(一部怪しい所もありましたが) 無事モナド則を証明できました！今日から胸を張ってFreeを使うことができますね

......っておいおい、これじゃただモナド則を証明しただけになっちゃうよ〜〜〜！！！トホホ〜〜 (終) (もしかしたらあとで何か書くかも)

  1. ちなみに、JoinじゃなくてBindで Free モナドを構成する流儀もあるらしい、あまりよくわからないが↩

(飽きたので途中までしか書いていません) 解説 ABC162 F - Select Half

F は DP の F！

問題

提出

基本方針

こんなんどっからどうみても DP やんけ！dp[i][j] := i (0 ≤ i ≤ N) 番目までで j (0 ≤ j ≤ N / 2) 個選んだときの和の最大値！おらどけどけどけどけ DPDPDPDP Θ(N2)Θ(N2)Θ(N2)Θ(N2) TLETLETLETLE → 高速化しよう

よくよく考えたら、i / 2 より j が大きすぎたり小さすぎたりするのは明らかにおかしいです。常に 0 ≤ (i + 1) / 2 - j ≤ 2 となっていなくてはいけません (たぶん)。なので、j 個選んだときではなく、j 個 (選べるのに) 選ばなかったときとすれば、0 ≤ j ≤ 2 となり、全体で Θ(N) になります。

(飽きたので終わり)

チョコレート

GABA 配合　ストレスの緩和によい

ふつうの　おいしい

ホワイト　あまあまあままなので1番すき

カカオが濃いやつ　香りがよい　これもすき

アーモンド入ってるやつ　おいしいけど口の中がアーモンドまみれに

クランチ　うまい　ちょっと塩気があるとよりよい

いちご　うまい　酸味がよい

酒が入ってるやつ　食ったことなし (未成年なので)

麦チョコ　うまい　こぼすと見つからない

きのこ　すき

たけのこ　すき

JOI のときに土産屋で買った、フルーツ味の七色のやつ　めちゃくちゃうまかったけど検索しても見つからず　詳細求む

アルフォート　うまい　何種類かあるけど、違いがわからず

中にちっちゃいマリオのフィギュアが入ってるエッグチョコ　とても懐かしい　クソガキのころめちゃくちゃ喰ってた　𝒎𝒆𝒎𝒐𝒓𝒚の味……

𝑴𝒆𝒍𝒕𝒚𝒌𝒊𝒔𝒔　うまし　いっぱい食うときつい

追伸

左頬からだけヒゲみたいなのが生えてくるの、なに？

青コーダー zer0-star が爆誕してしまった！！！

青色になりました　うれしみ〜〜〜

rating graph

history

青になったおきもちなど

水色になってから3ヶ月、思ったより短かったですね…… 3000000ヶ月くらいかかるかと思った

レートやパフォーマンスの推移を見ればわかるように、俺は元から強かったのではなく、競プロを始めた時は茶色くらいの実力だったっぽいんですよね。つまり、今の実力は成長の結果ということです！
AtCoder で「圧倒的成長」💪😤💪
青になったことに「圧倒的感謝」🙏🙏🙏

ということでね、これから黄色を目指していくことになると思うんですが、それは青になった以上に大変な道のりになると思います (そもそも水色に落ちて一生あがってこれない可能性もあるのでね) 。なので、みなさん、応援よろしくね！！！！！

青になるまでに覚えたアルゴリズムなど

  • 青になるまでに必要とするものは無い、または忘れた (追記: これ、水色から青まで、ってことね！！！) (追記2: 名前のついたやつはない、ってことね！！！) (追記3: 俺の場合は、ってことね！！！)

いや、水→青くらいだと新しく覚えるアルゴリズムやデータ構造ってあんまり無くて、考察の過程や解法のパーツとして名前のない典型や今まで覚えたものが無数に転がっているって感じな気がする (気がするだけかもしれないですが)

おわり

おわり！！！

水色になったよ

zer0-starくんは水色になりました やったね！ ratingGraph

遍歴

競プロを始める前

初めてプログラミングに触ったのは、3DS のプチコン (言語は、SmileBASIC というらしい) その後、パソコンを入手した後は C 言語を始める。正直 C は今でもよくわからない

その後、C から別の言語に乗り換えようというところで、Nim に出会った。 Nim は神！(神なので……)

その後、Nim のお勉強を始める　 今ではわりと Nim に詳しくなった気がする

灰色

正直、この期間のことは覚えてない (グラフを見ればわかるが、灰と茶の間には大きな虚無があるので)

茶色

競技プログラミングに復帰！ちなみに、復帰した時のコンテストはunratedでした (ぴえん)

一度ゴミみたいなパフォを出して爆冷えするも、直後に水パフォを出して爆温まり！何があったんでしょうね

緑

低迷期

緑になった時にレートが収束し始める　 この辺りから、コンテストには欠かさず出るようになった

Twitterアカウントを作ったのもこの辺りである

上昇期

収束しかけたと思った rating が上がりはじめる！ うれしい

この辺りから水色が見えてきはじめて、たのしくなってきた

水色

今です　 水色になってから、すごく調子がいい (そうやって喜んでいられるのも、今のうちですよ)

水色になるまでにやったことなど

ライブラリを整備した

ライブラリ整備は楽しいっすね＾〜 (コンテストには、結び付かないが……)

まあ、実際コンテスト本番で使ったのは (テンプレートを除いて) modint くらいしかない

実は、ライブラリのコードを手元に貼るための VSCode 拡張機能も作っていました　 使いたい人がいたら、勝手に使ってくれ

俺のライブラリ github.com

VSCode 拡張 github.com

アルゴリズムのお勉強

累積和とかにぶたんとか、DFS とか BFS とかくらいはかけるとうれしい　 AOJ の Course をやれば身につきそう (まあ、Nim を使っている俺には無理なことですが)(Nim は使えないので)

できるようになっったアルゴリズム・データ構造など (使いこなせるとは言ってない)

  • にぶたん
  • 累積和
  • DFS/BFS
  • Floyd--Warshall
  • UnionFind
  • ModInt
  • その他 (忘れた)

最後に

この記事を書いている途中で、他人の色変記事を見ようとして検索していたら Twitter が 2 回もフリーズしました　クソ

EdDP A~Cのおきもち備忘録

忘れないように書く　俺のために書く

リンクはこちら Educational DP Contest - AtCoder

A - Frog 1

典型的なやつですね 多分書かなくても忘れないので書きません 配っても貰ってもいいですが、端でIndex Out of Boundsしないように気を付けましょう

B - Frog 2

Aの改変です インデックスがあふれないように気を付けつつ、forで回しながらchminすればよいです

C - Vacation

基本的なことはAやBと同じです

dp[i][j]をi日目に活動j(Aなら0、Bなら1、Cなら2)を行ったときの幸福度の最大値 と定めると、以下のような遷移式が立てられますね(正直これを全て書くのは非常にめんどくさいので、コピペかforをうまいこと回すのが楽です)
dp[i+1][0] = \max(dp[i][1], dp[i][2]) + a_i dp[i+1][1] = \max(dp[i][2], dp[i][0]) + b_i dp[i+1][2] = \max(dp[i][0], dp[i][1]) + c_i

類題: D - パスタ (Pasta)

終了

めんどくさくなったのでCで終わり

古いNimでSegmentation Faultがコンパイル時に出るコード 

type
  Test = concept x
  Obj[T: Test] = object

proc f[T: Test](): Obj[T]

理由はわからないが、古いNimではセグフォが出る。Wandboxというサイト(オンラインでプログラムが実行できて、言語やバージョンも選べる)を使って調べたところ、0.17.0ではセグフォが発生するが、0.17.2ではimplementation of 'f()' expected(一部省略)と怒られるだけである。謎だ。

以下おまけ(見なくてもよい)

このままだとモヤモヤするので、調べてみることにする。すると、今回のケースにマッチするissueと、その修正commitが見つかった。

github.com

github.com

どうやら、sigmatch.nimに一行追加があったらしい。(色が非常に見にくいのは許してほしい)

    of tyUserTypeClass, tyUserTypeClassInst:
-     # consider this: 'var g: Node' *within* a concept where 'Node'
-     # is a concept too (tgraph)
-     let x = typeRel(c, a, f, flags + {trDontBind})
-     if x >= isGeneric:
-       return isGeneric
+     if c.c.matchedConcept != nil:
+       # consider this: 'var g: Node' *within* a concept where 'Node'
+       # is a concept too (tgraph)
+       let x = typeRel(c, a, f, flags + {trDontBind})
+       if x >= isGeneric:
+         return isGeneric

うーむ、なんのこっちゃわからん。このc.c.matchedConceptが重要らしいが、よくわからない。sigmatch.nimを見てもわからないので、諦める。モヤモヤするが、仕方のないことだ。

残念ながら、俺にわかったのはここまで。非常に中途半端な終わりだが、しょうがない。この調査ログはメモとして残しておくので、有識者の方はいろいろ教えてほしい。