FLOPS 2014 は二年に一回、日本で開催される関数型および論理型プログラミングに関する国際会議です。今年は6/4-6の日程で石川県金沢市で開催されました。
弊社はアドテクの会社で開発言語もScalaだったりと、まぁほとんど会社の業務と関係無いのだけど、やはりせっかく日本で関数型言語の国際会議があるなら是非聞きに行かないとね、ということで聞きに行きました。
以下、感想などです。各発表内容に関しては、プログラムのページから発表スライドを見る事ができるはず。
第１日目
★ "Liquid Types For Haskell" 招待講演
今回のFLOPSで一番興味を持っていたのがこの話です。
Liquid = Logically Qualified Data の略、のつもりらしく、liquid type というのは、
{v: Int | v >= 0} の様に、論理式で修飾された型のことです。Coq などの依存型を用いた定理証明系でもこのような述語を伴った型を使ってプログラミングを出来るところは同じなのですが、liquid type は述語を決定可能なPresburger算術の範囲に限定し、SMTソルバーを用いて自動証明をさせようというところが大きく違います。まぁCoqの証明を書くのは大変だし、開発の現場で必要とされる検証課題はほぼPresburger算術で充分なのだとしたら、自動証明の方が普及までの敷居が低いのは自明。LiquidHaskell がどんなものか試したい人はオンラインでどんなものか試すことが出来ます。
liquid type の型定義は、
{-@ type Even = {v:Int | v mod 2 = 0} @-} みたいにHaskell のコメントとして、実際のHaskellのコードに註釈します。すると double xs = [x + x | x <- code="" xs=""> のようなHaskellの実装について、{-@ double :: [Nat] -> [Even] @-} の様な仕様を満たすことを自動証明してくれる、というのを試せます。
個人的には Coq で証明を書くの好きなんだけど、やはり前の会社(SIer)や今の会社で仕事をしてみた印象としては、自動証明器も必要なのかなぁとも思います。ならば Why3 とか使って開発すれば良いかなとも思うけど、Haskell みたいに既にメジャーな言語でこの手のツールが使えるというのは、やはり強みなのかなぁと思います。他の発表は簡単に（というか専門家じゃないから解説なんか出来ない）。詳しくは、proceedings読んで下さい。
★ "PrologCheck - property-based testing in Prolog"
オブジェクト指向言語界隈では具体的なテストケースに対してユニットテストをすることが多い様ですが、関数型言語ではランダムにテストデータを生成して仕様（＝満たすべき性質）を満たすことを確認するようなproperty-baseのテストツールが標準的です。（ScalaでもScalaCheckというのが有りますが、開発現場ではあまり使われてないみたい。勿体ない話です。）
で、Prolog版のを作った、という話（だと思う）。
★ "Generating Constrained Random Data with Uniform Distribution"
で、その手の XXX Check系のテストツールには、「もし入力データが◯◯という性質を満たすなら△△」みたいなのをテスト出来るのですが、◯◯という条件を満たすランダム入力データを作るのはなかなか面倒だったりします。その辺を工夫したよ、という話（だと思う）。
★ "Guided Type Debugging"
関数型言語のエラーメッセージは、（C++ほどではないと思ってはいますが）Javaとかに比べると判りにくいところがあります。その原因の一つの、型の不整合の時のエラーのデバッグを容易にしようとする工夫（だと思う）。
★ "Using big-step and small-step semantics in Maude to perform declarative debugging"
Maude (という項書き換え系言語)の上に、何か言語の big-step あるいは small-step semantics を定義して実行とかデバッグとか出来るフレームワークを作った、という研究の様に思えた。確かに small-step semantics とか Maude の上に定義すると便利そうに思えますね。
★ "Faustine: a Vector Faust Interpreter Test Bed for Multimedia Signal Processing - System Description -"
Faust というのは信号処理用のDSLらしいのですが、これを使ったギターアプリ(タブレット上で動くギター風に演奏出来るアプリ)の動画デモが。こんな研究してる人もいるんだなー、と思いました。
★ "The Design and Implementation of BER MetaOCaml: System Description"
★ "On Cross-Stage Persistence in Multi-Stage Programming"
MetaOCaml というのは OCaml を拡張して型安全 eval を使える様にしたようなものなのですが、それに関する発表が２件。
第２日目
★ "Programming Language Methodologies for Systems Verification" 招待講演
L4 microkernel を作ってる研究機関での形式手法仕様に関する報告。当初OS班と形式手法班がIsabelle/HOLを使おうとして失敗し、Haskellを両者の共通言語として選択したら成功して、両者の共通言語としてのHaskellからIsabellあるいはC++を作る様になった（しかしその後、各班がHaskellをメンテしなくなって云々）みたいな報告。
この手の話聞くと、OS班とはいえ研究者の方々でも、やはり Isabelle などの形式手法（定理証明系）とかで仕様記述するの嫌なのか、と思ってしまいますね。。。IsabelleはZとかほど抽象的ではないと思うのだけれどなぁ。あと、線形型は勉強した方が良さそうだなと思った。
★ "Lightweight higher-kinded polymorphism"
OCamlには無いhigher-kinded polymorphismをdefunctionalizationすることで実現したよ、という話。
★ "Generic Programming with Multiple Parameters"
HaskellのGeneric programmingでパラメータを複数個使える様に、という話。うーむ、Haskellのgeneric programmingの話、ちゃんと復習しないとなー。
★ "Type-Based Amortized Resource Analysis with Integers and Arrays"
計算量というリソースを型として表現するという話。こういうことも出来るのか、と。
★ "Linear Sized Types in the Calculus of Constructions"
CoqのInductionの停止性、CoInductionのproductivityの判定の為に、それらを表現出来るような型を、という話。
★ "Dynamic Programming via Thinning and Incrementalization"
ナップザック問題を例にとってDPの解法アルゴリズムを、融合変換とかアルゴリズム変換とかを使ってアルゴリズムを最適化する話。この手の話に興味がある人は、"semiring fusion" とか "第三準同型定理" とかのキーワードでググると良いと知人より教わりました。勉強すること多いなー。
★ "POSIX Regular Expression Parsing with Derivatives"
微分を用いて正規表現を扱う話は知っていたのですが、POSIX準拠のはずの各種正規表現ライブラリが、どこで部分文字列をマッチすべきかについて正しく無い答えを返す、という話は知りませんでした。ちゃんとPOSIX仕様に基づいて、部分マッチ箇所を計算するアルゴリズムの話です。Proceedingsにはプレゼンでは端折ってあった箇所が書かれてて面白そうなので、あとでちゃんと復習しよう。
★ "Semantics for Prolog with Cut - Revisited"
Cut有りのPrologのsemanticsをCoqでやってる、という話。すみません、Prolog良く解らないので、どの辺が重要なポイントなのか判りませんでした。
★ バンケット
コース＋追加で寿司、天ぷら、日本酒という立派なバンケットでした。線形論理の話とか面白い話を聞けました。
第３日目
★ "Relating Computational Effects by TT-Lifting" 招待講演
計算(computation)を扱う理論的枠組みとしてdenotational semanticsというのがあるのですが、圏論を使って色々統一的に議論出来るよという話で、最初は判る話だったんですが、後半はさすがに振り落とされました。が、こういう話聞くと、また圏論勉強しよう、という気分になりますね。
★ "A New Formalization of Subtyping to Match Subclasses to Subtypes"
継承とジェネリクスと両方ある Java とか Scala みたいな言語だと、型宣言の際に共変反変の両方の制約を満たす為に(例えばScalaなら)
sealed abstract class List[+A] extends ... { def ::[B >: A] (x: B): List[B] = ... } みたいなイディオムを使わざるを得ないとか色々不便なところもあるのですが、この論文は新しい subtyping の定式化をしてみたよという話。OO言語関係に近い話題はこの一件だけでした。Scala などに興味がある人は ECOOP とか聞きに行くべきなんですかね。。。★ "Type Soundness and Race Freedom for Mezzo"
Mezzo というのはML風の言語なんですが、線形型を用いることでマルチスレッドプログラミングでロック取得の必要性などをコンパイル時にチェック出来る様にした言語で、言語の正しさ(型検査が通ればデータ競合が起きない事)を Coq で証明した、という話。Java とか Scala とかだとプログラマが正しくロックを取ってる事を保証しなくてはいけないので、Mezzo のこういう機能は素晴らしいと思います。
★ "Proving Correctness of Compilers using Structured Graphs"
木構造ではなく(非循環)グラフを用いてコンパイラを改善するみたいな話で、グラフを用いてコンパイル＆実行するのと、木も用いてとが等価だと言う証明の話（だと思う）。
★ "Constraint Logic Programming for Hedges: a Semantic Reconstruction"
すみません、これは良く判りませんでした。semantics と solver のアルゴリズムについて話してたと思うのだが。
★ "How many numbers contains a lambda-term?"
λ式でk-tupleとかを作った場合、λ式の型を決めると、そこに含む事の出来る自然数の個数には上限がある、という話（だと思う）。これも難しくて判りませんでした。
★ "AC-KBO Revisited"
項書き換え系にはクヌース・ベンディックス完備化アルゴリズムという完備化アルゴリズムがありますが、結合則
x+(y+z) = (x+y)+z や交換則 x+y=y+x のような規則を満たす演算子に関する場合にどうするかという話。Steinbach という人の論文が間違っているという論文があったけど実はそれは正しくてみたいな話とか、順序付けがNP-hardなことはこうやってSATに変換してとか、（詳細は理解出来ない）門外漢にも楽しめる発表でした。★ "Well-structured pushdown system: Case of Dense Timed Pushdown Automata"
Timed Pushdown Automata の話でした。これも基礎知識が無くどういう話なのか良く判りませんでした。
終わりに
社外勉強会の効能として、「今まで知らなかった話題に触れられる」「すごい人たちのやってるすごいことを知る」「もっと勉強しようというやる気を貰ってくる」といったことを主張する人は多いです。私もその意見に賛成します。
だとしたら、学会とか国際会議に行けば、第一線の研究者がやっている最先端の話題を知る事が出来ます。
そして、例えばHaskellとかOCamlなどは、言語の開発者がこういう学会で発表した事を言語の新機能として追加したりします。学会で話されている事は自分が使う機能と無関係な難しい話ばかり、という訳ではありません。
勿論、聞いても分からない話も一杯有りますし、周りは見知らぬ研究者ばかりで話す相手も内容も無い、などなどというところはありますが、まぁその辺は我慢するとして。判らなかった内容とかは、各種勉強会とかに行って論文コピー片手に詳しそうな人に質問するとか方法はありますし。
2016年のFLOPSは高知で春に開催だそうです。また PPL のような日本の学会とかなら敷居が低く感じるかと思います。
社外勉強会に行く次のステップとして、学会とか国際会議を聞きに行くのを是非お勧めします。
No comments:
Post a Comment