GHC 9.2 で導入されたQuick Look型推論アルゴリズムについて

初めまして、朝日ネット開発部の hogeyama です。今回は Haskell の中級的なトピックとして、 GHC 9.2 で導入された Quick Look 型推論アルゴリズムを取り上げようと思います。

概要

Haskell のデファクトスタンダードなコンパイラである GHC では通常の多相（ジェネリクス）の一般化である非可述的多相(impredicative polymorphism)を実装していますが、その型推論アルゴリズムは長らく「型推論が弱い」「実装が不安定でコンパイラのバージョンアップでデグレが起きる」といった問題を抱えていました。

しかし昨年10月、Quick Look という新しいアルゴリズムが GHC 9.2 に実装されたことでこの問題が解決しました。本記事ではこの Quick Look によって何が変わるのか、利用する際に何に気をつければよいのかを非可述的多相の概要から始めて説明していきます。

概要
復習：いわゆる普通の多相について
可述性による制限
これまでのGHCにおける非可述的多相
- 型推論が弱い
- コンパイラバージョン間で互換性がない
Quick Look 型推論アルゴリズム：これからのGHCにおける非可述的多相
推論に失敗するケースと対処方法
- ヒントの探索が打ち切られてしまう場合
- 間違ったヒントを見つけてしまう場合
代償
まとめ
参考文献
採用情報

復習：いわゆる普通の多相について

まずは普通の多相(polymorphism)の復習からしましょう。例としてリストの長さを返す関数 length :: [a] -> Int を考えてみます。この型の意味は「任意の型 a に対して、 a のリスト([a]) を受け取って整数(Int)を返す」という意味でした。つまり、 length の引数として真偽値のリスト [True, False] を与えてもよいし、文字のリスト ['a', 'b', 'c'] を与えてもよいということです。

これを型によって実装を使い分けるアドホック多相(ad hoc polymorphism)と区別して パラメトリック多相(parametric polymorphism) と呼ぶこともあります。「パラメトリック」という言葉の意味は「型は（自由に選べる）パラメータである」という風に理解すれば良いでしょう。実際、length の型に現われる a を 型パラメータ と呼んだりします。

Haskell のデファクトスタンダードなコンパイラである GHC では ExplicitForall という拡張を有効にすることで明示的に型パラメータを導入できます。これを使うと length の型は

length :: forall a. [a] -> Int

と書くことができます。逆に TypeApplications という拡張を有効にすることで、明示的に型パラメータ a を 具体化(instantiate) することもできます。例えば length @Bool と書くと、これは [Bool] -> Int という型の関数として振る舞います。このことを「length を Bool に型適用(type application)する」と呼びます。実際に文字のリストに使ってみましょう。

ghci> let chars = ['a', 'b', 'c']
ghci> length @Bool chars

<interactive>:2:14: error:
    • Couldn't match type ‘Char’ with ‘Bool’
      Expected: [Bool]
        Actual: [Char]
    • In the second argument of ‘length’, namely ‘chars’
      In the expression: length @Bool chars
      In an equation for ‘it’: it = length @Bool chars

確かに「[Bool] を期待しているのに [Char] が渡された」という型エラーになりました。

本記事ではこれ以降、 ExplicitForall と TypeApplications の2つの拡張が有効になっていることを前提とします。

可述性による制限

先ほど「任意の型 a に対して〜」という言い方をしましたが、正確に言うとこれは間違いです。例えば length に forall a. a -> a という型を適用すると、これは型エラーになってしまいます。

ghci> length @(forall a. a -> a)

<interactive>:1:1: error:
    • Illegal polymorphic type: forall a. a -> a
      Perhaps you intended to use ImpredicativeTypes
    • In the expression: length @(forall a. a -> a)
      In an equation for ‘it’: it = length @(forall a. a -> a)

実は、Haskell の多相型には「多相型の型パラメータ自身を多相型で具体化することはできない」という制約があるのです。これを 可述性(predicativity) による制限と呼びます。

この可述性による制限によって、型コンストラクタに多相型を渡すことも禁止されます:

ghci> type X = [forall a. a -> a]

<interactive>:1:1: error:
    • Illegal polymorphic type: forall a. a -> a
      Perhaps you intended to use ImpredicativeTypes
    • In the type synonym declaration for ‘X’
ghci> type Y = Maybe (forall a. a -> a)

<interactive>:2:1: error:
    • Illegal polymorphic type: forall a. a -> a
      Perhaps you intended to use ImpredicativeTypes
    • In the type synonym declaration for ‘Y’

これを回避するためには通常 newtype によるラッパーが使われます。 newtype Id = Id { unId :: forall a. a -> a } のような型を作り、length @(forall a. a -> a) の代わりに length @Id、[forall a. a -> a] の代わりに [Id] を使うというわけです。

例えば、Haskellの有名パッケージ lens では Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t) という型の newtype である ALens という型¹と、専用の関数群(^#, #~, #%~など) が提供されています。

ただ、いちいち newtype を作って毎回ラップ・アンラップしたり専用の関数を書くのは面倒ですよね。できる限りボイラープレートコードを減らしたいというのは全人類に共通する欲求と言ってよいでしょう。

これまでのGHCにおける非可述的多相

GHC はそのような欲求をみたすために十数年以上も前から ImpredicativeTypes という拡張を用意しています。この拡張を有効にすると可述性による制限が解除され、先ほどの type X や length @(forall a. a -> a) が使えるようになります。 ALens も不要になります。

ghci> :set -XImpredicativeTypes
ghci> type X = [forall a. a -> a]
ghci> length @(forall a. a -> a) [id,id]
2

これでめでたしめでたし、とは残念ながら行きませんでした。 GHC 9.0 以前の ImpredicativeTypes 拡張は次の課題を抱えていたのです。

型推論が弱い
コンパイラバージョン間で互換性がない

順に見ていきましょう。

型推論が弱い

デモンストレーションのために標準ライブラリ(base パッケージ)の runST :: forall v. (forall s. ST s v) -> v を使います。 argST という変数が forall s. ST s Int という型を持つとしましょう。すると当然 runST argST は型推論に成功します。しかし以下の app 関数を噛ませて

app :: forall a b. (a -> b) -> a -> b
app f x = f x

app runST argST とすると、それだけでパスしなくなってしまいます²。

GHCi, version 9.0.2: https://www.haskell.org/ghc/  :? for help
ghci> app runST argST

<interactive>:1:19: error:
    • Couldn't match type: forall s. ST s b
                     with: m0 a0
      Expected: m0 a0 -> b
        Actual: (forall s. ST s b) -> b
    • In the first argument of ‘app’, namely ‘runST’
      In the expression: app argST runST
      In an equation for ‘it’: it = app runST argST
    • Relevant bindings include it :: b (bound at <interactive>:1:1)

このように、プログラマにとっては明らかに型がつく式でも注釈なしにはコンパイルできないことが大半でした。これが問題その1です。

コンパイラバージョン間で互換性がない

さらにコンパイラバージョン間で互換性が保証されていないという問題もありました。次のコードは GHC 7.10.3 では型推論に成功しますが、 GHC 8.10.7 や GHC 9.0.2 では失敗します。

let f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
    f (Just g) = Just (g [3], g "hello")
    f Nothing  = Nothing
in (f . Just) reverse

GHC の型推論器は非常に巨大で、日々新しい機能が追加されたり修正されたりしています。以前のアルゴリズムはそのような変更に弱かったのです³。そのため、GHC は拡張を提供するものの、あくまで実験的な機能であって動作の保証はしないという扱いでした。 GHC 9.0.2のユーザーガイドには以下のように記載があります。

However the extension should be considered highly experimental, and certainly un-supported.

これが問題その2です。

Quick Look 型推論アルゴリズム：これからのGHCにおける非可述的多相

この十数年に渡る問題を解決したのが本記事のタイトルにある Quick Look と呼ばれる型推論アルゴリズムです。 GHC 9.2 にこのアルゴリズムが実装されたことによって

型推論が強くなった
コンパイラバージョン間で互換性が壊れにくなった

という変化が起きました。その結果、ImpredicativeTypes はついに正式にサポートされることになりました。

それでは Quick Look がどういうアルゴリズムで、なぜ型推論が強く互換性が壊れにくいのかをアルゴリズムの解説を通じてお伝えしようと思います。

アイデア

Quick Look の基本的なアイデアは、「型推論の途中で変数と関数適用部分だけをチラ見（= quick look）して型パラメータの具体化先のヒントを得る」というものです。

次の cons id ids という例を用いて説明をしましょう。

cons id ids -- 期待する型推論の結果は [forall c. c -> c]
  where
    cons :: forall a. a -> [a] -> [a]
    id   :: forall b. b -> b
    ids  :: [forall c. c -> c]

Quick Look では、先頭の関数(cons)の型の引数部分と実引数(id, ids)の型を見比べます：

a と forall b. b -> b
[a] と [forall c. c -> c]

この2つから a の具体化先のヒントを得ようというわけです。

さて、突然ですがここで問題です。上記の1番目から直ちに a := forall b. b -> b としてよいでしょうか？答えは No です。なぜならば、もし cons id の型を [forall b. b -> b] -> [forall b. b -> b] としてしまうと cons id [\x -> x + 1] のような式に型が付かなくなってしまうからです。 b := Int, a := Int -> Int のような可能性を残さないといけないわけですね。

一方で、2番目については a := forall c. c -> c 以外の選択肢はありません。というのも、1番目のように c := Int とすると [Int -> Int] が得られますが、これは元の ids の型 [forall c. c -> c] とは全く互換性のない型となってしまうからです。 forall b. b -> b は Int -> Int になることができますが、[forall c. c -> c] は [Int -> Int] になれないというところに違いがあるんですね。

Quick Look アルゴリズムはこの事実を見極め、 a := forall c. c -> c というヒントを見つけることができます。判断基準はやや複雑なため、正確な説明は元論文を参照していただきたいのですが、実用上は [forall c. c -> c] のように 型コンストラクタ内に多相型がある場合は Quick Look が機能することが多い と覚えておけばよいでしょう。

ヒントを得た後は、それを元の型に戻して通常の型推論に戻ります。今回の場合、 cons の型が (forall c. c -> c) -> [forall c. c -> c] -> [forall c. c -> c] になるので、id に a = forall c. c -> c という型が付くことと ids に [a] = [forall c. c -> c] という型が付くことを検査して終わりになります。

型推論能力の高さ

先ほどの例では型コンストラクタ [] を使った例をお見せしましたが、これは [] 以外のすべての型コンストラクタでも同様です。つまり、 Maybe はもちろんのこと -> でも Quick Look は機能します。

`Maybe` の例

(.) f Just
  where
    (.)  :: forall a b c. (b -> c) -> (a -> b) -> a -> c
    f    :: Maybe (forall d. [d] -> [d]) -> Maybe ([Int], [Char])
    Just :: forall e. e -> Maybe e

(.) の第一引数の型 b -> c と f の型をマッチさせて b := Maybe (forall d. [d] -> [d]) と c := Maybe ([Int], [Char]) を得ます。

`->` の例

app runST argST
  where
    app   :: forall a b. (a -> b) -> a -> b
    runST :: forall v. (forall s. ST s v) -> v
    argST :: forall s. ST s Int

app の第一引数の型 a -> b と runST の型をマッチさせて a := (forall s. ST s v) と b := v を得ます。

このように、記事の前半で紹介したすべての例を注釈なしで型推論できます。

GHCの変更への強さ

Quick Look が行うのは「変数と関数適用だけ⁴を見てヒントを挿入する」というだけで、残りは既存の型推論アルゴリズムと全く変わりません。このため、9万行からなるGHCの型推論器の中で Quick Look はたったの450行ほどで実装できたとのことです。

実装を小さくシンプルすることで、既存の多数の機能を壊さず、今後の機能追加・修正にも強くしているんですね。

推論に失敗するケースと対処方法

型推論能力が高いとは言ったものの、どうしても推論できないようなケースも存在します⁵。そこで、推論に失敗する典型的なケースとそのときの対処方法について説明します。

ヒントの探索が打ち切られてしまう場合

先ほど述べたように Quick Look は変数と関数適用しか見ません。このことは実装をシンプルに保つ一方で、λ式やif式、let式、case式などが現れた時点でヒントの探索を打ち切ることを意味します。例えば次のような式はだめです。

cons id $ case someFlag of
  True  -> ids
  False -> []

これを防ぐためには関数適用の外側で let を使って変数にしてやるのがよいでしょう⁶。

let arg = case someFlag of
            True  -> ids
            False -> []
 in cons id arg

間違ったヒントを見つけてしまう場合

app runST argST の変種として以下を考えます。第二引数を a から () -> a に変えてみました。

app' runST argST'
  where
    app'   :: forall a b. (a -> b) -> (() -> a) -> b
    runST  :: forall v. (forall s. ST s v) -> v
    argST' :: forall s. () -> ST s Int

こうすると第二引数も型コンストラクタ -> で包まれるため、 () -> a と forall s. () -> ST s Int もヒントの探索対象となります。説明は省略しますが、ここから得られるのは a := forall s. ST s Int ではなく、なんらかの単相型 s0 に対して a := ST s0 Int になります。その結果 runST の型と矛盾が起きて型推論は失敗してしまいます。

これを防ぐためには「λ式ではヒントが探索されない」というルールを逆手に取り、app' runST (\x -> argST' x) のように変換してあげればよいです。なお、このように、式 e を \x -> e x で置き換えることを η展開 と呼びます。

実用上は「とりあえず困ったらη展開してみる」という方針でよさそうです。

代償

残念なことに、Quick Look は無償で手に入ったわけではありません。

先ほど、「-> を含むすべての型コンストラクタで Quick Look は動作する」と述べましたが、実は -> を Quick Look に対応させるためには Simplify subsumption と呼ばれる変更が必要でした⁷。この変更には後方互換性がなく、例えば以下のコードは GHC 8 以前ではコンパイルできますが、GHC 9.0 以降⁸ではコンパイルできません。

f :: (forall a. Int -> a -> a) -> String
f h = h 0 ""

g :: (Int -> forall a. a -> a) -> String
g = f
--  ^
-- • Couldn't match type: forall a. Int -> a -> a
--                  with: Int -> forall a. a -> a
--   Expected: (Int -> forall a. a -> a) -> String
--     Actual: (forall a. Int -> a -> a) -> String
-- • In the expression: f
--   In an equation for ‘g’: g = f

この代償が Quick Look やその他のメリットに見合うものだったのかについては賛否両論があり、Reddit などで議論が交わされています。

なお、Simplify subsumption によってコンパイルできなくなったコードも、たいていの場合はη展開で修正できます。上記の例では g = \x -> f x と書き直せばコンパイルできるようになります。

まとめ

GHC 9.2 に Quick Look というアルゴリズムが実装され、 ImpredicativeTypes が公式サポートされました
- その結果、 newtype によるラッパーを使わずに済むことが増えます
Quick Look は(i)関数適用時に(ii)多相型が型コンストラクタに包まれた形で出現するとだいたいうまく動作します
- うまくいかないときは以下の方針で対処すると良いでしょう
  - 部分式を let で括り出す
  - それでもだめならη展開を試す
代償として、GHC 8 以前から 9 以降に移行する際にコードの修正が必要になる場合があります。
- この場合もη展開で直ることがほとんどです。

説明できなかった点も多いため、興味がある方はぜひ元論文をご覧ください。

参考文献

A quick look at impredicativity - Microsoft Research
- 元となった論文
A Quick Look at Impredicativity (ICFP 2020) - YouTube
- 上記論文の学会発表のビデオ
GHC proposal - Quick Look Impredicativity
GHC proposal - Simplify subsumption
6.4.16. Impredicative polymorphism — Glasgow Haskell Compiler 9.2.1 User's Guide
著者によるTwitterでの解説

採用情報

朝日ネットでは新卒採用・キャリア採用を行っております。

厳密に言うと単なる newtype ではないのですが↩
app と ($) はほとんど同一のものですが、実は runST $ argST は 9.0 以前の GHC でも(ImpredicativeTypes なしで)コンパイルできます。これは GHC が ($) を特別扱いしているためです。↩
Quick Lookの著者による説明があります: https://twitter.com/trupill/status/1378073234558570502 ↩
正確には型注釈を付けた式も対象です↩
非可述的な型を含む型推論は決定不能問題であることが知られています。つまり、常に完璧な答えを返すようなアルゴリズムはどうやっても作れません。↩
別解として型注釈をつけるという方法もあります: cons id (case someFlag of { True -> ids; False -> [] } :: [forall a. a -> a])↩
Simplify subsumption は Quick Look のためだけに導入されたわけではなく、GHC 8.0以前の simplify されていない subsumption が抱えていた、(i)コンパイラの複雑化、(ii)非直感的なセマンティクスという問題を解決する目的もありました。詳細については上記リンク(GHC proposal)や論文の5.8節をご覧ください。↩
Simplify subsumption 自体は Quick Look に先んじて GHC 9.0 で実装されました。↩

朝日ネット　技術者ブログ

朝日ネットのエンジニアによるリレーブログ。今、自分が一番気になるテーマで書きます。

GHC 9.2 で導入されたQuick Look型推論アルゴリズムについて

概要

復習：いわゆる普通の多相について

可述性による制限

これまでのGHCにおける非可述的多相

型推論が弱い

コンパイラバージョン間で互換性がない

Quick Look 型推論アルゴリズム：これからのGHCにおける非可述的多相

アイデア

型推論能力の高さ

`Maybe` の例

`->` の例

GHCの変更への強さ

推論に失敗するケースと対処方法

ヒントの探索が打ち切られてしまう場合

間違ったヒントを見つけてしまう場合

代償

まとめ

参考文献

採用情報

概要

復習：いわゆる普通の多相について

可述性による制限

これまでのGHCにおける非可述的多相

型推論が弱い

コンパイラバージョン間で互換性がない

Quick Look 型推論アルゴリズム：これからのGHCにおける非可述的多相

アイデア

型推論能力の高さ

Maybe の例

-> の例

GHCの変更への強さ

推論に失敗するケースと対処方法

ヒントの探索が打ち切られてしまう場合

間違ったヒントを見つけてしまう場合

代償

まとめ

参考文献

採用情報

`Maybe` の例

`->` の例