私が歌川です

@utgwkk が書いている

区切りの効能

わたしはもともと作業に没頭するとなかなか抜け出せないタイプだった. そのため研究室でコードを書いていたところ気がついたら20時を過ぎていたとか,あるいは家で続きを書いていたら朝になっていた,ということがあった.

/remind me 定時です at 18:00 every weekday

ここでは定時の概念はSlackのリマインダーとして顕現する. 平日の18時には必ず定時が知らせられ,気持ちに対する割り込みが起こる. 作業が終わりつつあるときには,それでは今日はここまでやってしまって終わりにしようとなり,あるいは定時近くになると,とりあえずあのタスクぐらいはやってしまおうとなる.

これは時間的な区切りの概念だいたいについて同じようなことが言えるのではないかと思う. 大きな区切りは遠くに見えるけど,どれくらい遠いのかが分からない. したがって小さな区切りによって少しずつ近づいていくのがいいのではないか.

いまは可変でない「定時」という区切りを導入し,まあうまくいっているのではないだろうかという段階. まだ運用を開始して1週間も経過していないので引き続き経過を見ていこうと思う.

皮膚科の効能

5月末ぐらいにもらった薬がなくなって,寒くなって表面がぼろぼろになってきたのでついに皮膚科に行った. 今までどおりの薬をもらって塗ってきたところかなり回復した.

まだ大丈夫とか,お金がもったいないとか,適当に薬だけ買えばいけるやろとかそういうことはないと思っていて,専門家に見てもらって適切な処理を受けるのがいちばんはやいし安い. いま行っている皮膚科は,診察のときにめちゃくちゃ長い世間話とかはなくて,

  • 最近どのようになっていますか
  • このようになっています
  • ではこうしましょう
  • ところで今ほかに困っていることはないですか

で終了するので,会話が苦手な身としてはかなり助かるし,なにより時間がかからない.

wsl-terminal が chsh 認識してくれない問題 (解決編)

utgwkk.hateblo.jp

この記事の続き.

いつの間にか -l オプションで起動したのち exec /bin/zsh が効かなくなったのでいろいろ調べてたところ,なんと -l で起動されるシェルは chsh で指定したものとは関係ないことがわかった!

github.com

そしてよく見ると,この設定ファイルは (wsl-terminalのroot dir)/etc/wsl-terminal.conf のことを指しているらしい. 当該ファイルの shell オプションを書き換えると無事にzshが起動された.

そしてさらに驚くべきことに,当該事項はちゃんとREADMEに書いてあった……. 丁寧にログインシェルを /etc/passwd のものに書き換えるバッチファイルまで添えてあった.

github.com

教訓

READMEを読もう.

ISUCON8 :thinking_face: 本戦に出て14位だった #isucon

チーム :thinking_face: *1 として学生枠でISUCON8の本戦に出場しました. 今回のお題は「仮想椅子取引サービス ISUCOIN」でした.

結果は5,981点で14位(ベストスコアは6,324点)でした. 学生の中では5位だったけれどそれ以前に学生のレベルがめちゃくちゃ高かったですね……*2

やったこと

予選とだいたい同じで,

  • id:wass80 がアプリを概観したのちやっていきのある実装をやる
  • id:nonylene がインフラまわりの作業をぜんぶやる
  • id:utgwkk がSQLを改善したり,すぐできる実装をぱっとやる

という分担になりました.

他のふたりがやったことはそれぞれのブログを読んでもらうとして,ここでは私がやったことを書きます.

https://scrapbox.io/wass80/ISUCON8_%E5%8F%8D%E7%9C%81scrapbox.io

nonylene.hatenablog.jp

N+1クエリの解消

model/ 以下にDBの各tableに対応するモデルファイルが置いてあり,クラスが定義されていました(なんと型アノテーション付き!). じつはこれは罠で,とくにOrderとTradeにN+1が埋め込まれていました.

N+1のある関数が呼ばれるのは精々数回だったので,丁寧に切り出してJOINに書き換えました.

Fix N+1 on /info by utgwkk · Pull Request #7 · innocent-team/isucon8-final · GitHub

Fix N+1 query on GET /orders by utgwkk · Pull Request #9 · innocent-team/isucon8-final · GitHub

_get_latest_trade()LIMIT 1 を付ける

_get_latest_trade() は文字通り最新のTradeを取ってくる関数なのですが,じつは最新の1件しか使わないのでクエリに LIMIT 1 を付け加えました. 確かこれがいちばん効いて,それまで1000点も出なかったのが突然3000点ぐらいまで上がったと思います.

LIMIT 1 · innocent-team/isucon8-final@9783f73 · GitHub

SettingsをRedisから取ってくる

Settingsは GET /initialize でのみsetされ,あとはgetしか行われないので,ここをDBから外す作業をしました. はじめはグローバル変数の dict に乗せていたのですが,そうするとgunicornで起動したときに /initialize を受けたプロセスでしか初期化されずFAILしていました. そのため各サーバにRedisを入れ,そこにSettingsを格納しました.

Do not use database for settings by utgwkk · Pull Request #4 · innocent-team/isucon8-final · GitHub

always get settings from Redis · innocent-team/isucon8-final@24c80be · GitHub

やらなかったこと

インデックスを貼る

今回はインデックスにはとくに手をつけませんでした. 各所に重たいクエリがあるのでまずそちらをどうにかしなければなーと思っていたら競技が終了していました.

ろうそくの改善

ろうそくを出すときにかなり重たそうなクエリが投げられていることは分かっていたのですが,最後までどうにもなりませんでした. MySQL 8.0なのでwindow functionが使えるしなんとかならないか!? と思ったけれどすぐにできるものではなかった…….

SNSシェアを有効にする

終了30分前ぐらいに,SNSシェアしたらどうなるか見てみましょうということで,

res["enable_share"] = True

をやってみたところ当然failしたのですぐに差し戻しました.

懇親会で聞いたところ,appサーバのうちどれか1つだけでSNSシェアを有効にするとか,一定確率で有効にするとかの戦略を取るのが正しかったようです. 巷ではこれをA/Bテストと呼びます.概念は知ってたけどそうする発想が出なかったのでめちゃくちゃ悔しい…….

サーバのリソースにはわりと余裕があったので,少しだけ有効にしてたら10000点は出ただろうなーと思っています.

ユーザのBAN

これも終了30分前ぐらいにエイヤッとやったところ当然failしたのですぐに差し戻しました. そもそもSNSシェアがかなりの割合で有効になってきてから効くようになるとのことだったので,早とちりでしたね…….

感想

テーマとしても面白く,かなり考えられた問題だなーというのが分かりました. 現代のwebサービスはアプリ内部だけ完結せずに外部APIと連携するものが多く,それを踏まえたテーマとなっていたように感じます. 懇親会で他のチームの方や出題者の方々とお話をしたところ目から鱗となる戦略がどんどん出てきて,やはり実力があるなーと思いました.

チームメイトの id:wass80 id:nonylene ,運営の皆様,他チームの皆様,そしていろいろなところでISUCONを支えてくださった皆様ありがとうございました.めちゃくちゃ楽しかったし勉強になりました. 学生のレベルがだんだん上がっており,しかも来年から学生枠がどうなるか不明という話を耳にしてビクビクしていますが来年も出たいです.

*1:team id:18

*2:もちろん社会人枠の方々のレベルもかなり高かった.

KMCの例会講座で「ラムダ計算のインタプリタを実装してみる」話をした

speakerdeck.com

KMCの例会講座で,型無しラムダ計算についての軽い説明と,そのインタプリタを実装した話をしました. できた実装はこちらです.

github.com

講座の流れ

  • ラムダ計算について知ろう
    • ラムダ項
    • 束縛変数と自由変数
    • 変数の置換(代入)
    • α変換
    • β簡約
  • ラムダ計算のインタプリタを実装しよう
    • 仕様の決定
    • データ型の定義 (syntax.ml)
    • 構文解析の実装 (parser.mly)
    • 字句解析の実装 (lexer.mll)
    • De Bruijn indexへの変換の実装 (deBruijn.ml)
    • β簡約の実装 (deBruijn.ml)
    • デモ

動機

ラムダ計算を実装するという体験の共有

ラムダ計算は計算体系の1つで,

  • 関数抽象(関数をつくること)
  • 関数適用

2つの操作によって構成されており,これだけでチューリング完全になります.

わたしは研究分野の性質上,ずっとラムダ計算を拡張した体系の論文を読んでいます. しかし今まで,その数学的な性質を確かめていても,簡約が機械的に行われることは自分の手で確かめていませんでした.

そんなわけで 論文を読むのがダルいときに 実装を進めていました. できあがったものの共有というのが講座をやった動機の1つです.

実際,じぶんの知っているラムダ計算の知識だけではうまく簡約ができず,試行錯誤する必要がありました. そういったつまずき体験を共有し,解決策についても共有する*1ことに講座のもう1つの意味があります.

プログラミング言語の処理系について意識してもらう

プログラミング言語コンパイラインタプリタがどのように実装されているか,というのは,普段のプログラミングではなかなか意識しないことだと思います. そこに少しだけ意識を向けてもらって,ザ・メイキングを見るときのような気持ちになってもらったり,よくわからないけどいろいろな世界があるのだなと思ってもらったりする,というのが講座の動機のもう1つです.

質問

講座のあとに出てきた質問とその回答,フィードバックを記録します.

β簡約のステップがよくわからなかった

私も最初はなぜこれでうまくいくのか全くわかりませんでした*2. 簡約のステップをスライドに示しつつやっていたので,そのスライドを再掲してゆっくり追ってもらいました.

じつはスライドに示した規則はβ簡約の規則の1番目に過ぎません. 項全体だけではなく,項のある一部分だけについても同様にβ簡約してよい,という規則があります. これは住井先生の「計算機ソフトウェア工学」の講義資料などにより正確な説明があります.

今回の講座ではそれを含めずにβ簡約について説明していたので,含めたほうがよかったですね*3

実装期間はどれくらいか

2週間ぐらいで実装しました.10/7には作業をした形跡があったのでそれぐらいの時期からやっていたようです*4

今後どこまで実装していくのか

ひとまずは「今後の課題」に挙げたものが解決できるとよいなーと思っています.

型を付けることに関しては,いちおう単純型の型推論がすでに実装されています. しかし講座でそこまで取り上げると型の説明のために時間が長くなってしまうとみて今回は割愛しました.

De Bruijn indexにおける自由変数の扱いについて,どうにかしたいと書いていましたが,諦めるしかないという結論になってきました. そもそも自由なので外部環境が変化すればindexも変化するため,外部環境が不明な状況では放っておくしかないでしょう.

その後

例会後に今更SICP読書会というSICPを読む会がありましたが,そこでチャーチ数に関する練習問題が登場し,人々が格闘していました.

わたしはWikipediaをチラ見しつつ階乗を求めるラムダ式を書いていました. Y (\fn. IFTHENELSE (ISZERO n) (\fn.fn) (MULT n (f (PRED n)))) を少し簡約したのが以下の式になります.

ところでこの階乗関数からYコンビネータを取り除いても型検査に落ちるのですが,そういうものなのでしょうか.

追記

発表原稿を公開しました

*1:あるいは解決できなくても試行錯誤の過程を共有する

*2:今もぜんぶ分かっているかについては自信がない.

*3:実際に,スライドの参考資料[1]ではβ簡約をleast compatible relation satisfying ~というふうに定義しています.compatible というのが今回示さなかった規則にあたります.

*4:commit logはいちど消し飛ばしてしまった…….

最近ずっとGoogle Homeのアラームを設定して,設定した時間よりちょっと早く目が覚めるというのをやっている. 試しにちょっと早めに目が覚めたらそのまま二度寝したら,アラームで起きたときめちゃくちゃ目覚めが悪かった. 文明を逆手に取って生活リズムが形成されているみたいな形になっている.