κeenです。ICFPに参加するために奈良に来てます。会場は奈良公園の中にある国際フォーラムで、鹿に囲まれています。

18日はICFPに併設されているワークショップの日で、Workshop on Type-Driven Development(TyDe)、Scheme and Functional Programming Workshop(Scheme)、 Workshop on Higher Order Programming with Effects(HOLE)、 Programming Languages Mentoring Workshop(PLMW)が開催されています。セッションの合間の休憩で自由に動いて良い形式だったのでどのワークショップとは決めずに興味のあるセッションを聞いて回りました。セッションの選び方に好みが出るところですね。

Opening

Workshop: TyDe

今回が初めての開催とのことでした。

APLicative Programming with Naperian Functors

Workshop: TyDe
Talk: Jeremy Gibbons
Paper: APLicative Programming with Naperian Functors
Slide: APLicative Programming with Naperian Functors

APLというプログラミング言語、あるいはその後継のJという言語では関数 square がただのスカラ値にも、ベクトルにも、行列にも、テンソルにも作用出来ます。 また、足し算のような二項演算も同じように振舞える他、スカラとベクトル、ベクトルと行列での演算が可能です。その時は小さい方を繰り返して大きい方に合わせますが、ベースの形(shape)が合ってないといけません。

このような機能をHaskellで実現したい、しかも形が合っていることに関しても静的に検査したいというモチベーションの下、実装を進めて完成したという話でした。

さらに、行列のflatな実装も型安全に出来たよというのもありました。

特に詳しい説明もないままHaskellのコードを羅列してどんどん進んでいくので「これがICFPか…」ってなりました。

Choose Your Own Derivative

Workshop: TyDe
Talk: Jennifer Paykin, Antal Spector-Zabusky, Kenneth Foner
Paper: choose Your Own Derivative – psf_choose_2016.pdf
Code: antalsz/choose-your-own-derivative: Code for the submitted TyDe ’16 extended abstract “choose Your Own Derivative” (in progress)

関数 choose の型にまつわる話です。例えば chooseList を考えてみましょう。

だとどの要素が選ばれたのか分かりづらいので

のように選ばれた要素の前後もリストのまま返してみます。さて、 ([IO a], a, [IO a]) をコンテキストと考えてみましょう。

このコンテキストの概念を他のデータ型にも適用してみましょう。Eitherだとシンプルでこうなりますね。

これは choosePair なんかになると少し複雑で、

のようになります。

これ、何かに似てませんか？そう、微分です。

一般に、

の形をしているようです。Pairの時は丁度積の微分公式になっていますし、Eitherは和微分公式になっています。

さらにこれはIOに限らずジェネレータやパーサでも同じようなことが成り立つよね、面白いよね、という内容でした。

A Scheme concurrency library

Workshop: Scheme
Talker: Takashi Kato

Scheme処理系Saggitariusの作者のTakashi Katoさんによる自作Scheme並行ライブラリの紹介でした。 SRFIの提供する並行APIは低レベルで使いづらく、デッドロックなどの危険性もあるので改善したいという背景があります。 そこで並行に使えるキューやスレッドプール、フューチャーなどを実装した、という内容でした。

会場からはGuileのライブラリとの違いは？との質問が出て、こっちはポータブルだ、などのやりとりがありました。

Nash: a tracing JIT for Extension Language

Workshop: Scheme
Talker: Atsuro Hoshino

Scheme処理系のGuileはバイトコードインタプリタとして実装されていますが、そのバイトコードをJITコンパイルして爆速で動かす開発をしているAtsuro Hoshinoさんからの発表でした。 最初のマンデルブロ集合の描画のデモでは素のGuileが19秒ほど掛かっていたものをJIT付きだと0.4秒ほどで終えていました。

その後の発表はGuileの実行モデルを説明したあと、JITがどのように動いているかなど詳しく説明していました。

会場からは「スレッド使って並列に動かしたらどうなるの」などのイジワルな質問も飛んでました。 また、unboxedなfloatなども扱っているのでGCとの兼ね合いは？という質問があり、発表者が戸惑っていましたが別の参加者からBoehm GCはConservativeだから問題ないよ、などの突っ込みもありました。

Ghosts in the machine

Workshop: Scheme
Talker: Daniel Szmulewicz

Clojureの system の作者のDanielさんから、インタラクティブシステムについてでした。 心理学や認知脳科学の話を交えつつ、SmalltalkやForthなどの「環境」、Lispの歴代のIDEの話をし、ClojureのREPLについての話がありました。 他のLispならば環境の再起動で済みますが、Clojureについては起動が重いので再起動はせずに名前空間のリロードなどで代用します。 その時に捕捉された古い変数などが残ってしまうために問題になるなどの指摘をしていました。

Danielさんは語りが熱く、唯一（？）時間一杯まで使ってしまって途中で止められていました。

R7RS update

Workshop: Scheme
Talker: Alex Shinn

R7RS-smallの委員会の座長のAlexからR7RS-largeの進捗についての発表がありました。 スライドをロクに使わず、ぼそぼそと喋るスタイルだったので聞き取れずに後でR7RS-largeを実装しているKatoさんから話をききました。

R7RSはdocketという単位に分かれていて、そのうちdata structuresのred docketが終了して、numbersのorange docketが作業中だそうです。 会場からはいつR7RS-largeが出るの？と質問が飛んで、「頑張ってるよ（意訳）」との返答がありました。

GNU Guix: The Functional GNU/Linux Distro That’s a Scheme Library

Workshop: Scheme
Talker: Ludovic Courtès

INRIAのLudovicさんから、Guix(ギークス)というパッケージマネージャについての説明がありました。 若いプロジェクトであるものの40名ほどのコントリビュータがいて活発に開発されているようです。

特徴としては関数型であること。デモを交えながら発表していました。 インストールやremoveなどを1トランザクションで実行出来、さらにトランザクション毎にジェネレーションが付きます。 そして任意のジェネレーションにrollback/rollforwardが出来ます。

さらに、例えばGuileが欲しいと思ったら必要なパッケージを入れた隔離環境(Linux Container)も作れたりします。

発表ではさらにビルドシステムについてやSchemeライブラリとしての使い方などの説明がありました。 NixOSへの言及や比較もしつつで、充実した内容でした。

ALGEBRAIC EFFECTS FOR FUNCTIONAL PROGRAMMING

Workshop: HOLE
Talker: Daan Leijen

MSRのDaanさんからAlgebraic Effectについて。 Algebraic Effectは圏論が基礎にあるシステムで、操作の扱いに長けています。 例えば例外や繰り返し、非同期など。

そこで、kokaというJSへとコンパイルされる言語を紹介しています。 この言語は全ての関数が入力、出力、そしてEffect型を持っています。 Effect型についてはraw polymorphismを入れているようです。 Effect型にはrow polymorphismが自然なんだそうです。

「詳しいことは [koka book daan] でググって」とのことです。

このkokaという言語、型の修飾子にtotalyとかexc とかdiv, consoleなどがあり、なるほどEffectという感じでした。

私もよく分かっていないのですがEffectから自由代数を作ってそこから自由モナドにもっていってそこでセマンティクスを与えている（？）ようです。

デモではgetstrを呼ぶ関数をhandlerで囲って、そのgetstrの返り値をコードで与えてやることで標準入力からの入力じゃない値で動く、などがありました。あとはもちろんexceptionのraiseとかでも同じようなことが出来ます。

Effectの実装には限定継続か自由モナド変換が必要ですが、kokaの場合はType Directed Selective CPSを使っているそうです。

Administrative normal form, continued: Sharing control in direct style

Workshop: HOLE
Talker: Luke Maurer, Paul Downen, Zena M. Ariola, Simon Peyton Jones

CPSとANFの話です。 コンパイラの中間言語に使う時に、ANFは元のコードに比較的似ているので扱いやすい反面、一部の最適化が出来ないなど不便な点があります。 一方CPSだと最適化はやりやすいのですが、関数の形が完全に変わってしまうのでつらい部分もあります。

そこでANFを少し拡張していいとこどりしようという話です。

例えばANFだと困る例としてcase of case transformationがあります。

はすぐに消費されるのにJustかNothingを生成してしまい、非効率です。

ということで “Think in CSP; work in ANF” を目指します。それがContificationです。 この辺の話はHaskell DayのSimon Peyton Jonesさんの話と被るので割愛します。

Parameterized Extensible Effects and SessionTypes

Workshop: TyDe
Talker: Oleg Kiselyov
Paper: Parameterized Extensible Effects and Session Types (Extended Abstract)

Extensible Typestate をやっていくと最終的にSession Typeになるよねという話です。 typestateとは、（あまり素直でない）Effectの拡張です。適用可能な操作が型だけではなくて状態にも依存します。

モチベーションは、例えば以下のようなコードを考えます。

これは2値を返すためだけに一旦タプルを作ってすぐに壊しています。嬉しくないですね。 これを避けようと思うと

のように今度はSomeを使わないといけなくてこれもまた嬉しくありません。理想的には

のように手続的な書き方が出来ると嬉しいです。

それを構築しようというのが今回の主旨です。 最初のアプローチから試行錯誤していく方式で、 PolyStateMonadを使って変数を型レベルに話からExtensible EffectとかVariable State Effectとかを色々を使いつつ Parameterized Extensible Effectsに辿りついてました。最終的には型パラメータが6つくらいになっててお、おうといった感じでした。

An Agda formalisation of the transitive closure of block matrices

Workshop: TyDe
Talker: Patrik Jansson, Adam Sandberg Eriksson
Paper: An Agda Formalisation of the Transitive Closure of Block Matrices (Extended Abstract)
Code: DSLsofMath/FLABloM: Functional Linear Algebra with Block Matrices

使いやすくてかつ証明しやすいBlocked Matricesとその推移閉包ををAgdaで定式化しましたというお話。

最初に行列のShapeを

で定義したらRawとColをを定義出来るので行列が出来ます。 さらに行列の推移閉包も定義して、定式化しました。

最後に

初日のワークショップが終わりました。 他の参加者に話をきくと、HOLEではScalaのソースコードを変えずに型を変えることでEffectを実現する話だとかOCamlにEffectの型をつけて例外やその他をごちゃまぜでパターンマッチする話だとかもあったそうです。 因みにScalaの話はコード例は「誰も分からないScalaではなくて全員が分かるHaskell」だったそうです。ICFPらしいですね。

さて、次の日からICFP本体が始まります。