POPL 2008メモ3日目

プログラム http://www.cs.ucsd.edu/popl/08/program.html

招待講演その3

話者：Cornellの分散コンピューティングLab出身。ポスドクのときのpart time jobからfull timeになった。

Jane Street Capital (proprietary trading company)でのOCaml利用事例。社員150人、うちOCamlプログラマ20人。OCamlは「窓際」ではなく中心。取り引きシステムからGUIまで、ほとんどのプログラムをOCamlで開発している。

技術的要求

  • Correctness: 金額がでかい:-)ので重要
    • C#で書いてみたらコードが冗長になってプログラム理解の妨げ
    • 動的機能もプログラム理解の障害(!)。例：オブジェクトのメソッド呼び出しが、実際にどのコードを呼び出すのかローカルに特定できない
  • Agility: 変化（特に、新しいideaや新興市場）への対応が中心なので重要
    • 十数年前(?)の株価暴落のとき、NASDAQの売買インターフェースが「人」で電話に出ないので取り引きが麻痺した
  • Performance: 開発でも運用でも速度が重要
    • 単純な最適化で十分な性能（予測可能性が重要）
      • JavaのHotSpotの性能挙動は予測困難
    • OCamlのGC速い(fast minor GC, incremental major GC, etc.)
      • 負荷が低いときにGCする
    • FFI（他言語ライブラリとのインターフェース）も悪くない

OCamlの改善可能性

  • Usability (Cf. Python)
    • 言語自体は遥かに良いが
  • ライブラリ(Cf. Java)

"We're hiring"

  • Javaで募集すると有象無象が来るが、OCamlで募集してもsmart peopleしか来ない:-)
  • "These languages are not academic toys"
  • "Functional languages give real values to people and companies"

[Q] Who can make decision to go to OCaml? [A] "It was sort of my fault.":-) Management cares correctness.

[Q] Hiring functional programmers (other than OCaml)? [A] We are hiring smart people.:-) Functional programmers are smart in general.

[Q] Any feature of OCaml you avoid? [A] Objects.:-) We use almost no objects. "Hard relationship" with polymorphic variants (sometimes great, but subtyping hard). Also, be aware of cost of higher-order functions and functors (cf. MLton).

[Q] Missing feature of OCaml? [A] Generic programming e.g. printing values (cf. Haskell's "deriving")

[Q] What was the worst mistake losing dollars? [A] Nothing big; "loop that sold something at near 0 dollar many times"

[Q] legacy codeからの当初移行？ [A] わりとスムーズ（3ヶ月）。ExcelやVBなどから、ちょっとずつ移植。

[Q] 3rd partyライブラリやコンパイラのバグ? [A] コアな部分には3rd partyライブラリはない。コンパイラのバグは問題になったことはない。

[Q] External tool to verify correctness? [A] 考えたが使ったことはない。

セッション9

関数型プログラミングのセッション

  • ある種のgenericな木traversal関数(zipper)を「代数的データ型（に対応する演算子）の微分(dissection)」で導出する話？（エキスパート:-)によると少し違ったらしい。）ラムダ計算(lambda-calculus)と微積分(calculus)の関係。OHPシート切り貼りで動かしてアニメーション（そのせいで時間不足になっていたが）。Message: "Types induce computational structure (for free)"
    • [Comment by Phil] Feedback what you think of pearls to me and the SC
  • GADT (generalized algebraic data types)のためのinitial algebra semantics。Descrete functor categoryで考えれば良いという話？　Left Kan extentionにより"Every GADT is equivalent to a nested type"（すみません、カテゴリー理論の知識がないのでわかりません…）
  • Toyota Technological Institute at Chicago（トヨタの計算機科学研究所？）。ちょっとずつ変わる入力に対する出力のmemoization + 差分計算。セル生成・初期化mod v、書き込みwrite l v、読み出しread l as x in e。書き込みで「影響を受けた」部分だけ自動再計算。そのために計算の"trace"を記憶して"change propagation"。健全性（等価性）証明はstep-indexed (and untyped!) logical relationsによる(with bijection on stores)。効率的実装についても。計算量評価。

セッション10

プログラミング言語セキュリティのセッション（３番目以外。３番目は「余ったから入れた」？）

  • Security type system（high-security, low-securiyを型と考える）を暗号で実装したときの、計算量理論的な安全性(computational non-interference)の証明。（プログラミング言語的には言語や攻撃モデルが「やや不自然」だが、暗号理論的要求により設計されている？）　CCA2などの暗号理論的仮定も同じ言語で表すことにより、確率的等価な変換の連続により安全性証明が可能（言語の安全性を暗号の安全性に還元）。
  • 同じような話だが、ソース言語に鍵生成・暗号化・復号があり、security typeはない。

案の定ここで退室する人多数。３番目の話者が多少可哀想？

  • Javaのinstanceofの実装。動的クラス追加があっても時間・計算効率が良い実装方式を考えた。（すみません、自分も他の論文を読んでいたので中身は聞いていません）
    • 時間10分ぐらい余るが質問出ない(!)のでsession chairの吉田さんや本田さんが一般的質問（「他にfuture workは？」「その空間計算量は現実的にどれぐらい重要か」等）
    • 個人的印象：かなり枯れている＆応用範囲の狭いテーマで、既存研究(DST)との差が小さいような…。メモリ消費量が減るといっても、元から問題にならないレベルでは？（本田さんの質問と同じ話だが）

セッション11

Curry-Howard isomorphismやhigher-order abstract syntax（対象言語の変数束縛をメタ言語のλで表現する手法）のセッション？　これも案の定人少ない…

  • わからない＆聞いていませんでした。(_ _) 証明論関係。（タイトルにも関わらず）実はHOASではなく"abstract higher-order syntax"の話？
  • HOASで変数の名前を取り出して使う話？（これもよくわからない…）　Key idea: contextual modality: exp[Ψ]。Add (Nat 0) (Nat x)はexp[x : Nat]型。Ψのおかげでnominal approachでのfresh nameがescapeしない。例：特定の変数の出現回数を数える、環境渡しインタプリタなど。
  • Call-by-valueのdelimited continuationに対応する計算体系をcall-by-nameにしてみました、という話。スライドの字小さすぎ。メイン部分で話者交代しようとしたが、すでに時間不足でほとんど発表できず(!)。
    • [Q by me] 1 + reset 2が3にならないのでは？ [A] そもそもreset 2とか書けない(!?)。"Delimited continuation"の意味が「普通(Danvy-Filinski)じゃない」らしい。shiftはあるし、continuationのcomposeもできるが、resetがcontinuation applicationの直前(?)に限定されている（よくわからないので聞き間違いか？）。

セッション12

最終セッション。「やわらかい型システム」のセッション？

  • "Typed Scheme"。Schemeなど静的型情報のない「スクリプト言語」のプログラムはメンテ困難。そこで「ちょっとずつ」型をつけることにする。型なしコードから型つきコードを呼び出すとき（あるいは逆）はcontractで実行時検査。型つけ規則が実行時型情報による場合分け（integer?とか）にも対応。Future work: Pythonとか、オブジェクトがあり、逆にcontractやモジュールはない。
    • [Q by me] set!とかset-car!とかどうするの？ [A] set!は事前に解析して「場合分け型つけ」の対象から除外。[A by Felleisen] set-car!とset-cdr!はPLT Schemeではもう禁止（会場拍手）
  • Boomerang（ブーメラン）。PennのHarmonyプロジェクトの一貫。異なる文字列データベース間の双方向変換（一方への変更を他方に反映）を記述するための言語と定式化。正規表現パターンマッチングの一種で記述。Kleene star（リスト）を単純に双方向変換すると「位置」だけがキーになってしまうので、"key"プリミティブでキーを、< >で位置が移動可能な要素を明示できる。BibTeXとかゲノムとかの例。
    • [Q] Keyが変わったら？ [A] 現バージョンではマッチが取れなくなる（ので変更が伝搬しない）。スキーマによる「似ていたらマッチング」を考え中。
  • PADSの話。正規表現型つき文字列データ操作言語。データからパターンを機械学習をして、その「データベース」の「スキーマ」（正規表現型）を推論。トークンの区切り文字は指定しないといけないらしい。出現回数のヒストグラムで分類(structs, arrays, unions)、rough decriptionを生成して、rewritingによりrefine (details in paper)。Training time/sizeはほぼ線形時間。Training accuracy（自動学習したパターンでparseした成功確率）は場合によるが、5%〜60%の学習で90%以上の正確さ（半数以上は5%でOK）。いろいろなlogやnetstat -an, ls -l等の例。

以上。多分、後半ほど適当です（最初から適当ですが）。