Simon Peyton Jones先生招待講演について

nushio
エンジニア

2011-09-28 14:54:00

村主です。

2011年9月21日に、ICFP2011で来日していたSimon Peyton-Jones先生を弊社にお招きして、Glasgow Haskell Compilerの最新事情について講演をしていただきました。当日は体が浮きそうなほどの風が吹く大嵐でしたが、多くの人の協力のおかげで無事に終えることができ、感謝しています。

サイモン先生からスライドを分けてもらったので、講演会の動画とあわせて読む形で、記事にまとめてみました。Haskell/GHCのさまざまなトピックをカバーするこの講演、みなさんのHaskell勉強の一助となれば幸いです。


サイモン先生に「君たちも何か話してよ」と頼まれたので、僕が流体計算言語Paraiso(リンク先にスライドあり)の話をまずしています。

31:46 頃からサイモン先生のトークが始まります。まずはHaskell Communities and Activities Reportの紹介をしています。いろんなHaskellで作ったものを集めたリストです。半年に一度集計しているので、Haskellで何か作っている人はぜひ作ったよ〜報告をして載せてもらいましょう。

42:00 最初のテーマは型クラス入門です。

対応箇所はスライドの14ページ目からです。

52:00 次は、type families (型族)の話です。

スライドの10ページ目からあわせてご覧ください。

1:14:30 そしてGADTの話です。ここでサイモン先生はホワイトボードを使ったのですが、動画だとほとんど読み取れません。そこで、この記事の後の方に、板書を再現したものを載せましたので、ご参照ください。

1:34:50 最後のテーマは、Haskellでのさまざまな並列プログラミングの紹介でした。

この同じParallel = Functionalのスライドを使ったサイモン先生の講演動画はここから見ることができます。

講演会後、神勢に行ってラーメンを食べました。

神勢でサイモン先生を囲む

GADT板書

サイモン先生のGADTに関するトークをもとに、ホワイトボードの内容を再現してみます。実際に動かせるコードはこちら


さて、GADTとは何か?GADTを使う古典的な例といえば構文木です。そこで構文木を作ってみましょう。こんな構文木に馴染みがありますか?(なくても大丈夫)

data Expr
= LitI Int — Intのリテラル
| LitB Bool — Boolのリテラル
| Plus Expr Expr — 2つの式の加算
| If Expr Expr Expr — 条件分岐
deriving (Eq,Show)

限定的な演算しかありませんが、これで以下のような式をHaskellで表現できます。

ast1 :: Expr
ast1 = If (LitB True) (LitI 81) (LitI 118)
ast2 :: Expr
ast2 = Plus (LitI 3) (LitI 7)

しかし、このままではこんな構文木も書けてしまいます!

ast3 :: Expr
ast3 = Plus (LitB True) (LitI 4971)

こいつは型がつきません!ナンセンスです。このような式が許される言語があるとしたら、とてもわるい言語と言えるでしょう。え?そうです、Cはとてもわるい言語ですね!このようなわるい式を受け付けないようにするために、GADTを使って構文木を改造してみましょう。

GADTを使うためにはまず、代数データ型の定義を、ちょっと違う構文で書き直す必要があります。

data Expr where
LitI :: Int -> Expr
LitB :: Bool -> Expr
Plus :: Expr -> Expr -> Expr
If :: Expr -> Expr -> Expr -> Expr
deriving (Eq,Show)

代数データ型のコンストラクタのそれぞれに関数としての型を併記しています。この型はさっきとは見た目が変わっただけで同じ型ですので、いままでの式は(わるい奴まで含めて)みなこの型の構文木として表現できてしまいます。

いよいよこの型をGADT化してみます。まずは、Exprを型から型コンストラクタにする必要があります。Expr a は「a型の答えを返す式」といった意味になります。それぞれのデータコンストラクタがどう進化するか考えてみましょう。

data Expr a where
LitI :: Int -> Expr Int
LitB :: Bool -> Expr Bool
Plus :: Expr Int -> Expr Int -> Expr Int
If :: Expr Bool -> Expr a -> Expr a -> Expr a
deriving instance Show (Expr a)

構文木にはこんな感じで型がつくようになりました。

ast1 :: Expr Int
ast1 = If (LitB False) (LitI 81) (Plus (LitI 3) (LitI 7))
ast2 :: Expr Bool
ast2 = (LitB True)

そして、あのわるい式は型エラーになりました。やったね!悪は去った!

ast3 = Plus (LitB True) (LitI 4971) — 型エラー!!

このように、構文木のデータ型のコンストラクタがパラメタ化されて、それが含んでいる型の情報を表現できるようになりました。その結果、まず構文木を作るのが楽しくなりましたね。しかし、構文木からデータを取り出すことを考えると、もっと楽しいことが起こるのです!

その例として、この構文木のevalを作ってみましょう。

GADTを使う前の、旧版のExprのevalを作る事はできなかったでしょう。

eval :: Expr -> a — 何型を返せばいいの?

ところが、Exprが型コンストラクタである今となっては、evalの型は自明です。

eval :: Expr a -> a

さあ、実装してみましょう。Intリテラルのevalはこう書けます。

eval (LitI i) = i

だって、LitIにマッチした時点で、iの型はIntであると分かりますから!同じ理由からBoolリテラルは

eval (LitB b) = b

となります。またPlusはこうなります。

eval (Plus x y) = eval x + eval y

xとyはExpr Int型ですから、evalすることでInt型の値が取り出せて、それらは足し算ができるってわけ。
Ifも同様です。Ifにパターンマッチした後では、eval aはBool型だと分かりますから、これをifに渡すことができます。

eval (If a b c) = if eval a then eval b else eval c

ここで注目すべきは、GADTを使うと、

data Expr a where

という、型変数aを含む代数データ型Expr aのコンストラクタでありながら、

LitI :: Int -> Expr Int
LitB :: Bool -> Expr Bool
Plus :: Expr Int -> Expr Int -> Expr Int

のように、Expr a以外の(より具体的な)型を返すようなものを記述できるということです。すると、そのコンストラクタにパターンマッチした分岐では、型変数aについて、追加の情報が得られる、ということです。凄いじゃないですか!

これがGADTの全てです。GADT = General Algebraic Data Typeです。Generalだ、というのは、通常のHaskellのデータ型、たとえばMaybe aを書いたときには、

data MayBe a where
Just’ :: a -> MayBe a
NoThing :: MayBe a

のように、コンストラクタは常にデータ型宣言と同じ型の値しか返せませんでした。しかし、GADTならそれ以外の値も返せるってことです。単にそれだけです!

GADTで型変数に与えられる制約はただ、型を具体化するだけではありません。GADTでどんなことができるのか、見て行きましょう。
まずリテラルは、一般化できますね。

Lit :: a -> Expr a

足し算できるものはIntに限りません。Numのインスタンスである型なら何でも足し算できるはずです。ですので、Plusを

Plus :: Num a => Expr a -> Expr a -> Expr a

と拡張してみます。これで、Plusにパターンマッチした分岐では、aはNumクラスの型だと分かるので、足し算ができます!

それから、レコードに名前をつけることもできます。

If :: {cnd :: Expr Bool, tru :: Expr a, fls :: Expr a} -> Expr a

詳細については、GHC user’s guide 7.4.7節を見てください。もちろん、GHCの最新の構文が知りたかったら、user’s guideを見るのが一番。とくに7章は最高です!(訳注:執筆時点で、GHC 7.0.3の構文が更新され、user’s guideにある構文はdeprecatedになっているので、GHC7.0.3のほうに合わせてあります)

LitがShowのインスタンスばかりとは限らなくなったので、deriving ShowするにはaがShowのインスタンスであるという制約が必要になりました。

deriving instance Show a => Show (Expr a)

evalもアップデートしましょう。リテラルのevalはこう書けます。

eval (Lit a) = a

Plusは一見変更ないように見えますが、xとyは Expr Int 型から、Num a => Expr a 型に拡張されました。

eval (Plus x y) = eval x + eval y

Ifも変更なしです。

eval (If a b c) = if eval a then eval b else eval c

Int型以外の構文木も作れるようになりました。せっかくなので新しく導入したレコード名を使ってみましょう。

ast2 :: Expr Double
ast2 = If {
cnd = Lit False,
tru = Lit 81,
fls = Plus (Lit 0.7) (Lit 3.5)
}

最後に、こんな関数を考えてみましょう。

foo :: Expr a -> a -> a

ご覧の通り、fooは一般の型aに対して定義されています。そんな時でさえ、

foo (Plus _ _) z = z * (z+1)

と、Plusにマッチした分岐では、aがNumのインスタンスであることが分かりますから、zに対してNumのメソッドである足し算、掛け算、fromIntegerなどが使えるようになります。もちろん、他の分岐、たとえばLitにマッチした場合には、型変数aについてなんの情報も得られませんから、同じようにzに演算を施そうとするとエラーになってしまいます。

foo (Lit v) z = z * (z+1) — これは型エラー!

“GADT Haskell”で検索するとさまざまな美しい例が載った論文がたくさん出てきます。しかし、覚えておくべき大事なことは、パターンマッチという動的な行為の結果、型についてなにがしかの静的な情報を得ることができるということです。

Leave a Reply