Blog

2016.9.18

ICFP及び関連イベント参加レポート – Haskell Day –

κeenです。夜行バスで預け荷物が行方不明になるなどのトラブルがあって更新が遅れましたが関数型言語の国際カンファレンス(at 奈良)のICFP及び併設イベント、及び周辺の有志イベントに参加しています。今日は0日目、有志で行なわれるHaskell Dayでした。 Haskellの父にしてGHC作者のSimon Pyton JonesさんがICFPで来日しているので東京で1日使ってHaskellの勉強会が開かれており、それに参加してきました。

タイムテーブルは以下のようになっていて(イベントページより引用)、私は午後のセッションから参加しました。

時間	発表内容	発表者	スライド	発表
10:00-12:00	Haskell チュートリアル ( 準備 )	hiratara	日本語	日本語
12:00-13:30	ランチ(lunch time)
13:30-13:50	Haskell Relational Records	khibino	英語	日本語
13:50-14:10	Spock	lotz84_	英語	日本語
14:10-14:30	Introduction to Stack’s Docker integration (with our company’s case!)	igrep	英語	日本語
14:30-14:50	SAT/SMT solving in Haskell	msakai	英語	英語
14:50-15:10	HTTP/2 and TLS in Warp	kazu_yamamoto	英語	英語
15:10-15:30	休憩(break)
15:30-17:30	Into the Core: squeezing Haskell into nine constructors	Simon Peyton Jones	英語	英語

Haskell Relational Record Composable, Typesafe SQL building

presenter: khibino
slide: Haskell Relational Record Composable, Typesafe SQL building

Haskell Relational Record作者のkhibinoさんによるHRRの解説でした。

HRRはHaskell DSLからSQLを生成するクエリビルダです。特徴としてはDSLなので合成可能で、型安全な所です。文字列でSQLを書いちゃうと合成も出来なければ返り値の型も分かりませんね。さらに、Template Haskellというコンパイル時コード生成機構(Lispの衛生的マクロのようなもの)でコンパイル時にテーブルスキーマからコード生成もできます。

余談ですがkhibinoさんの会社の認証サービスは1割がHaskellで出来ているそうです。

宣言的と言われるSQLですが、

SELECT ALL T0.name AS f0, T0.age AS f1, T0.family AS f2,
           T1.name AS f3, T1.day AS f4
      FROM EXAMPLE.person T0 INNER JOIN EXAMPLE.birthday T1
    ON (T0.name = T1.name)

SELECT ALL T0.name AS f0, T0.age AS f1, T0.family AS f2,

T1.name AS f3, T1.day AS f4

FROM EXAMPLE.person T0 INNER JOIN EXAMPLE.birthday T1

ON (T0.name = T1.name)

のようなクエリはもうちょっと数学的に宣言的に書けて、

{(p,b)∣p∈P,b∈B,πP.name(p)=πB.name(b)}

1	{(p,b)∣p∈P,b∈B,πP.name(p)=πB.name(b)}

のようになる筈です。 Haskellっぽく比較的それに近い記法で書くとこうなります。

   [ (p, b)
   | p <- person, b <- birthday , P.name p == B.name b ]
   -- List Comprehension

do { p <- person; b <- birthday; guard (P.name p == B.name b)
   ; return (p, b) }  -- List Monad

[ (p, b)

| p <- person, b <- birthday , P.name p == B.name b ]

-- List Comprehension

do { p <- person; b <- birthday; guard (P.name p == B.name b)

; return (p, b) } -- List Monad

で、実際は

personAndBirthday :: Relation () (Person, Birthday)
personAndBirthday =  relation $ do
  p <- query person
  b < b

personAndBirthday :: Relation () (Person, Birthday)

personAndBirthday = relation $ do

p <- query person

b < b

のように書けるというのがHRRの売り。

今の例だとINNER JOINを簡単に書けましたが、OUTER JOINだったら右のテーブルがMaybeになったり、 GROUP BYを使うとまた型が変わったりと「ちゃんと型付け出来る」という紹介がありました。

また、特徴にcomposabilityがありましたが、

sameBirthdayHeisei :: Relation () (Day, Int64)
sameBirthdayHeisei =  aggregateRelation $ do
  p <- query person
  b =. value (fromGregorian 1989 1 8)
  gbd . value 1
  return $ gbd >< personCount

sameBirthdayHeisei :: Relation () (Day, Int64)

sameBirthdayHeisei = aggregateRelation $ do

p <- query person

b =. value (fromGregorian 1989 1 8)

gbd . value 1

return $ gbd >< personCount

のように繰り返し使われる式はletで束縛することでコード上は重複を避けることが出来ます。

その他にもMySQLのように無言で間違った式を実行してしまうRDBMSを使っていても、HRR側が型で弾くので安全です。

1つkhibinoさんが悩んでいる所はplaceholder機能で、「Placeholderは1変数につき1回だけ使用可能で、引数としては出現した順に受けとる」という制約をDSLで表現するのが難しいとのことでした。私がuniq型を使って1回だけ使用可能という部分を表現してはどうかと質問しましたが、引数が可変長であったり順番に受け取らないといけなかったりする部分で難しさがあるとのことでした。その後の議論でHListを使ってセッション型にすれば型としては表現出来るけど果たしてそれで便利になっているかはまた別の話ということになりました。

Spock

presenter: lotz
slide: Introduction to Web Development with Spock – Qiita

次はlotzさんでSpockというWebフレームワークの紹介とそれを使ったWebアプリの作り方にについての発表でした。 SpockはSinatraライクなフレームワークで、手軽にサクッとWebアプリを作れるとのこと。発表でも「明日からHaskellでWebアプリが作れるように」のコンセプトでサクサクと実装を進めていていました。

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Web.Spock
import Web.Spock.Config
import qualified Data.Text as Text

main :: IO ()
main = do
  spockCfg <- defaultSpockCfg () PCNoDatabase ()
  runSpock 8080 $ spock spockCfg $ do

    get root $
      text "Hello Spock!"

    get ("hello"  var) $ \name ->
      text (Text.concat ["Hello ", name, "!"])

{-# LANGUAGE OverloadedStrings #-}

module Main where

import Web.Spock

import Web.Spock.Config

import qualified Data.Text as Text

main :: IO ()

main = do

spockCfg <- defaultSpockCfg () PCNoDatabase ()

runSpock 8080 $ spock spockCfg $ do

get root $

text "Hello Spock!"

get ("hello" var) $ \name ->

text (Text.concat ["Hello ", name, "!"])

パスやURLパラメータに型がつくなどのHaskellらしい特徴もありました。

DB connectionやセッションはアプリケーションのコンテキストに入れて引き回すようです。そこまでフレームワークが面倒をみてくれるんですね。他にもテンプレートエンジンや暗号ライブラリの紹介なども。

DBと繋ぐ時のSQLは手書きのようなので、上述のHRRと組み合わせることも出来そう。

Spock自体はRubyでいうRackのようなWAIの上に構築されています。例えばログを出したいとなったらミドルウェアを夾むと簡単に出来るそうです。

会場からの質問は、Spockと同様なフレームワークのScottyとの違いは、というのがありました。色々と違いはあるものの、SpockはWAIのミドルウェアを作るのに対してScottyはApplicationを作るのでSpockの方がアプリケーションのカスタマイズ性が違うとのことでした。

もう一つ、パフォーマンスについての質問がありましたが発表者は調べてないとのことでした。まあ、世の中Railsのように重いフレームワークでも元気にプロダクションで動いているのでベースのサーバが速ければその上のフレームワークはそこまで関係ないですかね。

Introduction to Stack’s Docker integration (with our company’s case!)

presenter: igrep
slide: Introduction to stack’s docker integration (1)

次はigrepさんによるHaskellのツールチェーン、StackのDocker Integrationの紹介でした。

Haskellのコンパイラ、GHCはHaskellをコンパイルするとシングルバイナリを吐くので本来ならそのバイナリを配置するだけでデプロイは完了します。しかし実際にはクロスコンパイルだったりバイナリ互換だったりの問題があるので中々上手くいきません。そこで、StackのDocker Integrationを導入することで手軽にサーバで動くバイナリを生成出来ます。

stack.yamlに

docker:
  enable: true

1 2	docker: enable: true

と書くだけでビルド環境をDockerの中で構築して、コードをビルド、バイナリを吐いてくれます。環境構築がなくて非常に楽とのことでした。曰く、「もはやCIとかなくてもいいかも」とのこと。

便利ですね。

SAT/SMT solving in Haskell

presenter: msakai
slide: HaskellDay2016_sakai – HaskellDay2016_sakai.pdf

次は抽象によるソフトウェア設計−Alloyではじめる形式手法や型システム入門 −プログラミング言語と型の理論−の翻訳で有名なmsakaiさんによるSAT (Boolean Satisfiability Problem) とSMT (Satisfiability Mobulo Theories)のソルバの話でした。

SATとは「(P ∨ Q) ∧ (P ∨ ¬ Q) ∧ (¬ P ∨ ¬ Q) のような論理記号式の変数、 P , Q に真または偽を代入して式全体を真に出来るか」を解く問題です。この例だと解くことが出来て、解は {P ↦ True, Q ↦ False} になります。この問題はNP完全で、解くには本来なら膨大な時間が掛かりますが、様々に最適化されたSATソルバを使うことで数百万変数/制約の式でも解くことが出来ます。怖いですね。

SAT自体は理論的にも実用的にも重要であるものの、解きたい問題を落とし込むのが難しい、低レイヤーなソルバなのでもっと高レイヤーなSMTを使うと便利です。 SMTソルバはSATソルバと何かしらの理論のソルバ、を組み合わせたもので、例えば算術ソルバと組み合わせたりBitVectorソルバと組み合わせたりします。

SMTソルバの使い道はソフトウェア/ハードウェアの検証、定理証明、数独などのパズル、Liquid Haskellの型チェックなどなど様々な使い道があるそうです。

そして、そのSMTソルバをHaskellから使えるSBVの紹介がありましたバックエンドにはz3やCVC4、Yices、Boolectorなどが使えるそう。

コード例はSEND+MORE=MONEYの覆面算で出てました。

sendMoreMoney :: IO SatResult
sendMoreMoney = sat $ do
        ds @[s , e , n , d , m , o , r , y] = 0 &&& x .<= 9
            val xs = sum $ zipWith (*) (reverse xs) (iterate (*10) 1)
            send = val [s,e,n,d]
            more = val [m,o,r,e]
            money = val [m,o,n,e,y]
        constrain $ bAll isDigit ds
        constrain $ allDifferent ds
        constrain $ s ./= 0 &&& m ./= 0
        solve [send + more .== money]

sendMoreMoney :: IO SatResult

sendMoreMoney = sat $ do

ds @[s , e , n , d , m , o , r , y] = 0 &&& x .<= 9

val xs = sum $ zipWith (*) (reverse xs) (iterate (*10) 1)

send = val [s,e,n,d]

more = val [m,o,r,e]

money = val [m,o,n,e,y]

constrain $ bAll isDigit ds

constrain $ allDifferent ds

constrain $ s ./= 0 &&& m ./= 0

solve [send + more .== money]

sInteger のように整数型のSMT変数を作るDSLだったり .<= のようにSMTの制約を作るDSLだったりがあります。

さらに、ご自身でPure HaskellなtoysolverというSAT/SMTソルバも作られていて、それの紹介もありました。現状SMTのコンペティションでは全然奮いませんが来年再チャレンジしたいとのことでした。

HTTP/2 and TLS in Warp

presenter: kazu_yamamoto
slide: http2.gby – 2016-http2-tls.pdf

HTTP/2関連でかなり活躍されているkazu_yamamotoさんからWarpという高速なHaskellのHTTPサーバの紹介がありました。

先程のSpockがWAIの上で動くフレームワークですが、WarpはWAIのプロトコルを喋るサーバです。

最初にHTTP/1.1の問題点を指摘したあと、HTTP/2での解決策を紹介しました。

そして、HTTP/2の機能のためにframingやhpack、priority treeなどを実装したそうです。さらにそれをWarpに載せて、TLSライブラリの強化も行なったそうです。さらにパフォーマンスに関してもチューニングをし、マルチコア環境においてはNginXよりも高速にレスポンスを返すまでになったそうです。すごい。

TLSに関しては度重なる脆弱性の発覚や仕様の不足、次期仕様が策定中などの条件を勘案するとTSL 1.2しか使えるものがなく、どうしてもTLS 1.2が必要だったそうです。

この他にも将来的にTLS 1.3の実装やTCPの代替のQUICプロトコルの実装などが必要だそうです。

その他、質問ではSimon Peyton Jonesさんから「Cのライブラリとかもあるのに何故Haskellで実装したの？」と質問がありましたが「プロトタイピングなので何度も作っては壊すことになり、ある程度テストを書かなくても型で正しさを保証してくれる言語が欲しかった」との回答がありました。

Into the Core: squeezing Haskell into nine constructors

presenter: Simon Peyton Jones

Haskellの父のGHCの作者のSimon Peyton Jonesさんの講演です。

Simonさんは最初からテンション高めに裸足で講演をし、何度か会場に質問を投げ掛けながら進めていったので入りから会場をがっつり掴んでいきました。

内容はGHCのコア部分についてで、GHCのコミッタを増やしたいからみんなに解説するね:pとのことでした。

コア部分についてですが、GHCは様々な機能を持っていますがその大部分は構文糖として提供されていて、脱糖したあとの言語は非常に小さいです。それをCoreと呼んでいます。そのCoreのデザインなどが主な話でした。

コア言語はSimply Typed Lambdaでは無理があり、

compose :: forall a b c. (b -> c) -> (a -> b) -> a -> c
compose = \f: b -> c. \g:a -> b. \x:a.
  let tmp:b = g x
  in f tmp

compose :: forall a b c. (b -> c) -> (a -> b) -> a -> c

compose = \f: b -> c. \g:a -> b. \x:a.

let tmp:b = g x

in f tmp

のような式はabcが解決されないので破綻します。

System Fを使えだとかなんだとか様々に意見が上がったそうですが、結局本当にSystem Fが求めていたものだそうです。

compose :: forall a b c. (b -> c) -> (a -> b) -> a -> c
compose = \\abc. \f: b -> c. \g:a -> b. \x:a.
  let tmp:b = g x
  in f tmp

compose :: forall a b c. (b -> c) -> (a -> b) -> a -> c

compose = \\abc. \f: b -> c. \g:a -> b. \x:a.

let tmp:b = g x

in f tmp

のようにして型も引数で受け取るようにしたら解決するとのことでした。そこで会場から「GHC8.0.0で入った機能に似てる」という質問がありましたが、まさにそれはCoreの機能で一部をユーザに公開したものだとの回答がありました。

次はCore言語に対する処理の話でインライン化、rewrite rules、ベータ簡約、caseの最適化とjoin pointなどの話が続きました。

コンパイルのパスは様々にあるがこれらの適用順番はどう決めた？という質問が会場から上がり、手探りだよとの回答がありました。そこでさらに機械学習で順番決めたら？と質問があり、「そうだね！妖精さんが解決してくれるもんね！」との回答もありました。因みにコンパイルパスの順序決定は挑んでいる人もいるようですが、1ヶ月遺伝的アルゴリズムを回して3%改善した、などの結果に終わっているようです。

コンパイルパスを色々に紹介されていたのですが、ここではcaseのショートカットやその辺の話をピックアップして紹介します。

例えば

case x of
  True  -> case x of (True -> e1 | False -> e2)
  False -> e3

case x of

True -> case x of (True -> e1 | False -> e2)

False -> e3

のような式はよく考えたら

case x of
  True  -> e1
  False -> e3

case x of

True -> e1

False -> e3

で済む筈です。こういう変数について分かっている情報を伝播すればある程度簡単になります。しかし、そうも簡単な話ではなくて、例えば

notNull xs = not (null xs)

1	notNull xs = not (null xs)

をインライン展開すると

notNull xs = case (case xs of
                     []     -> True
                     (p:ps) -> False) of
                True -> False
                False -> True

notNull xs = case (case xs of

[] -> True

(p:ps) -> False) of

True -> False

False -> True

となりますね。これは先程の最適化をアテにするなら

notNull xs = case xs of
               []     -> case True  of (True -> False | False -> True)
               (p:ps) -> case False of (True -> False | False -> True)

notNull xs = case xs of

[] -> case True of (True -> False | False -> True)

(p:ps) -> case False of (True -> False | False -> True)

とすると

notNull xs = case xs of
               []     -> False
               (p:ps) -> True

notNull xs = case xs of

[] -> False

(p:ps) -> True

と畳み込めます。でも、これは case xxx of (True -> False | False -> True) のコードをコピーしています。今回は True False と簡単な式でしたがもし巨大な式だったら case xxx of (True -> BIG1 | False -> BIG2) をコピーしてしまうことになり大変なことになります。それに対する回避策やさらなる問題、その答えなどの話もありました。

最後にGHCとコミュニティの話をして、みんなもコミュニティに入ろうぜとして締められました。

最後に

ICFPの前哨戦となるHaskell Day 2016が終わりました。 SPJさん来日とあって150名を越えるHaskellerが集い、Simonさんも興奮気味でした。私を含む次の日のICFP併設ワークショップに参加する人達は夜行バスで移動する人が多いようです。

それではまた明日も頑張ります。

Author

admin