「TaPL読書会 第1回」に参加しました

2012/7/17(火) 「TaPL読書会 第1回」に参加してきました。

PARTAKE
http://partake.in/events/b42e1272-dcfc-44b2-93cf-aee790e07dee

Ustream
http://www.ustream.tv/recorded/24052808

Types and Programming Languages (2002/02/01) Benjamin C. Pierce 商品詳細を見る

会場は株式会社ワークスアプリケーションズの1Fラウンジです。
JR新橋駅からほぼ１本道なのですが、歩いて１５分ほどかかるのです。
しかも、この日は今年一番の暑さだったらしく、群馬県の館林では39℃だそうな。。。
日は沈んでいるものの、これだけ暑いとさすがに汗だくになりますねー


さて、私がこの勉強に参加したいと思い立ったのは大きく３つの理由があります。

■１．関数型言語（特にHaskell）への興味
■２．英語のお勉強
■３．大学院生の頃のリベンジ

いちおう、簡単に紹介しておくと。。。

■１．関数型言語（特にHaskell）への興味

去年は「スタートHaskell」という勉強会に参加していて、そして今年に入ってから「スタートHaskell2」という勉強会に
引き続き参加しています。ここで出会ったHaskellという関数型プログラミング言語が、これまた興味深いのです！
普段はJavaをメインに使って仕事をしていますが、それ以外では、これまでC言語やC#, VB.NETといった
オブジェクト指向型あるいは手続き型の言語を中心に経験を積んできました。
（あと他にはJavascriptやPerl, ExcelVBAなども仕事で使ってます）
そんな私にとって、Haskellの思想を学んだときは一種のカルチャーショックを受けましたね。。。
そしてHaskellの特徴でもある型システムについても学んでみたい、と思った次第です。


■２．英語のお勉強

最近、ウチの会社でも、グローバル！ぐろーばる！　と盛んに言われるようになり、英語の習得が
避けられない状況になってきました。。。　上司や後輩も、最近海外出張とか海外研修に行ってるし。
んで、どうせ英語を勉強するなら、モチベーション高く学習したいなぁ、と。
それならば、自分が興味あるIT系の原書を読む読書会を見つけ、参加すればいいんじゃないか！と思ったのです。
なんと単純な考え。。。
でも勉強って、やっぱモチベーションが大事だと思うのです。好きこそ物の上手なれ、です。


■３．大学院生の頃のリベンジ

現在、このTaPL読書会以外にも、名古屋大学でTaPLの勉強会が定期的に実施されています。
実は、私の母校なんです～
大学院の所属は情報科学研究科だったのですが、私も輪講で型システムをテーマにした原書を読みましたよ！

でも、あえなく撃沈した苦い思い出しかありません。。。
しかも、輪講の本の名前は忘れましたが、たぶんTaPLだったと思うのです。。。
だって、今読み直しても、すごく見覚えとかあるし！（もう10年近く前のことで記憶が定かではありませんが）
というわけで、今回は当時のリベンジなのです。今回この読書会に出会ったのは運命とすら感じた。
大学の後輩もTaPL頑張っていることだし、私も頑張ろう！
で、でも、ついていけるかなぁ。。。



さて、オープニングは@none_tokaさんによる1章「Introduction」の発表です。

TAPL勉強会 第1章 (2012-07-17) from none_toka

なんと、大学院でもずっと型システムを研究されていたとのこと。

発表は全体的に非常にわかりやすく、いかにもTaPLを極めていることが窺い知れる内容でした。
なによりも、発表から型システムに対する愛を感じた！

やっぱ、この難解な書籍を読み進める上で、有識者がいるのといないのとでは、大きな差が出ると思うんです・・・

1章の発表のポイントを、スライドから抜粋して以下に纏めてみます。

---

■プログラミング言語における型システムとは
　→　プログラムが「ある振る舞い」を行わないことを文法レベルの分析で保証する手法の１つ

■型システムは、実行時の振る舞いを静的に（コンパイル時に）近似計算しているとみなせる。（静的型検査）

■型システムの有用性
　・型エラーを静的に検出
　・言語の安全性（language safety）の一部を静的に保証
　・実行の効率化（型システムにより、コンパイル時の最適化に有用な情報を収集できる）
　・etc

■言語の安全性と型安全性は同じではない。（前者は、実行時検査でも可能な場合がある）

■型システムと言語の設計は連携して行うべし！
　理由：　互いに文法／機能レベルで依存するから

---

普段使っているJavaにも型というものはあるが、この本で紹介されている型とは、ちょっと異なるようです。
型って、奥深い。。。

あと、発表の中にも出てきましたし本でもチラホラ出てくるMLというプログラミング言語ですが、私も
大学３年生の時に情報工学科の講義で受講しましたよー。科目名は確か「関数型プログラミング」という
名称だった気がする～。でも、もう10年以上も前になるのか・・・懐かしいです。
ちなみに当時の講義は↓の書籍が教科書として使用されました。

プログラミング言語ML (ASCII SOFTWARE SCIENCE Language) (1996/03) ジェフリー・D. ウルマン 商品詳細を見る

単位もちゃんと取得したけど、最後のほうの講義はけっこ難しくてついていけなかったんだよなぁ。。。
ただ関数型言語との出会いのインパクトは強烈でして、将来もう一度勉強するかもしれない、と思ってこの本、
大事にとっておいたんですよー。昨日押入れの段ボール箱を漁ったら、ちゃんと出てきました！



さて、次は@ruiccさんによる３章の発表で、章題目は「Untyped Arithmetic Expressions」です。

この本、3章からDefinitionやTheoremやProofやExcerciseがいっぱい出てきて、いきなり難しいです。。。
この章のポイントは、帰納法や導出木による証明を理解できるかどうかにかかっている気がします。

@ruiccさんの発表で難解な箇所については@none_tokaさんが補足を入れる、という感じで進んできました。
やっぱ有識者がいるってのはデカいですね。。。

発表の中で詳しく見たトコは、3.4節のSemantic Styleですかね。次の3種類があるとのことです。
■１．Operatinal semantics （操作的意味論）
■２．Denotational semantics （表示的意味論）
■３．Axiomatic semantics （公理的意味論）

@none_tokaさん曰く、これらの違いについてはWikiを読めばよいとのこと。

あと重要なポイントは、3.5.3節の導出木（derivation tree）は、下から上に向かって作るということです。
これ、私が大学時代の講義でハマッたポイントなんで、当時の苦い記憶を鮮明に思い出しましたよ。。。

自分は正直、3章でさえ、ついていくのに必死なレベルです。。。
うーむ、今回は3章までで時間になったので、次回参加するまでに復習するとしよう。
でも、たまには普段の仕事やプログラミングから離れて、こーいうアカデミックな勉強をするのも新鮮ですね。

次回の第2回は8/1に開催されるとのことで、ぜひ参加したいと思います。

最後に、会場を提供してくださったワークスアプリケーションズの関係者様、主催者様、ありがとうございました。
次回も楽しみにしてます。


・・・懇親会、出席しておけばよかったと悔やんでる。