Blog

Tech

参加レポート

2016.9.25

ICFP及び関連イベント参加レポート – ICFP 3日目 –

κeenです。ICFPに参加するために奈良に来ています。これはICFP本体の3日目のレポートです。会場付近は鹿のアレで臭いです。

A Functional Programmer’s Guide to Homotopy Type Theory

Talker: Dan Licata

3日目のキーノートはHoTT本の著者のダニエルさんから、関数型プログラマ向けのHoTTの紹介。

ダニエルさんの個人ページからスライドにアクセス出来ます。

私が説明するよりスライドを見た方が分かりやすいと思うのでそちらに譲ります。ゆっくりしたペースで聞き取りやすく喋っていたので非英語ネイティブには非常に有難い講演でした。

因みにHoTTに詳しそうな人を捕まえてHoTTって何が嬉しいの？って聞いてみたら「色々な見方があって一概には言えない」とのことでした。奥ゆかしいですね。

Ghostbuster: A Tool for Simplifying and Converting GADTs

Talker: Trevor L. McDonell, Timothy A. K. Zakian, Matteo Cimini, Ryan R. Newton
Paper: Ghostbuster: a tool for simplifying and converting GADTs

型付きアセンブラのaccelerateをハックしようとした時の経験を導入にし、GADTを使って強く型を付けたプログラムは安全かもしれないけどそこにさらに機能を加えるのが難しくなるということから幽霊型を消すライブラリを作ったというお話。

Vec n a のような型インデックス付きデータ型からシンプルな List a を得るには手で作るかevalを使うかが必要になりますが、どちらも現実的ではないです。

(恐らく)GHCの拡張として実装されたGhostbusterを使うと裏で生成してくれるそうです。

{--# Ghostbuster: synthesize n #--}
data Vec n a where
  VNil :: Vec Zero a
  VCons :: a -> Vec n a -> Vec (Succ n) a

data Vec' a where
  VNil' :: Vec  a
  VCons' :: a -> Vec a -> Vec a

{--# Ghostbuster: synthesize n #--}

data Vec n a where

VNil :: Vec Zero a

VCons :: a -> Vec n a -> Vec (Succ n) a

data Vec' a where

VNil' :: Vec a

VCons' :: a -> Vec a -> Vec a

Indexed Codata Types

Talker: David Thibodeau, Andrew Cave, Brigitte Pientka Paper: Indexed codata types

Datatypeにtype index付けたら便利なんだからCodatatypeにもIndex付けたら便利だろという内容。

うん、確かに気持は分かるんだがあまり使い所が分からない

Disjoint Intersection Types

Talker: Bruno C. d. S. Oliveira, Zhiyuan Shi, João Alpuim
Paper: Disjoint intersection types

let x = 1 ,, True :: Int & Bool

1	let x = 1 ,, True :: Int & Bool

のように項レベルでの交差のある体系を考えた時に

let x = 1 ,, 2 :: Int & Int

1	let x = 1 ,, 2 :: Int & Int

のように両方とも同じ型だったら困るよね、ということから困らない範囲に限定しようというのがこの論文。非交差なものに限定すれば出来るよ、とのこと。まあ、簡単に言ってますが関数のsubtypeとかコヒーレンシーの問題とかTop型が入った時にどうなるかとかの問題もあります。

「出来たところで何が嬉しいの？」とか、項レベル交差はタプルの射影をimplicitにやっているだけなので「型付き言語使ってるんだから手で射影書いた方が綺麗ない？」などと(外野で)言われてました。

一応好意的に解釈すると項レベルの交差は

let x = {foo: 1} ,, {bar: 2}

1	let x = {foo: 1} ,, {bar: 2}

のようにレコードのマージにも使えたりするのでそういう所に持って行きたいのかなぁとか。

github.com/jalpuim/disjoint-intersection-types でソースコードを公開しているそうです。

Set-Theoretic Types for Polymorphic Variants

Talker: Giuseppe Castagna, Tommaso Petrucciani, Kim Nguyễn Paper: Set-theoretic types for polymorphic variants

OCamlの多相バリアントがユニフィケーションベースなので

let f = function 'Apple -> 'Pomme
               | 'Cherry -> 'Cerise
               | x       -> x
(* -> {'Aple, 'Cherry, 'Pomme, 'Cerise, x} -> {'Aple, 'Cherry, 'Pomme, 'Cerise, x}* )

let f = function 'Apple -> 'Pomme

| 'Cherry -> 'Cerise

| x -> x

(* -> {'Aple, 'Cherry, 'Pomme, 'Cerise, x} -> {'Aple, 'Cherry, 'Pomme, 'Cerise, x}* )

のように正確ではない型に推論されてしまって嬉しくないよねーって話からintersectionとunionを入れて上手くやったよ！という内容。

しかし東北大の大堀先生から「私の20年前の論文との差分は？」とか「ちゃんと先行研究との比較した方がいいよ」とかあと他にも数名からボコボコにされてました。

Hierarchical Memory Management for Parallel Programs

Talker: Ram Raghunathan, Stefan K. Muller, Umut Acar, Guy Blelloch
Paper: Hierarchical memory management for parallel programs

関数型な言語だったら(特に分割統治で)コールグラフが木構造になるけど部分木同士では互いにメモリを干渉し合わないから普通のGCより上手くメモリ管理出来るよねってお話。

ということでλ^HPなる体系を作ってなんかごにょごにょして良い感じになった、と（語彙力）。

あ、なんかfork-joinプールとの関係にも言及してました。

Allocation Characterizes Polyvariance: A Unified Methodology for Polyvariant Control-Flow Analysis

Talker: Thomas Gilray, Michael D. Adams, Matthew Might
Paper: Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis

これまた抽象機械界隈の事情を知らないのでよく分からないのですがpolyvarianceというのが静的解析の1つの指標になっているらしいです（同じ関数が違う状況で呼ばれたらその分だけ解析する。「状況」というのが引数だったりオジェクトだったりでデザインの違いが出る）。もちろん、精密にやろうと思えばいくらでも出来るのですがそうすると今度は複雑性が上がるトレードオフ関係にあるので様々な手法があるようです。

これらを統一的に見るために抽象抽象機械というのを考えて、storeを明示的に渡していくstore-passingスタイルでモデリングすることでなんか出来たというもののよう。

bitbucket ucombinator/p4f-prototype でソースを公開しているらしいです。

A Fully Concurrent Garbage Collector for Functional Programs on Multicore Processors

Talker: Katsuhiro Ueno, Atsushi Ohori
Paper: A fully concurrent garbage collector for functional programs on multicore processors

「ラムダは出てきません」と前置きしてました。実装寄りの論文です。

マルチコア環境だと勿論マルチコア対応したいけど関数型に適切なGCアルゴリズム作ったよ、というお話。

ベースになっているのはBitMapでオブジェクトを管理するUeno-Ohori-Otomo Collectorで、湯浅先生のSnapshotの概念を取り入れて並行対応を実現しているようです。

どうSnapshotを取るかが問題になりますが、各スレッドにメッセージを出して自身の管理するroot setをマークしてもらう、メッセージを出してから全てのスレッドがroot setをマークするまでのあいだに変更されたオブジェクトはWrite Barrierで管理する、という方針のよう。GC中だけWrite Barrierをonにするという概念とそもそも関数型だったらあんまりWriteしないだろ、って話は非常に気に入りました。

現在のSML#に入った実装は残りの部分がSequencialなのであまりスレッド数に対してスケールしないようですがそれでもStop the Worlが劇的に短くなっているようです。素晴しいですね。

因みに大堀先生と少し話す機会があったのですが、これで大きな機能が入り終わったのでSML#の最適化にも取り組んでいきたいとのことでした。期待。

Talking Bananas: Structural Recursion for Session Types

Talker: Sam Lindley, J. Garrett Morris
Paper: Talking bananas: structural recursion for session types

セッション型に構造的再帰型を付けたいというお話。記号が竹内外史の線型論理の本とかと違うので苦しいですが頑張って読みましょう。

The Best of Both Worlds: Linear Functional Programming without Compromise

Talker: J. Garrett Morris
Paper: The best of both worlds: linear functional programming without compromise

先程に続いてJ. Garrett Morrisさんが発表します。「私がこの世で好きなものはλとケーキだ」という導入からλのようになんどでも値を使い回せる計算とケーキのように消費してしまう計算を組み合わせた言語を作ったというお話。まあ、単純型と線型型を組み合わせたものって中々ないですね。

言語はquillというらしいです。

ちょっと気になったのは関数のオーバーローディング。Rustだったら引数を所有しているかしていないかで関数を作り分ける必要がありますが、quillは自動でオーバーロードしてくれるよう。すごい。

Context-Free Session Types

Talker: Peter Thiemann, Vasco Thudichum Vasconcelos
Paper: Context-free session types

Session Typeはオートマトンをってスレッド間のやりとりを型を使って表現する手段ですが、オートマトンだとω-正規言語までしか表現出来ないので文脈自由文法まで広げましょうというお話。

言うには簡単ですが実際に形式化して云々とやるには一手間必要だったようです。

Combining Effects and Coeffects via Grading

Talker: Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu
Paper: Combining effects and coeffects via grading

Effectがコンテキストへの変更、Coeffectがコンテキストへの要求。これらを組み合わせたいというのがモチベーション。例えばEffectで例外を、Coeffectでファイルのリソースを要求しているとして、例外が起きたらリソースの要求を取り止めたい、など。

それをGradeを使って実現したという内容。

String Diagrams for Free Monads (Functional Pearl)

Talker: Maciej Piróg, Nicolas Wu
Paper: String diagrams for free monads (functional pearl)

String図を使ったらなんかヤバそうな証明が簡単になったよ、便利！

最後に

ICFP 2017はオックスフォードであるそうです。

これでICFP本体は終わりですがまだまだ併設ワークショップは続きます。

Author

admin