Blog

2016.10.2

ICFP及び関連イベント参加レポート – 併設ワークショップ2日目 –

κeenです。そろそろ奈良市内循環バスにも馴れてきました。シカにはもう飽きたので駱駝の画像でも。

これはICFP併設ワークショップ2日目のレポートです。ちょっと数え方がよく分からないのですがICFP本体が19-21日にあって、併設ワークショップが18, 22, 23, 24日にあったのですが、これは22日のものです。

From Identification of Parallelizability to Derivation of Parallelizable Codes

Workshop: FHPC
Talker: Akimasa Morihata
Paper: From identification of parallelizability to derivation of parallelizable codes

並列プログラムは書くのが難しいからフレームワークで抽象化して、ユーザには詳細を見せないであげる必要があるということから並列計算に向いた体系を構築中というお話。

例えばリストの長さを取るのは並列化が難しそうですが、pointer splicingというテクニックを使うと分割して作業が出来るのでRandom Mateを使ってあげれば並列化出来そうです。

o-[]-[]-[]-[]-[]-[]-[]

o-[]-2-[]-2-[]-2-[]

o-3-[]-4-[]

o-7-[]

o-[]-[]-[]-[]-[]-[]-[]

o-[]-2-[]-2-[]-2-[]

o-3-[]-4-[]

o-7-[]

理想的には「何も考えなくてもフレームワークを使えば並列化してくれる」ですが、現実的にはちゃんと考えてちゃんと並列化しないとダメでしょう。

ということで構築中なのが PTypeという体系だそうです。型が付いたプログラムは並列化出来るという特徴を持ちます。

なんか分割統治みたいにシーケンスの真ん中で、引数と本体同時に計算可能な特殊なλ式で切ってあげると並列化出来そうだよねーみたいなやつでした。あとADTはチャーチエンコーディングする。

WebAssembly: high speed at low cost for everyone

Workshop: ML
Talker: Andreas Rossberg
PrePrint: WebAssembly: high speed at low cost for everyone

GoogleのAndreasさんからWebAssemblyについて。

WebAssemblyは主要なブラウザベンダが集まってオープンに作られている仕様で、ブラウザ上でネイティブコードと同等の速度を出せるバイナリが欲しいという需要から作られています。（筆者注: 現状、まだasm.jsに比べてバイナリになった分ロードが速い程度で実行速度はそこまで変わらなかったと重います。）

目的としてはJavaScript以外の言語を動かしたいだとかJavaScriptで出来ない機能を実現したいだとかハイパフォーマンス（ネイティブコードの20%以内）だとかasm.jsや(P)NaClの置き換えだとを狙っているそう。

因みにwasmはプログラミング言語でもなければブラウザ上のVMでもないです。さらに動作環境はWebに限られたものではありません（！）

ゴールはセマンティクス的には

言語非依存
ハードウェア非依存
速い実行
安全な実行
決定的
分かりやすい

データ表現的には

コンパクト
生成が用意
デコードが速い
コンパイラを検証しやすい
ストリーミング可能
並列化可能

だそうです。

ということで設計は

バイトコード
スタックマシン
現実の機械に合わせた型とオペレーション
構造的コントロールフロー
Fully Typed

になっています。ちょっと筆者による解説を加えると、バイトコードとは1バイト1命令ということです。スタックマシンになっているのは、マシン毎にレジスタ数が異なるのでそこに非依存にしたというのとwasmをネイティブコードにコンパイルする時にスタックマシン->レジスタマシンへの変換になりますが、その手間はそんなに掛からない（らしい）からだと思います。構造的コントロールフローというのは要は goto じゃなくて if で条件分岐するという話です。/解説。

因みにこのようにモジュールや関数、ループ、ifなどがあるのでassemblyという名前から想像する以上に高級です。どちらかというとCFGを書いている気分。

(module
 (func $fibonacci (param $i i32) (result i32)
       (local $a i32)
       (local $b i32)
       (local $tmp i32)
       (set_local $a (i32.const 1))
       (set_local $b (i32.const 0))
       (loop $done $loop
             (if (i32.le_s (get_local $i) (i32.const 1)) (br $done)
               (block
                   (set_local $tmp (get_local $a))
                   (set_local $a (i32.add (get_local $a) (get_local $b)))
                   (set_local $b (get_local $tmp))
                   (set_local $i (i32.sub (get_local $i) (i32.const 1)))))
             (br $loop))
       (get_local $a))
 (export "fib" $fibonacci))

(module

(func $fibonacci (param $i i32) (result i32)

(local $a i32)

(local $b i32)

(local $tmp i32)

(set_local $a (i32.const 1))

(set_local $b (i32.const 0))

(loop $done $loop

(if (i32.le_s (get_local $i) (i32.const 1)) (br $done)

(block

(set_local $tmp (get_local $a))

(set_local $a (i32.add (get_local $a) (get_local $b)))

(set_local $b (get_local $tmp))

(set_local $i (i32.sub (get_local $i) (i32.const 1)))))

(br $loop))

(get_local $a))

(export "fib" $fibonacci))

S式ですね。基本的に機械で処理するので機械可読性が高くてかつ人間可読性も高いフォーマットが選ばれたんでしょう。

で、現状は1.0に向けてほとんどが安定化しているそうです。ChromeやFirefox、 Edgeでテクニカルレビューがあります。また、コンパイラはLLVM、Emscriptenで用意されています。周辺ツールはChromeにテキストビュワーとステッパーがあるそうです。

今後のロードマップは「Ship and Iterate」、とにかくどんどん試していくそうです。1.0で完成ではなくて「最小成果物」でアップデートをどんどんしていく。今のところasm.jsと同等の速度だそうです。もうちょっとC/C++からのコンパイルを整備したいとのこと。面白い機能は後回しだそうです。

仕様に関しては、なんと形式的意味論が定められています（！）。スモールステップの操作的意味論だそうです。リファレンスインタプリタがOCamlで書かれています（これはMLワークショップの発表でしたね:)）

OCamlを使って良かった点は

高速な開発（初期のインタプリタは3日で作ってしまったそうです）
コードが簡潔で「動く仕様」のようになった
型のお陰でバグを防げた
ADTや関数便利
OCamlだと低レベルな型が使える
ポータブル（なおWindows）、ツールチェーンが便利

問題となった点は

文化の衝突
「読めない（´・ω・｀）」
「C++とかPythonとか”real”な言語使おうぜ」
「31/63bit整数ってなんだよ」（筆者注: OCamlはGCのフラグのために整数のbit数ががマシン語 – 1になっています）
「2015年にもなってヘッダファイル？？」
「変数名長くね」
参入障壁
演算子のオーバーローディングがない(int32, int64)
ノミナルなレコードのラベル
セミコロンが紛らわしい
シンタックスエラー
型推論と型エラー
ファンクタ

ハマり所は

評価順序が未定義
構文が変（if vs let vs ; ）
等価性が複数あれけどどれが正しいという訳でもない
ocamlyaccでソースコードのポジションがステートフル

など。

さらに、wasmに特有の問題として

32bit浮動小数点がない
符号無し算術がない
NaN

などなどがあったようです。

因みに中の人が1、2人しかおらず、それはOCamlや関数型言語、形式的意味論に詳しい人が少ないのが原因だそうです。なんかここまで聞いてあまりOCamlの良さを感じないのですが大丈夫ですかね。

そして将来的には

高級言語のサーポートを強化
多値
GC
タグ付き値
クロージャ
末尾呼び出し（の最適化）
例外
スレッド
SIMD
各言語のコンパイラ

なんかをやっていきたいそうです。

Extracting from F* to C: a progress report

Workshop: ML
Talker: Jonathan Protzenko, Karthikeyan Bhargavan, Jean-Karim Zinzindohoue, Abhishek Anand, Cedric Fournet, Bryan Parno, Aseem Rastogi, Nikhil Swamy
PrePrint: Extracting from F* to C: a progress report

TLSの実装を証明したいというモチベーションから産まれたF*という言語について。INRAとMSRとケンブリッジの共同研究で産まれたという血統書付きの代物です。内部的にはCにエクストラクトします。OCamlじゃない理由は整数が1ビット少ないというのとOCamlにはランタイムがあるから、だそうです。

コンパイルフローは

F* -> low* -> C* -> C

1	F* -> low* -> C* -> C

のように3段階に分けてコンパイルしています。

lowというのはFのサブセットで、コンパイルしやすいように一旦低レベルに落としているんでしょう。C*というのは文指向言語です。まあ、手続き型ってことなんですかね。

スタックなんかを手で扱えるけど安全、なんかの特徴をもつようです。

ちょっと色々と説明しづらい点が多いので公式ページを参照して下さい。

F*: A Higher-Order Effectful Language Designed for Program Verification

Compiling with Continuations and LLVM

Workshop: ML
Talker: Kavon Farvardin, John Reppy
PrePrint: Compiling with Continuations and LLVM

タイトルはAndrew W. AppelのCompiling with Continuationsのもじりですかね。

Manticoreという中間表現にCPSを使う並列をサポートするML処理系のバックエンドにLLVMを使った時のお話。一言でいうとつらい。

LLVMは広く使われているコンパイラバクエンドです。SSA形式の中間表現を採用しています。

Manticoreのランイタイムモデルは

効率的な第一級継続（並行のため）
Compiling with Continuationと同じくreturn continuationは引数として渡される
関数は明示的に継続を起動することでreturnする

さて、このモデルをLLVMにコンパイルしようとすると

末尾呼び出しを効率的にしないといけない
GC
割り込みとマルチスレッディングのサポート
第一級ラベル

などなどが問題になります。特に末尾呼び出しについてはかなり問題で、LLVMではこの問題は有名なんだそうです。

LLVMで末尾呼び出しを最適化してもレジスタの保存と復帰が残ってしまうので効率的ではありません。要は使い物にならない。

末尾呼び出しのオーバーヘッドを減らすにはいくつかアプローチがあって、

MLtonはトランポリンを使って手続の呼び出しを減らしている
GHCの呼び出し規約ではcallee saveのみ消せる
ManticoreではJWAという呼び出し規約を作って全てのオーバーヘッドを消した上、naked function（レジスタ操作など余計な命令が付かない関数）も使っている

とのこと。

Naked Functionについてもう少し掘り下げると

ランタイム側がコールフレームをセットアップする
コンパイラはレジスタ溢れ数を制限する
全ての関数で同じフレームを使い回す
FFI呼び出しはそのままいける

のようになります。となると今度はGCについて考える必要があります。

LLVMにGCサポートはあるが、ランタイムモデルにスタックを想定している
しかしManticoreではスタックはただのレジスタが溢れた時の退避場所

つまりGCはスタックを走査する必要がない。普通のGCより簡単になっている。

次は割り込みとマルチスレッディングについてですが、引数で明示的に継続を渡しているのでそこまで問題になりません。スレッドやGCで割り込んだあとは継続を起動するだけです。

で、最後に第一級継続について、ラムダを作るのに第一級ラベルが必要になりますが、LLVMはサポートしていません。どうしたかというとJWAで使っていないリターンアドレスなんかを上手く悪用してどうにかしたようです。

そしてパフォーマンスについてはML RISC（筆者注: 恐らくMLで書かれたコンパラバックエンドだと思います）より随分速かったとのこと。しかし普通じゃないLLVMの使い方をしているせいか、最適化オプションはあまり意味がないよう。

将来的にはSML/NJにマージして欲しいよねーとか言ってました。

SML# with Natural Join

Workshop: ML
Talker: Tomohiro Sasaki, Katsuhiro Ueno, Atsushi Ohori
PrePrint: SML# with Natural Join

大堀研の方から、言語レベルでSQLをサポートするSML#におけるSQLの自然結合の型付けと型推論の話。

割とアルゴリズムの話がメインなので予稿を読んで頂けると。

Eff Directly in OCaml

Workshop: ML
Talker: Oleg Kiselyov, KC Sivaramakrishnan
PrePrint: Eff Directly in OCaml

Olegさんの発表。 delimcc という限定継続ライブラリを使ってEffというエフェクトを扱える言語っぽいeDSLをOCamlに構築したという話。

ここに資料や実装があるので参考にして下さい。

特筆すべき点として、ダイナミックなエフェクト、つまり実行時にEffectを作ることも実現しています。「Creation of effect is itself an effect」だそうです。

Compiling Links Effect Handlers to the OCaml Backend

Workshop: ML
Talker: Daniel Hillerström, Sam Lindley, KC Sivaramakrishnan
PrePrint: Compiling Links Effect Handlers to the OCaml Backend

Multicore OCamlをバックエンドに使うLinksという言語でのEffectの実現について。

代数的エフェクトは抽象的な操作の集合で、コードと操作を分離することが出来ます。操作の実体は後でhandlerという形で渡してあげます。このhandlerには引数の他に限定継続も渡されるので例外や繰り返しなんかが実現出来ます。

さて、限定継続を渡してしまうとなるのちょっと考えることがあります。ハンドラの分類を考えましょう。

例外ハンドラ（継続を無視する）
線型ハンドラ（継続を1回だけ使う）
多重ハンドラ（継続を2回以上使う）

で、これらをMulticore OCamlのバックエンドにコンパイルしたい訳ですが、パフォーマンスが気になります。例外ハンドラや線型ハンドラだと高速化が可能です。しかしながら実際のハンドラがどれになっているかを判定するのは難しいという問題。結局パフォーマンスを諦めて全て多重ハンドラとして扱ってしまったとのこと。

今は線形型を使って線型ハンドラをトラッキング出来ないか模索しているとのことです。

Pattern Synonyms

Workshop: Haskell
Talker: Matthew Pickering, Gergo Erdi, Simon Peyton Jones, Richard Eisenberg
Paper: Pattern synonyms

面白そうだったのでHaskell Symposiumに話を聞きにきました。

パターンのシノニムを作りたいというお話。モチベーションとしては抽象化、可読性、多相パターンの構築なんかがあるそう。

関数が値の構築を抽象化するようにパターンシノニムはマッチ（分解）を抽象化します。

-- Datatype Definition
data Type = TyApp String [Type]

-- Functions abstract construction
tyInt:: Type
tyInt = TyApp "Int" []
mkFunTy:: Type -> Type -> TypemkFunTy t u = TyApp "->" [t, u]
plusTy: TypeplusTy = tyInt `mkFunTy` tyInt `mkFunTy` tyInt

-- petren synonym absrcats matching
pattern FunTy:: Typpe -> Type -> Tye
pattern Funty t u = TyApp "->" [t, u]
funArgTyps:: Type ->([Type], Type)
funArgTys(FunTy t u) = case funArgTys u of
 (ts, r) -> (t:ts, r)

-- Datatype Definition

data Type = TyApp String [Type]

-- Functions abstract construction

tyInt:: Type

tyInt = TyApp "Int" []

mkFunTy:: Type -> Type -> TypemkFunTy t u = TyApp "->" [t, u]

plusTy: TypeplusTy = tyInt `mkFunTy` tyInt `mkFunTy` tyInt

-- petren synonym absrcats matching

pattern FunTy:: Typpe -> Type -> Tye

pattern Funty t u = TyApp "->" [t, u]

funArgTyps:: Type ->([Type], Type)

funArgTys(FunTy t u) = case funArgTys u of

(ts, r) -> (t:ts, r)

さて、シノニムをGHCに入れようと思ったらフロントエンド部分を全て触る必要があります。パーサやリネーム、型検査器などなど。逆にバックエンドへの変更は一切必要ありません。

今回はパターンシノニムの型検査と脱糖についてにフォーカスします。

パターンの型について、まずは型検査の原則から。

パターンの定義を参照することなく、パターンの型のみに基いてwell-typedであるかを決定出来るべきである

ということでパターンの型について考えていきます。パターンはマッチ対象があって、マッチ結果を利用する節があるのでrequirementsやprovidesなんかへの制約があります(Show のインスタンスである、だとか)。考察は長いので省略してしまうと、結果的にパターンシノニムの型には以下の6つが必要になります。

普遍的境界型の変数 univ
要求のコンテキスト Req
scrutinee型(???)の t
存在的境界型の変数 ex
供給のコンテキスト Prov
引数の型 t1 t2 …

ということでパターンの一般化した型はこのようになります。

pattern P::forall univ.Req => exists ex.Prov => t1 -> t2 -> .. -> t

1	pattern P::forall univ.Req => exists ex.Prov => t1 -> t2 -> .. -> t

次に脱糖。変わった点として、マクロ展開とは異なるので少しセマンティクスが変わります。

{-# LANGUAGE PatternSynonyms #-}

f1:: [Bool] -> Bool
f1 [True] = True
f1 _ = False

pattern Single a = [a]
f2 :: [Bool] -> Bool
f2 (Single True) = True
f2 _ = False

main :: IO ()
main = do
  print $ f1 [undefined, undefined] -- undefined
  print $ f1 (False: undefined)     -- False
  print $ f2 [undefined, undefined] -- False
  print $ f2 (False: undefined)     -- undefined

{-# LANGUAGE PatternSynonyms #-}

f1:: [Bool] -> Bool

f1 [True] = True

f1 _ = False

pattern Single a = [a]

f2 :: [Bool] -> Bool

f2 (Single True) = True

f2 _ = False

main :: IO ()

main = do

print $ f1 [undefined, undefined] -- undefined

print $ f1 (False: undefined) -- False

print $ f2 [undefined, undefined] -- False

print $ f2 (False: undefined) -- undefined

こちらに論文とスライドが置かれているようなので興味のある方は見てみて下さい。

Desugaring Haskell’s do-Notation into Applicative Operations

Workshop: Haskell
Talker: Simon Marlow, Simon Peyton Jones, Edward Kmett, Andrey Mokhov
Paper: Desugaring Haskell’s do-notation into applicative operations

GHCのメインの実装者のSimon Marlowsさんから。モナドのdo記法とApplicativeの話。思ったより複雑な事情でした。 Applicativeにもdoを使えるようにしよう、だけでなく、MonadであってもApplicativeの、を使った方が嬉しいケースがあるため。

よく燃える非同期プログラミングの例として、

testFriend a b = do
  ida <- fetchId a
  idb <- fetchId b
  return testFrientById ida idb

testFriend a b = do

ida <- fetchId a

idb <- fetchId b

return testFrientById ida idb

のようにシーケンシャルに書いてしまって「非同期になってないぞと」怒られますね。しかしApplicativeを使って

testFriend a b = testFriendById  fetchId a  fetchId b

1	testFriend a b = testFriendById fetchId a fetchId b

のように書けば2つの fetchId が同時に実行されます(Haskellは書けないので合ってるか自信ないです)。この例のように単純ならまだマシなのですが複雑になると手でApplicativeを書くのは無理があります。

実際、Facebookで使っている非同期ライブラリHaxlで困っているのでどうにかしたい、というのがモチベーションのよう。

さて、どのようなケースでApplicativeに出来てどのようなケースでMonadじゃないといけないかはちょっと面倒です。それは次のような例を見せれば分かるでしょう。

do
 x1 <- A
 x2 <- B
 x3 <- C[x1]
 x4 <- D[x2]
 return (x3, x4)

x1 <- A

x2 <- B

x3 <- C[x1]

x4 <- D[x2]

return (x3, x4)

あとは実際にHackageに上がっているコードで試してみた話なんかもありました。

Malfunctional Programming

Workshop: ML
Talker: Stephen Dolan
PrePrint: Malfunctional Programming

MLワークショップに帰ってきてMalfunctionの話。

OCamlのバックエンド、 Lambda が便利なのでその外部表現であるMalfunctionというのを作ったというお話。

中間表現にはGHCだったら型付きのCore、Javaだったらバイトコード、LispだったらLisp(!)がありますが、OCamlの中間表現には型無しのLambdaが使われています。

MalfunctionはそんなLambdaの外部表現であり、かつインタプリタでもあります。関数型言語の中間表現として有用なのではないかということで作ったそうです。

試しにIdrisのバックエンドをMalfunctionにしてみたレポートがありましたが、IdrisのCバックエンドに比べて数倍速かったようです。

ソースコードは以下より。

Ambiguous pattern variables

Workshop: ML
Talker: Gabriel Scherer, Luc Maranget, Thomas Réfis
PrePrint: Ambiguous pattern variables

OCamlでパターンマッチのORとガードを組み合わせると不自然な挙動になるよね、どうにかしようというお話。

以下のコードを見て下さい。かけ算で、どちらかが1だったらそのまま、それ以外のケースでは Mul を構築するような計算を書いています。

type 'a exp =  | Const of 'a
               | Mul of 'a exp * 'a exp

let is_neutral n = (n = 1)

let mul a b = match a , b with
 | (Const n, v) | (v, Const n)
   when is_neutral n -> v
 | a, b -> Mul (a, b)

type 'a exp = | Const of 'a

| Mul of 'a exp * 'a exp

let is_neutral n = (n = 1)

let mul a b = match a , b with

| (Const n, v) | (v, Const n)

when is_neutral n -> v

| a, b -> Mul (a, b)

これに右が1のパターンを食わせると

# mul (Const 2) (Const 1) ;;
- : int exp = Mul (Const 2, Const 1)

1 2	# mul (Const 2) (Const 1) ;; - : int exp = Mul (Const 2, Const 1)

Const 2 ではなく Mul (Const 2, Const 1) が返ってきてしまいます。これは最初の (Const n, v) にマッチした後、ガードの when is_neutral n に失敗するので次の a, b のパターンに進んでしまうためです。厄介ですね。

かといって (p | q) when g を (p when g) | (q when g) とコンパイラが変換するのは難しく、既存コードのセマンティクスが変わってしまいますし副作用も重複します。どうしようもないです。

ただ、警告という形でユーザに喚起を促すことは出来ます。今回の話はその検知のアルゴリズム。因みにOCaml4.03で既に取り込まれているよう。

実装の詳細については省きます。pattern matrixとか出てきて大分大変そうでした。

Typed Embedding of Relational Language in OCaml

Workshop: ML
Talker: Dmitri Kosarev, Dmitri Boulytchev
PrePrint: Typed Embedding of a Relational Language in OCaml

リレーションを扱う言語としてminiKanrenというのがありますが、それの型付きDSLをOCaml上に構築したというお話。それだけ。

最後に

Industrial Receptionがありました。様々な関数型言語を使う企業からの求人情報があったり、駱駝のデカい置物があったりしました。私はお茶大の浅井先生と話す機会があったのでOCamlの delimcc の実装について訊いたりしてました。

ICFPから時間が経ってしまいましたが併設ワークショップ2日目のレポートでした。もう1日分レポートがあるのでお楽しみに。

Author

admin