GHCの中間言語Coreへの脱糖を覗き見る

Haskell (その3) Advent Calendar 2017 11日目の記事。(予約投稿知らなかったのでフライングになった)

GHCがコンパイルの途中で中間表現として用いるCoreの生成っぷりを観察する。

観察して、あーはいはいなるほどね(わかってない)、と言うだけになりそう。

はじめに

GHCはHaskellのソースコードを低レベルなコードへとコンパイルする過程で様々なpass(コンパイルのステージ)を通じてプログラムデータを変換する。 俯瞰図は下記のリンクに詳しい。

Compiling one module: HscMain

僕がGHCの話をどこかで聞きかじってかっこいいな、と思ったのは、 GHCがコンパイラの中間言語として定義しているCoreを知った時。

このCoreと名付けられた中間言語はDesugar passにて生成され、下記のような性質を持っている。

• 小さな構文
  • 3つのデータ型と15の値コンストラクタ
• 束縛変数には全て型がついている
  • 前段で推論されている
• 全て型がついているため高速に型検査ができる
  • もう推論は終わっているので検査が高速
• 単純だが大きな表現力を持つ
  • Haskellのソースプログラムがこれに変換される

GHCはリリースのたびに様々な言語拡張が増えていて、 表面上の構文は多様になってきている。 それにも関わらずこのCoreという中間言語は下記のような小ささを保っている。

• 3つのデータ型
• 15の値コンストラクタ

ghc-8.2.2 CoreSyn

data Expr b
  = Var   Id
  | Lit   Literal
  | App   (Expr b) (Arg b)
  | Lam   b (Expr b)
  | Let   (Bind b) (Expr b)
  | Case  (Expr b) b Type [Alt b]
  | Cast  (Expr b) Coercion
  | Tick  (Tickish Id) (Expr b)
  | Type  Type
  | Coercion Coercion
  deriving Data

data AltCon
  = DataAlt DataCon 
  | LitAlt  Literal
  | DEFAULT
   deriving (Eq, Data)

data Bind b = NonRec b (Expr b)
            | Rec [(b, (Expr b))]
  deriving Data

type Arg b = Expr b
type Alt b = (AltCon, [b], Expr b)

各値コンストラクタが依存している更に細かいデータ型はあるにせよ、 Haskellのソースコードは上記のデータ型にdesugar(脱糖)されて単純化される。

正直、僕もすべてのコンストラクタの意味が解っているわけではない。 しかしあの多彩な表現力を持ったHaskellの構文が この小さなCoreに変換可能である ことに大きく驚いた。

ここではこれらのデータ型の詳細には立ち入らず、 実際にHaskellのプログラム書きながらこのdesugarされたCoreがどう変化しているかを見てみようと思う。

観察してみる

この節ではGHCのデバッグオプションを使って、 parseされたプログラムがDesugar passを経た後の結果を確認してみる。

どんな感じで見えるんだろ。

Setup

stack.yamlにオプションをつけておこう。

ghc-options:
  "*":  -ddump-to-file  -ddump-ds -ddump-simpl -dsuppress-idinfo -dsuppress-coercions -dsuppress-uniques -dsuppress-module-prefixes

長い。長いけれどポイントは -ddump-ds のみ。 -dsuppres 系は冗長な出力を減らすために指定しているだけ。

このオプションをつけておくとstackのビルドの成果物を格納する .stack-work ディレクトリの下にレポートが出力される。

今回 src/Lib.hs に定義を書き下しているため出力結果は

.stack-work/dist/x86_64-linux-nix/Cabal-1.24.2.0/build/src/Lib.dump-ds

というファイルに出力される。

定数

stringConst :: String
stringConst = "Hello"

-- RHS size: {terms: 2, types: 0, coercions: 0}
stringConst :: String
stringConst = unpackCString# "Hello"#

まあ、なんか、うん。そうだよね。

関数適用

falsy :: Bool
falsy = not True

-- RHS size: {terms: 2, types: 0, coercions: 0}
falsy :: Bool
falsy = not True

変化なし。単純過ぎたか。

Infix

two :: Int
two = 1 + 1

-- RHS size: {terms: 6, types: 1, coercions: 0}
two :: Int
two = + $fNumInt (I# 1#) (I# 1#)

なにか起きた。。。

二項演算子も結局は関数なので、 + 1 1 のようなS式っぽい見た目になるのはわかる。

$fNumInt という謎のシンボルが出てきた。

後でも出てくるが型クラス Num の Int インスタンス定義を渡している模様。

関数合成

notNot :: Bool -> Bool
notNot = not . not

-- RHS size: {terms: 3, types: 3, coercions: 0}
notNot :: Bool -> Bool
notNot = . @ Bool @ Bool @ Bool not not

x . y が . x y に変換された。 これもまた二項演算子が2引数の関数に変換されている。

だけではなくて @ Bool なる記号が出てくる。 これは . が持つ多相性に関連する。 次で説明。

多相関数

identity :: a -> a
identity x = x

-- RHS size: {terms: 3, types: 3, coercions: 0}
identity :: forall a. a -> a
identity = \ (@ a) (x :: a) -> x

ちょっと形が変わった。大事なところにきた。

Haskellで匿名関数と作る時は

\ x -> x

とする。

なので

\ (x :: a) -> x

となるなら解る。 「aという型を持つxという値を受けとり、そのxを返す」というような意味で読める。

しかし実際は

\ (@ a) (x :: a) -> x

こう。

(@ a)

匿名関数に引数が増えている。

これは 型変数が関数の仮引数として定義されている ことを表す。

とても不思議。

-- 型    値
\  (@ a) (x :: a) -> x

型と値が同列の引数として扱われていることになる。

Coreでは型の引数と値の引数が同列に扱われて関数に適用される。

なのでこの関数に引数を適用する場合は、

identity Int 1

のようにして型引数が決定され、値引数が決定されているものと思われる。

補足: forall について

identity :: forall a. a -> a

forall が表れるが意味的にはもとの a -> a となんら変わらない。 糖衣構文として forall の省略が許容されていたものが、 脱糖を経て明示化されただけ。

補足: Core上の表現

この関数がCore上でどう表現されているかというと

Lam (TyVar "a") (Lam (Id "x") (Var (Id "x")))

ラムダ計算っぽく書くと

λ a. λ x: a. x 

こんな感じ? (解らないけど a にはkindとして * でもつくのかな？)

1つめのラムダ抽象の引数は型で、 2つめのラムダ抽象の引数はa型の値xとなる。

この2つの引数はCore言語内で Var という型を持つ。

Var

型と値が同列で引数になる仕組みは簡単で、 関数の引数に束縛されるデータ型 Var が下記のようになっているから。

data Var
  = TyVar ...   -- 型レベルの変数
  | TcTyVar ... -- 不明 "Used for kind variables during inference" らしい
  | Id ...      -- 値レベルの変数

この関数の引数に与えられるデータが

• TyVar: 型
• Id: 値

どちらも受け付けるようになっている。

多相関数の適用 (型変数が決定されるのか？)

本当に型も引数として関数に適用されているのかを観察。 先程の多相関数に引数を適用してみる。

one :: Int
one = identity 1

-- RHS size: {terms: 3, types: 1, coercions: 0}
one :: Int
one = identity @ Int (I# 1#)

予想通り。

@ Int で確かに型を適用している。

高階関数

おなじみの関数合成。

comp :: (b -> c) -> (a -> b) -> a -> c
comp f g x = f (g x)

-- RHS size: {terms: 9, types: 11, coercions: 0}
comp :: forall b c a. (b -> c) -> (a -> b) -> a -> c
comp =
  \ (@ b) (@ c) (@ a) (f :: b -> c) (g :: a -> b) (x :: a) -> f (g x)

引数がお化け。。。。

だけれど、型変数の抽出ルールはやはり明確だ。

型変数は b c a の順で登場する。 それに合わせて forall b c a の順で定義される。

さらに forall に続く型変数はCoreのラムダ抽象で引数になる。

パターンマッチ

hasValue :: Maybe a -> Bool
hasValue (Just _) = True
hasValue Nothing  = False

-- RHS size: {terms: 8, types: 7, coercions: 0}
hasValue :: forall a. Maybe a -> Bool
hasValue =
  \ (@ a) (ds :: Maybe a) ->
    case ds of _ {
      Nothing -> False;
      Just _ -> True
    }

関数定義部におけるパターンパッチはcase of構文に変換されている。

CoreのCaseコンストラクタに変換されているらしい。

Case  (Expr b) b Type [Alt b]

実はこのコンストラクタ b と Type の部分がまだ何者か判明していない。

b が Expr b を束縛しており、 Type が [Alt b] の式の型を注釈している？

型クラス制約

型クラスつきの関数を定義するとどうなるだろうか。

join :: (Monad m) => m (m a) -> m a
join = (>>= id)

-- RHS size: {terms: 8, types: 17, coercions: 0}
join :: forall (m :: * -> *) a. Monad m => m (m a) -> m a
join =
  \ (@ (m :: * -> *)) (@ a) ($dMonad :: Monad m) (ds :: m (m a)) ->
    >>= @ m $dMonad @ (m a) @ a ds (id @ (m a))

斬新な変数が出てきた。 引数部分を分解して一つ一つ読み解こう。

(@ (m :: * -> *))    -- Monadのインスタンスとなるべき型
(@ a)                -- mで修飾された入力値の型の一部
($dMonad :: Monad m) -- 型クラスを満たすインスタンスの定義
(ds :: m (m a))      -- 実際の関数の入力値

join に表れる型変数は m と a 。

なのでその2つは最初に (@ (m :: * -> *)) と @ a として束縛される。 (ds :: m (m a)) は実際の関数の引数なので疑問なし。 問題は ($dMonad :: Monad m) というどこから出てきたのか解らない束縛。

これは型クラスのインスタンスも関数の引数として受け取るための束縛らしい。

ということは、型クラスのインスタンスを渡しているところも見られるかもしれない。。。

型クラスのインスタンス適用

さきほど定義した join を使ってみよう。

maybeOne :: Maybe Int
maybeOne = join (Just (Just 1))

-- RHS size: {terms: 6, types: 5, coercions: 0}
maybeOne :: Maybe Int
maybeOne =
  join
    -- (@ (m :: * -> *))
    @ Maybe
    -- (@ a)
    @ Int
    -- ($dMonad :: Monad m)
    $fMonadMaybe
    -- (ds :: m (m a))
    (Just @ (Maybe Int) (Just @ Int (I# 1#)))

コメントで先程の join の定義と対照してみた。

Monad のインスタンス定義を受け取る部分には

$fMonadMaybe

が。

名前から察するにどうやらMaybeのインスタンス定義が渡されているようだ。 (Scalaが型クラスのインスタンスとしてimplicitパラメータで渡しているものと、ほぼ同じものだと思われる。)

Monad

最後にモナドを含むdo記法がどのようにCoreに変換されるのかを見てみる。

printArgs :: IO ()
printArgs = do
  args <- System.Environment.getArgs
  print args

-- RHS size: {terms: 7, types: 8, coercions: 0}
printArgs :: IO ()
printArgs =
  >>=
    @ IO
    $fMonadIO
    @ [String]
    @ ()
    getArgs
    (\ (args :: [String]) -> print @ [String] $dShow args)

doは糖衣構文なので脱糖後は >>= を使った式に変換されるのは予想できた。

型周りは思ったよりいろいろ混ざってきて混乱。 上から見ていく。

bind関数の定義。(型制約は除く)

>>= :: m a -> (a -> m b) -> m b

これは forall つきで表現すると

>>= :: forall m a b. m a -> (a -> m b) -> m b

となる。

よって

(@ (m :: * -> *))
(@ a)
(@ b)

が型変数として関数の引数に抽出される。 実際の対応をみてみると

-- (@ (m :: * -> *))
@ IO
-- ここはMonadのインスタンスとしてIOの定義を渡している
$fMonadIO
-- (@ a)
@ [String]
-- (@ b)
@ ()

これらを使うと >>= は下記のように具象化される。

--     getArgsより    printより
>>= :: IO [String] -> ([String] -> IO ()) -> IO ()

型変数だった部分全てに具体的な型が当てはまった。

まとめ

Haskellのプログラムはdesugar(脱糖)後にCoreという中間言語に変換される。

Coreは基本的に型付きラムダ計算(の変種)なので

• 変数
• 関数の定義
• 関数の適用
• その他 Let, Case ...

などのわずかな定義で構成される。

さらに値と型が同レベルで束縛されるラムダ抽象を用いることで

• 型クラスのインスタンス渡し
• 具象型の決定

などの操作が ただの関数適用 で実現されている。

少ない規則で多彩なユースケースを実現している好例がGHCの中に潜んでいることを知ることができてよかった。

Less is more.

Yoshiko is Yohane.

Reference

• Simon Peyton Jones Into The Core
• GHC Compiler pass
• CoreのAPI Document in GHC 8.2.2
• GHCのデバッグオプション
• GHCにおける多彩な情報の出力方法
• もっと踏み込んだ解析 Dive into GHC: Targeting Core
• この記事よりもちゃんと調べている: GHC Core by example, episode 1: Hello, Core!

下記、余談

モチベーション

Haskell Day 2016が日本で開催された時にSimon Peyton Jonesさんが"Into the Core"というタイトルでプレゼンされたらしい。 残念ながら僕は都合がつかず聞きにいけなかったけれど、同じテーマの講演が動画に収められていたのでそれをリンクしておく。

Into the Core - Squeezing Haskell into Nine Constructors by Simon Peyton Jones

早口過ぎて99%何を言っているのか僕には解らない。 けれどところどころなんとなく伝わる気がする。

プレゼンで使ったスライドは こちら

これをぼんやり聞いていて「Coreってなんだか面白いな」と思ったのがきっかけ。

これから

Coreの理論的背景になっているSystemFというラムダ計算の一種が何者なのか気になる。

GHCで用いられているSystemFCという変種については下記のリンクが参考になりそうだけど。

System F with type equality coercions

僕はそもそもラムダ計算素人なので下記の書籍を読み進める必要がありそう。

型システム入門 プログラミング言語と型の理論

最短で

• 3章: 型無し算術式
• 8章: 型付き算術式
• 9章: 単純型付きラムダ計算
• 23章: 全称型

を読めば辿り着けるように見える。

いやーほんとかなあ。。。