2011年の振り替えり
もう2011年も終わりなので、参加したイベントを中心に、今年を振り替えってみたいと思います。
今年もいろんなことがありました。
1月: /usr/bin消失
年明け早々、/usr/binを消しました。 そして、iMacが壊れて、SnowLeopardのディスクを飲み込まれました。
新年を新マシンとともに始めることができた、と前向きにとらえたいと思います。
2月: 名古屋Ruby会議 02
2011年最初のビッグイベントでした。仕事の都合で前日まで東京に居たので、移動が大変だった記憶があります。
裏イベントで名古屋Reject会議02を企画したら、いろんな人が応募してきてくれて嬉しかったです。
ただ、Reject会議にずっと居たので、本会にほとんど参加できなかったのがちょっと残念です。
2月: AsakusaSatelliteリリース
[twitter:@suer]さんと[twitter:@mallowlabs]さんとSkypeで話しながら作ってたチャットアプリAsakusaSatelliteをこのあたりでリリースしました。codefirst名義でいろいろなソフトウェアをリリースするようになったのも、このあたりな気がします。
3月: リリカル合宿
「えっ、[twitter:@wof_moriguchi]さん、リリカルなのは見たことないんですか? それは一度、お泊まり会をやってみないといけないですね」という訳のわからない理由で合宿イベントをやりました。結局、日程が合わず[twitter:@wof_moriguchi]さんは来れなかったし。
ホントは温泉でやりたくて熱海の宿とかを調べてたんですが、移動の都合とかも考えて名古屋市内になりました。いつかは温泉イベントもやりたいです。
合宿中は、[twitter:@lgfuser]さんがが徹夜でAndroidで動くソースコードビューワを書いてたのが、すごく印象に残ってます。鼻血も出してた気がします。
3月: TDDBC福岡
suer「TDDのリズムが今ひとつわかんないんだよね」mzp「それはTDDBCに行くしかないですね。次は福岡でありますよ」というわけで福岡まで行ってきました。
TDDBC中に@ukstudioさんにrspecのすごさについて教えてもらいました。「うーん、このテストの出力、文法的にちょっと…」という言葉がすごく印象に残ってます。
4月: 第3回MessagePackハッカソン（春）
2010年の末ごろからこそこそ作ってたMessagePack for OCamlをたずさえてMessagePackハッカソンに参加しました。参加してる人たちがみんなすごいひとたちばかりでビクビクしてましたけが、たのしかったです。
この時、始めて夜行バスを使って東京に行ってみました。そして、これ以降は使ってません。
4月: ActionScriptを使わないFlash勉強会
Reject会議で[twitter:@yoya]さんと「swf生成たのしいですよね」という感じでもりあがったので、東京で勉強会をやりました。 「今アツいのはJavascriptによるFlashプレイヤーの再実装ですよね」という頭がおかしいとしか思えない会話がそこかしこで聞こえて、とても楽しかったです。
あとFlashの勉強会には女性が多いというウワサを聞いてましたが、完全にデマでした。
5月: Boost.勉強会 名古屋
C++とかよく分からないのにBoost.勉強会で発表したりしました。 とりあえず「エラーメッセージが多すぎて読めない」というジョークが鉄板ネタだということだけは把握しました。
発表はFrama-Cネタをしたんですが、やっぱりCを検証するのはいろいろと難しいので、素直にCoqを使ったほうがいい気が最近はしています。
6月: 開発環境勉強会
つくばのほうでやってた開発環境勉強会に影響されて名古屋でも開催しました。
そろそろ第二回をやってもいい時期な気がします。
7月: Codefirst合宿
2月にリリースしたAsakusaSatelliteを大幅にリファインしました。あまりに変更しすぎて、まだ新バージョンをリリースできてまん(>_<)。 年明けには出す予定です..。
このとき使った京屋旅館 http://kyoya.to/ は駅から近い、WiFi完備、コーヒー飲み放題、プリンタ完備という謎の充実っぷりだったので、クリスマスソンでも再利用しました。
9月: 品川駅に閉じ込められた
台風直撃と東京出張が被って、品川駅に6時間ほど閉じこめられました。 品川駅にはたいぶ詳しくなりました。
9月 函数型プログラミングの集い・Proof Summit
いろんな話が聞けて、すんごい楽しかったです! みんなすごかった!!
あとLtGのキャラは、とてもかわいくてよいです。ボクはCopyくんがすきです。
10月 芋煮会
よんたさんこと [twitter:@keita44_f4] が「冬になったのに芋煮会をやらないとかないわー」と行って主催してまいた。
飲みすぎたので、乾杯をしたあたりからの記憶が非常に断片的でよく分かりません。とりあえず、芋煮はおいしかったことは覚えています。
11月: LL名古屋
夏の間は輪番休日せいで勉強会の主催も参加もあまりできなかったので、そのうっぷんをはらすようなめちゃくちゃなイベントでした。
勝手にプログラムに組み込んでから、発表交渉を始めるという新境地に至りました。
Webサービスの埋め込み用HTMLを手軽に取得するためのWebAPI『QuoteIt』を作りました
# この記事は名古屋クリスマスハッカソン2011で書いてます。メリークリスマス!
GistとかTwitterとかの最近のWebサービスは他のページに埋め込めるようになっていますね。ただ、サービスごとに埋め込むためのHTMLコードが違うので、いちいち調べるのが面倒ですよね。
そこで各種Webサービスの埋め込み用HTMLを統一的に取得できるWebAPI『QuoteIt』を作りました。しかも、誰でも引用元を簡単に追加することができます。
使い方
URLを指定すると、埋め込み用のHTMLを取得できます。
例えば、
http://twitpic.com/73wiod
を埋め込みたい場合は、
http://quoteit.heroku.com/clip.html?u=http%3A%2F%2Ftwitpic.com%2F73wiod
にアクセスすることで、埋め込み用のHTMLを取得できます。
対応サービスの増やし方
埋め込み用のHTMLを取得するためのメタデータはwedataで管理しています。 そのため、OpenIDを持つ方ならば誰でも対応サービスを増やすことが可能です。
例えばTwitter引用は、下記のコードだけで対応できます。
wedataの定義方法についてはドキュメント を参照してください。
対応サービス
それ以外の対応サービスはプラグイン一覧で確認できます。
ソースコード
ソースコードはgithubで管理しています。MITライセンスですので、ご自由にお使いください。
https://github.com/codefirst/quoteit
ちょっと便利な関数の紹介
(* この記事は、F# Advent Calendar 2011の16日目の記事です。 *)
こんにちは、mzpです。 クリスマスたのしみですね。
さて、関数型プログラマは自分だけの関数を持っていることが多いものです。 ライブラリ化にするほどの規模でないので、コピペによって各プロジェクトを移動しながら、洗練されたり新しいオペレータが追加されれたりします。
というわけで今日はOCamlﾊｶｰのosiireさんのオペレータを紹介していきます。
F#標準
まずはF#だと不要な関数です。
let id x = x let (@@) f x = f x let (+>) f g = g f let (+$) f g x = f (g x)
それぞれid, (<|), (|>),(<<)に対応してます。「え、こんなのもデフォルトで定義されてないんですか(笑)」と言うと効率的にOCamlerをdisれるのでおすすめです。
Haskellからの輸入
Haskellで定義されている関数を輸入した関数です。
let curry f x y = f (x, y) let uncurry f (x, y) = f x y let flip f x y = f y x
順番を入れ替えたりできるので、引数の形を変更するだけの無名関数を書くのを避けれます。
> List.map (fun (x,y) -> x + y) [(1,2); (3,4)] val it : int list = [3; 7] > List.map (uncurry (+)) [(1,2); (3,4)] val it : int list = [3; 7]
無限ループ
無限ループするための関数です。
let rec forever f x = let v = f x in forever f v
同じ処理を繰り返すプログラムの本体部分で使ったりします。
let _ = forever read_eval_print ()
例外とOption型の変換
let maybe f x = try Some (f x) with e -> None let may x f = match x with None -> None | Some v -> Some (f v) let may_default d f = function Some v -> f v | None -> d let default d = function Some v -> v | None -> d
option型を返さずに例外を投げてくる関数を扱うための関数です。
maybe List.hd xs |> may do_something_for_head |> default 0
ただ複数引数とる関数の場合は、ちょっと不恰好になります。
(* List.tryFind相当 *) maybe (List.find x) xs
デバッグ用
let tee f x = ignore (f x); x
Unixのteeコマンドのように処理を挟みこんだりするときに便利です。
do_A () |> do_B |> tee printfn |> do_C
みたいにすれば、パイプライン中の値を覗けます。
最後に
人のコード読むのはたのしいですね。
Show Scriptコマンドによる証明の整形
(* この記事はTheorem Proving Advent Calendar 2011の5日目の記事です。 *)
Coqはタクティックを使って対話的に証明を構築していけます。その反面、注意して書かないと、読みにくい証明になってしまいます。
そんなときは、Show Scriptコマンドで整形すると楽になります。
例： 読みにくい証明
例として次のようなリストに関する補題を証明するときのことを考えてみます。
Require Import List. Lemma rev_app_distr : forall A (x y:list A), rev (x ++ y) = rev y ++ rev x.
Focusを使ってサブゴールを移動しながら証明したり、インデントなしで場合分けの証明したりすると、こんな感じの読みづらい証明になってしまいます。
Proof. induction x as [| a l IHl]. destruct y as [| a l]. Focus 2. simpl. rewrite app_nil_r. auto. Show. simpl. auto. intro y. simpl. rewrite (IHl y). rewrite app_assoc. trivial. Qed.
Show Scriptコマンドによる証明の整形
そんなときは、Qedの直前にShow Scriptコマンドを使うと、次のような整形した証明を出力できます。
induction x as [| a l IHl]. destruct y as [| a l]. simpl. auto. simpl. rewrite app_nil_r. auto. intro y. simpl. rewrite (IHl y). rewrite app_assoc. trivial.
Focusによるサブゴールの入れ替えを元に戻して、場合分けごとにインデントしてくれます。
ただ、"現在の証明"に対してしか使えないのでQedする前でないと使えませんし、コメントはすべて消えてしまいます。
おまけ: そのほかのShow XXXコマンド
ちなみに、Show Script以外にも、証明木を表示するShow Treeコマンドもおもしろいです。
先ほどの証明をShow Treeすると、次のような証明木を出力できます。
BY induction x as [| a l IHl] A : Type ============================ forall y : list A, rev (nil ++ y) = rev y ++ rev nil BY Evar change ============================ forall y : list A, rev (nil ++ y) = rev y ++ rev nil BY destruct y as [| a l] ============================ rev (nil ++ nil) = rev nil ++ rev nil BY Evar change ============================ rev (nil ++ nil) = rev nil ++ rev nil ….
まとめ
Show Scriptコマンドで証明を整形すると、たのしいですよ。
LL名古屋 開催経緯
11/5にLL名古屋というイベントを開催されました。
プログラムを見てもらえば分かりますが、いわゆるLLではなく「Lが2個はいっていれば、それはLLです」がテーマのLT大会でした。
開催経緯
発端
OSC Nagoya 2011とLL Planetの開催日が同日だったせいでLL Planetに行けなかったし、輪番休日のせいで休日が分断されて勉強会が開催しづらくてムカつく、という話をミスドでしていたらいつのまにか決まっていました。反省はしていません。
「Lが2個あれば何でもOK」ルールは、いわゆるLLのみにテーマをしぼってしまうとCoqの話ができなくなりそうだったからです:D。 あと発表者が集めにくそうだったというのもあります。
ロゴが多い理由
しらない。
当日の様子
VSTTE Competition参加記録
id:yoshihiro503さんに誘われて、VSTTE Competitionというソフトウェア検証コンテストに参加しました。
「検証ツールに特に制限はないぜ」と書かれていたのでCoqを使いました。
競技プログラミンングに初めて参加しましたが、48時間ぶっとうしで同じ課題に取り組むのはとてもエキサイティングで楽しかったです。
一日目
開始直前
- yoshihiro503さんから"uiro,tebasaki,miso,..."と列挙された謎のメールが届く。 どうやらチーム名の候補だったらしいです。
- yoshihiro503さんとSkypeで話しながらbitbucketの準備をしたりする。
- 0:00からの開催に備えて仮眠をとる。
0:00ごろ
- 問題が公開される。 https://sites.google.com/site/vstte2012/compet/problems
- ざっと見た感じだとProblem2,Problem4,Problem5が関数型ぽっかったので、Problem2をボクが、Problem4をpirapiraさん、Problem5をyoshihro503さんが担当することにする。
- 簡単かと思ったProblem2をよく読むと「停止性のない関数を定義しろ」と書いてあって、散々苦しむ。
3:00ごろ
5:00ごろ
- 新聞配達の人が来て、時間の進む速度にびびる。
- なんとかProblem3の疑似コードをCoqに変更することができたので、さすがに寝る。
二日目
9:00ごろ
13:00ごろ
- Problem3がだいたい解ける。あとは細かい補題を示すだけ。
- 五十嵐先生の講義を聞くために大学への移動する。
16:00ごろ
- 五十嵐先生の講義終了。 [twitter:@keigoi]さんとyoshihiro503と合流する。
- @keigoiさんがProblem2について「OCamlで記述してCFMLで証明すればいいんじゃない?」と意味のわからないことを言っていた 。
- Problem3の証明が終わったので、@yoshihiro503さんと一緒にProblem5にとりかかる。
19:00ごろ
22:00ごろ
- 翌日に備えて、早めに就寝。
三日目
8:00ごろ
- 起床。Problem1の続きを始める。
- 関数をCoqっぽくしてるので、特に問題なく進む。
13:00ごろ
- Problem1証明終了。
- メールチェックをするとpirapiraさんがProblem4をhirose_golfさんがProblem2を解き終わっていた。このひとたちすごい。
- 残っているProblem5にとりかかる。
18:00ごろ
- 何もすすまないまま夕方になる。
- partake.in のために名駅に移動する。
20:00ごろ
22:00ごろ
- 帰宅。 Problem5を解くのを完全にあきらめる。
- yoshihiro503さんと現状を確認して、投稿の準備を始める。
23:00
- tarballを作ったりビルドスクリプトを書いたりして投稿。
感想
- めちゃくちゃ楽しかった。次もぜひやりたい。
- 他のメンバーの証明能力がハンパなくてびびる。
- 夜って意外と短かい。
