おいお前ら、TAPL読むぞ!
こんにちは。VOYAGE GROUP エンジニア blog Advent Calendar 最終日分の記事です。
TAPL(Types and Programming Languages, 型システム入門)を一緒に読もうよという内容になります。
アドベントカレンダー最終日、クリスマス・イブだからおもしろネタ記事かと思った?残念!型システムでした! クリスマスだからって浮かれているようではエンジニアとして生き残れないですぞ!(弊社では社内バーでクリスマスにビールを飲んだり楽器を鳴らしたりしてワイワイする voyarock という会がありますので、興味ある方はぜひ参加してみてください https://atnd.org/events/59995 )
あと、ネタ枠は Slack で役に立たない Bot を運用するときの知見とか - ミントフレーバー緑茶 で勘弁して下さい。
社内読書会について
VOYAGE GROUP では技術書の読書会がいくつかあります。今年参加した/しているものをリストアップしてみると
- SQLアンチパターン勉強会
- @hironomiu の解説付きで、3 周目があるとか
- 参考: http://tech.voyagegroup.com/archives/7759653.html
- ハイパフォーマンス ブラウザネットワーキング輪読会
- 今年の前半に @hagino3000 中心で輪講会がありました
- モバイルアプリケーションの最適化など色々な分野にまたがっていて、参加者の傾向がバラけていていい感じだった
- 参考: http://hagino3000.blogspot.jp/2014/08/hpbn.html
- SICP(Structure and Interpretation of Computer Programs, 計算機プログラムの構造と解釈)輪読会
- プログラムの動作原理を学べる非常に面白い本
- 問題を解いていきながら丁寧に理解していく輪読会で、2 年以上掛かかりましたが最近終わりました
- 2 年掛かってもついてくる人がいるのは、@ajiyoshi のサポートあってこそ
- 参考: http://d.hatena.ne.jp/ajiyoshi/20121226/1356493118
- PRML(Pattern Recognition and Machine Learning, パターン認識と機械学習)輪読会
- @a_macbee を中心に最近始まりました
- 難しいけれどデータ解析周りに興味がある人が多いのか、結構人気(未検定)
と、自分の感覚では質の高い勉強会が開催されています。
最近では上記の勉強会に加えて TAPL 勉強会という、型システムを学ぼうという勉強会を毎週月曜日にやっています。 最初は輪読会のように TAPL のある章を読んで解説するという進め方をしていたのですが、最近の参加者は 2, 3 人で、その少人数で気合入れて資料作ってきてもねぇという雰囲気になり、今はもくもく会の体をとっています。各自で TAPL を好きなように読んで、何かトピックがあればそれについて話すという形です。
以降では TAPL を読む理由や、現在までに自分が 10 章まで読んで学んだことを書きます。取っ付き辛そうと思っている方や、ちょいと割高なので二の足を踏んでるから雰囲気を知りたいと思っている方の参考になったらと思います。
TAPL とは・何が学べるのか
TAPL は型システムについて詳しく解説された本です。動的型付けや静的片付けに関係なく、プログラマなら普段お世話になっている方も多そうな型システムについて理解を深めることができます。
自分が 10 章まで読んで学んだことを箇条書きでまとめると
- 型システムで解決できること
- 型の無い場合はどのような不都合があるのか
- 型無し・型ありラムダ計算器の実装
どういう流れで TAPL を読んでいるか・オススメの読み方
最初は1章・2章・3章…と順番に読んでいましたが順番に読んでいると、証明がよく分からない!自分の頭の悪さよ!!辛い!!!という事態になりがちです(少なくとも自分は)。10 章までの流れだと、定義や証明の多い理論の章=>理論の実装という流れになっており、理論ベースの章に書いてあることを完璧に把握しながら進めるのは難易度が高いかと思います。
幸い実装の章があるので、手を動かしながら全体をゆっくり把握していく学び方が性に合っている方は理論の章を斜め読みした後、実装の方を先にやって、分からないがあったら戻るというやり方がオススメです。実装の章はXXのML実装と書いてある章になるかと思います。
ただし、7 章最後の脚注に「実装したからといって、理解したとは限らない -- Brian Cantwell Smith」とあるように、実装しながら理解すると理解したつもりになって実は間違った理解をしていたとか、実装には現れない部分があったなど「TAPL 完璧に理解した」という状況にはなれないことは気をつけておきたいですね。とはいえ難しい問題や証明があるので、そこで足踏みしたり挫折するなら先に行った方が良い。もしくは「TAPL 完璧に理解した」人に焼き肉を奢ってさっさと教えを請う方が良い(自分の周りには「TAPL 完璧に理解した」人はいないのですが、頭の良い人が多いのが救い)。
各章について(10 章まで)
自分の読んだ 10 章までに書いてある事をまとめます。こっからは個人のチラ裏メモレベルの殴り書きで、TAPL の雰囲気を感じてもらえたらと思います。興味ないとかネタバレ嫌だという方は一気にまとめまで。
1 章 はじめに
TAPL における型システムの定義や、型システムがもたらすものについて書かれている。
型システムとは、プログラムの各部分を、それが計算する値の種類に沿って分類することにより、プログラムがある種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的手法
1.1 節「計算機科学における型」より
- プログラムが想定外の振る舞いをしないよう、評価前に検査する仕組みという理解でいる
型システムがもたらすものとして書かれているのは
- エラーの検出
- 抽象化
- ドキュメント
- 言語の安全性
- 効率性
2 章 数学的準備
- 後から分からない部分が出てきたらここで調べる(飛ばした)
3 章 型無し算術式
- 小さな言語を定義することで、構文や評価の表現方法について学ぶ
- 評価は t という状態を t' へ進めると表現できる
- 1 回だけ評価する関係を 1 ステップ評価関係といい (t -> t') で表せる
- もうこれ以上評価できないという状態の項を正規形と呼ぶ
- 正規形は true/false や数値のような値である場合と、値ではないが評価できない場合がある
- 後者は「行き詰まり状態」であり、数値に1を加えるような関数 succ (後者関数) に false を適用したもの succ(false) は、3章で定義された構文では次にどういう状態になるべきか定義されていない
- 行き詰まり状態を実行時エラーとして表すことができる
4 章 算術式の ML 実装
- 型無し算術式を OCaml で実装する
5 章 型無しラムダ計算
- ラムダ計算は関数定義と関数適用を関数だけで表現する
- 項は 3 種類
- 変数 x
- ラムダ抽象 λx.t
- 関数適用 t t
- 例えば、引数をそのまま返すような関数 id への関数適用 id z は (λx. x) zと表現できる
- 項は 3 種類
ラムダ計算は単純ながら、色々な計算を表現できて強力である
- カリー化による複数引数を取る関数の表現
- Church ブール値 true = λt. λf. t
- 2つ組
- Church 数
- 0 の表現 C0 = λs. λz. z
- 1 の表現 C1 = λs. λz. s z
- 後者関数 s を 0 の表現に何回適用したかで n を表す
- 他にも test (if を表現する)、足し算、掛け算、iszero、不動点コンビネータ等
- 表現力はあるけどパズルみたいな複雑さがあって、よくもまあ定義したなあと思う
- (λm. λn. λs. λz. m s (n s z)) (λs. λz. s z) (λs. λz. s (s z)) が1+2 を表してます!というのは自分で考えつく気がしない
後は代入の形式的定義など
6 章 項の名無し表現
- 主に変数の取り扱いについて書かれており、TAPL のラムダ計算では de Bruijn インデックスを用いる
- de Bruijn インデックス
- k 番目に束縛されたときの番号を変数名として利用する
- そもそもなぜこのような名無し表現が必要かというと、変数に名前を付けた場合名前の重複があると実装上ではどの変数(名前無し)を指しているか分からない
- シフトと代入
- 代入が入ると自由変数だった変数が束縛された場合、インデックスの付け替えが生じる
- また、評価(簡約)の場合は変数が消費されるので、これまたインデックスの付け替えが生じる
7 章 ラムダ計算のML実装
- ラムダ計算を実装する
8 章 型付き算術式
やっと型が出てくる
- 4 章で実装した算術式を静的な型で強化する
- 項を評価する前に「行き詰まり状態」にならないかチェックできる
型システムの最も基本的な性質は安全性
- 正しく型付けされた項はおかしくなることがない
- おかしくなるとは行き詰まり状態になること
行き詰まり状態にならないことを進行定理と保存定理によって証明する
- 進行: 正しく型付けされた項は行き詰まり状態ではない
- 保存: 正しく型付けされた項が評価できるならば、評価後の項も正しく型付されている
9 章 単純型付きラムダ計算
- ラムダ抽象に型がつく
- (λx:Bool. x) :Bool->Bool
- Bool を引数にとり、Bool を返す
- 進行と保存の証明とかは長いので飛ばした
10 章 単純型のML実装
- 実装の章(待ってました)
- https://github.com/jewel12/tapl/tree/master/ch10
- パース後に型検査して、評価する
*Main> run "^x:Bool. x"
"(^x:Bool. x) : Bool->Bool"
Bool->Bool を期待されているのに true が引数なので怒られる例。
*Main> run "(^x:Bool->Bool. ^y:Bool. y) true"
"*** Exception: parameter type mismatch
*Main> run "(^x:Bool->Bool. ^y:Bool. y) (^k:Bool. k)"
"(^y:Bool. y) : Bool->Bool"
まとめ
- 弊社には良質な読書会がある
- TAPL を僕と一緒に読もう!
- 人数が少ないので、社内の方でも社外の方でも興味があればぜひ
- クリスマスだからって浮かれているようではエンジニアとして生き残れない(弊社では社内バーでクリスマスにビールを飲んだり楽器を鳴らしたりしてワイワイする voyarock という会がありますので、興味ある方はぜひ参加してみてください https://atnd.org/events/59995 )
VOYAGE GROUP エンジニア blog Advent Calendar 最終日の記事でした!楽しいクリスマスを!
Slack で役に立たない Bot を運用するときの知見とか
この記事は Slack Advent Calendar 2014 - Qiita の 11 日目の記事です。
Slack のようなチャットツールを導入したら Bot を運用するのが人間の性なので、皆さんのチャンネルでも Bot がワイワイ活気付いてる姿が見られるかと思います。 Slack Advent Calendar 2014 - Qiita を眺めていても、Bot の話がいくつかあるようですね。僕が属している会社の Slack チームでも、jewelpet という役に立たない Bot がいます。
今日は Slack で動いている役に立たない Bot の機能紹介と、それを運用して得た役に立たない知見を紹介します。
機能紹介
社内向けなので身内ネタも多い。
jpi
hubot image me
のエイリアスです。hear
を使って jpi
という文字列に反応するようにしています。jewelpet image hoge
よりも短く jpi hoge
と書けるので、画像コミュニケーションが捗ります。
hubot/scripting.md at master · github/hubot · GitHub
社内マップ
会議室の名前と部屋の位置の対応が覚えにくいのでよく使う。
JSON
便利な気がする
返事
鳥
寿司
他にカンパチや太巻きがあります。
ウィキ
コナミコマンド
ジャバ
ガチャ
進捗
いい話カウンター
ユニックスタイムスタンプ
長い
回文
ビール
距離
あなたとダウンロード
優柔不断
コンパイル速度
その他
- 株:
jewelpet 株 CODE
- n 秒後にコメント:
jewelpet timer 10 コンパイル時間
- あとは夕会の通知とかありそうな感じのは大体あります
知見
200 人以上が利用している社内 Slack チームで、鬱陶しいことに上記の様な糞 Bot が運用されていることを紹介しました。
Slack の利用人数が多くなってくると多くの人の目に糞 Bot の糞機能が触れられるようになるため、なるべく角が立たないように運用したくなるかと思います。糞 Bot が運用されている状況を観察して得た知見は、怒られにくくするには愛着がわきやすい Bot を作るのが大切ということです。下手なことを言っても仕方ないと思わせる、そんな可愛さが必要です。
jewelpet には次のような可愛さがあります。
- バグは極力直さない
- バカな子ほど可愛いという諺がある
- 便利な機能は極力付けない
- バカな子ほど可愛いという諺がある
- ChatOps とかもってのほか
- 特定のユーザーしか使えない機能など、あざとい機能もある
この可愛さのお陰で、今のところ怒られずに運用できているみたいです。可愛いは正義!
おまけ: ロギング
役に立たない Bot を運用することの知見からは外れるのですが、Slack で Bot を運用するときはロギング用チャンネルを作って、そこにログを吐いていくと便利です。例えば hubot-cron のようなプラグインを利用するとき、誰が設定した・設定を外したというようなことが分かります。あと検索もできる。
なんか Slack Advent Calendar というよりも Hubot Advent Calendar という感じでしたが、11 日目の Slack Advent Calendar でした。
ISUCON 2014 の思い出
ISUCON 2014 という、いい感じにパフォーマンスチューニングしてスピードアップさせるコンテストの予選に参加しました(詳しくは http://isucon.net/archives/cat_1024989.html)。ポータルに送った時のスコアは 15000 くらいで、一番良かった時は 19000 くらいでした。結果としては惨敗です。
チーム名は「ドラゴンチャーハン」で、@lesamoureuses と @tana_ra と僕が適当に集まって社内チームを組みました。
この記事のまとめとしては、ISUCON 楽しかった!が、惨敗で悔しいので来年も頑張りたい!です。
反省メモ
以下は社内振り返りのために殴り書きしたメモをもう少し読みやすくしたもの。読みにくいと思いますが、来年参加する人の参考になればラッキーです。
予選に向けた練習
ISUCON 2014 夏期講習の AMI を使って練習(去年の予選)しました。
ISUCON 夏期講習 2014 を開催しました : ISUCON公式Blog
2 回集まって練習し、前半はアプリケーションの把握、後半(前日)はチューニング。 前日に Varnish とかを使ってスコアが大きく上がってワイワイしてました。
役割分担
フロントエンドや DB 周りの調整を @lesamoureuses さん、アプリケーション周りでコード書くのを @tana_ra と僕。 このメモはアプリケーション側をいじってた僕の目線で書かれています。
チューニング要点
- Varnish で /mypage をキャッシュしたり、前日に用意していた秘伝のタレ(設定ファイルの調整)をプロファイリング後に入れる
- できるだけメモリに乗っけるようにコードを書き換える
- ストレージが HDD であることと、メモリが 7.5 GB くらいあると聞いた時点で、I/O を発生させないようにする方針になった
- 後述のインテグレーション失敗で全部はできなかった
序盤
- 午前中
- 人数分のインスタンス起動・webapp 以下を Git 管理
- プロファイリングの準備
- Nginx の設定を前日に用意したものに
- LTSV で吐いて、ログを解析しやすくする
- rack-lineprof を入れる
- プロファイリング
- 当然 /report が遅い。 次いで /mypage が遅い
- /report のレスポンスは加点しないということレギュレーションに書いてあったが見落としていたため、ここをチューニングする方針になった
- アプリケーションの理解・戦略を考える
中盤
- 16 時ごろまで
- Redis のセットアップ
- Ruby から Redis を使う方法など変更の方針を共有
- Redis を選んだのは前日に練習で使っていたのと、reds-objects に Redis::Counter というのがあって、ログイン失敗回数をインクリメントしていくのに便利そうだと考えたため(Redis について全然知らなかった)
- 再起動時してもデータの変更内容を保存しておかないといけないことにサポートチャットで気付いた
- Redis に入れてるデータが消えないようにするスクリプトを作成するなどの作業
- 永続化のノウハウが無さすぎた
- ここら辺で /report のレスポンスを高速化する必要がないことに気付く
- アプリケーション側は Redis データ永続化とアプリ変更の2人に分かれた
後半
- 16 時すぎくらい
- 変更済みコードではデバッグが厳しいとわかったので app.rb をまっさらにして、小さい部分から変更していく
- 決断が遅かった
- 残りの時間ないでできることはギリギリまでやって終了
時間があればできたと思うもの
- 主にアプリケーション周り
- SQL を駆逐するつもりしかなかったのでインデックスを張ってない
- 最初にアプリケーション全体に手を加えるという博打をやらずに、インデックス張ったりに手を出してもよかった
知見・反省点
- 中盤まで /report のことしか考えてなかったので、レギュレーションをちゃんと読む。もはやみんなで音読するレベル
- 仕事のやり方みたいな話だが、大きな変更をするときは小さい仕事に分割してちょっとずつ進める
- 実際に3人で本番を想定して練習することがなく、役割分担が不慣れだったということもある
- 練習が足りない
- 前日に Varnish とか Redis を触りだすレベルだったので、もっと持ちネタを増やして望む
YAPC::Asia Tokyo 2014で当日スタッフをしました
去年に引き続き、当日スタッフをしてきました。
YAPC::Asia 2013に参加したです! - ミントフレーバー緑茶
スタッフと言っても例年通りコアスタッフの方々がしっかり準備してくださっているので、椅子を運んだりマイクを運んだりカキ氷を運んだりするくらいであんまり偉そうなことはしません。イベントは準備がキモですね。イベントホールの状況はコアスタッフでウルトラスーパー PHPer であるところの uzulla さんの記事がよくまとめられてて最高です。
スタッフとしてのYAPC::Asia 2014 レポート(Without about my talk) - uzullaがブログ
イベントホールスタッフを 3 グループに分割して、担当部分じゃないところは他のトークを見に行ったら良い。という提案を uzulla さんがしてくださったので、去年よりトークを見る時間ができて良かった。
以下は自分が見た発表&スライドについて。社内で YAPC フィードバック会があるので、もうちょっと発表スライドを読んでいきたい。
「コマンドラインツールについて語るときに僕の語ること」 @deeeet さん
YAPC::Asia 2014でコマンドラインツールについて語ってきた | SOTA
自分にとって目新しいところはなかったけど、スライドがすごく見やすい&分かりやすい。
「オープンソースの開発現場 - Perl 5.20 のSubroutine Signaturesが来るまでの奮闘の軌跡」 @lestrrat さん
YAPC::Asia Tokyo 2014 オープンソースの開発現場 - Google スライド
Subroutine Signatures を追加するまでのドラマが紹介されていた。皆が使っている既存のものに手を入れるということはそれぞれの人にとって賛否両論ある。自分にとっては良かれと思ってやっていることもいろいろな人にいろいろなプライオリティがあるから、否定されることもある。そんな中で自分のやりたいことを実現するには、コードを書いて実装するというだけではなく、やりたいことが実現するように仕向けていく人間力・政治力という、本質的ではなさそうなものが残念ながら必要になる。
大切なのは「自分以外の人は別のプライオリティを持っている」ということを認識し、それを持った上で立ち止まらず進み続けることかなと思う。他人が別のプライオリティを持っているということを知ると、他人がどんなプライオリティを持っているかという点を考慮しながら人間力・政治力を振るうために役立つし、人間力を発揮しなくても、他人の意見は他人の意見として過度に傷つかずに無視して我を通すか諦めるかして次に進むことができそう。
個人的には、既に動いている機能に手を加えるようなアグレッシブな変更よりも、質問の時に弾さんが言っていたように sub じゃなくて fun を作ってみるという手もありだったのになぁと思う(予約語が増えて、既に fun を使っているようなコードにダメージがあるかもしれないが)。有力そうな Subroutine Signatures の実現方法のひとつが序盤でバッサリと切られていたというのは残念。
HASH COLOR
ちょっとしたHTMLはGitHub Gistに置いてbl.ocks.orgで表示するのがお手軽です - Qiita で bl.ocks.org を知り、何か試してみたくなって、入力に応じて色を変えまくるやつ作った。ずっと入力してると気分悪くなる。
http://bl.ocks.org/jewel12/f20ed3003e57cf558e2e
bl.ocks.org は gist の HTML を表示するだけというシンプルさが最高だと思う。
SlackのCUI
https://github.com/jewel12/slacui
チャンネル一覧とチャンネルを指定して読むことしかできない。 percol / peco でチャンネルを絞り込むと少しは便利に使えるけど、毎回API叩くから遅くて使いものにならない。
lacui channels | peco | cut -f1 | xargs slacui read
コンパイルログとかに何かしら色をつけたい
最近はHaskellの本を読んでいて写経したり色々試したりするのだけど、コンパイルログの見辛さによって、静的型付け言語の強みであるコンパイル時エラー検出の力が出せていないような気がした(ghcに--colorオプションとかある?)。
社内LTもあることだし、自動で色付けするマシーンを作ろうと思いたって作り始めた。テキストに自動で色をつけるというと、テキストをルールでパースして色をつけるというやり方になるかと思う。しかしいちいちパースルールを書くのもだるいし、テキストを適当に標準入力から突っ込むと適当に色付けしてくれるものが欲しい。
自分が知っている自動色付け方法はCoding in colorという、シンタックスハイライトされない部分にも色を付けて見やすくしてやろうというもの。
Coding in color — Hacking Programs : Code, Programming Idea, Tutorial, Showcase, Experience — Medium
function等のキーワード以外の単語を名前順にソートして、予め用意しておいた色のリストに割り当てていくというやり方になっている。例えばtypoしたときに色が違っていたりするので気付きやすいという利点がある。
他にどうやってログに色付けするかも考えつかなかったのでパクろうと思いHaskellで書いてみようとしたが、自分は想像以上にHaskellに精通しておらず、色々調べながら進めていたら就業時間後の2日かけても出来上がらなかった。余談だけど、System.Console.Rainbow (https://github.com/massysett/rainbow) のコードを読むのはMonoidとかを実際に使っていて、初心者には勉強になった。例えば "text" <> blue <> bold で太い青色文字列 "text" を表わすとして、この組み合わせは "text" <> bold <> blue でもいいみたいな。
今すぐHaskell力を上げるのは厳しいことがわかったので、色付けプログラムをRubyで書いてみたらプロトタイプがLT発表日のお昼休みで出来上がった。
https://gist.github.com/jewel12/b33f73635bbbed2b9e97
入力を空白でsplitしていったものを単語として扱っていて、Coding in colorと同じように着色していった結果。
自分のコンソールではカビが生えたような彩色になってしまった。
元のログはこんな感じ。
他にも色付けする方法ないかと無い知恵を絞ったところ、語の頻度によって、高頻度になるに連れて色を強調していくという方法をとってみた(逆にどうでも良い語だともとれるので強調しないというのもあり)。
カビよりも落ち着いた感じになったが、たいして読みやすくなったようには思えない。"Not in Scope"の塊で色がついてるのはいい感じがする。頻度で色付けする方法の辛いところは、テキストファイルを全部読み込まないといけない点で、コンソールに流れるログに色付けはできない。
個人的には色をつけるだけでもなんとなく読みやすくはなったと思う。カッコ内は1語だったり複合語を考慮したりと適切な粒度の塊に色付けすればもっと見やすくなる予感はある。なんか適当に色付け方法を考えて試してみて、偶然いい感じになってくれたらと期待してたけど、まずここに色をつけて欲しいというふうに自分で色付けしてみてから、それに合わせて色付け作戦を練っていくアプローチが真っ当だったっぽい。
ご意見ご感想お待ちしております。