非可述多相に触れる： GHC の ImpredicativeTypes 拡張

この記事では、マイナーGHC拡張の一つである ImpredicativeTypes について解説してみようと思います。これが必要になる場面はほぼないと思います。

ここのコード例は GHC 8.0.2 と 8.2.2 でテストしています。他のバージョンでの結果は保証しません。

まずは、非可述的 (impredicative) じゃない、通常の多相からおさらいしていきましょう。

# 多相

一つの関数やデータ型を任意の型に対してに適用できることを、（パラメーター）多相と呼びます。便利ですね！

```haskell
data Maybe a = Nothing | Just a
-- Maybe Int や Maybe String, Maybe (Maybe Bool) などが使える

double :: (a -> a) -> a -> a
double f x = f (f x)
-- double :: (Int -> Int) -> Int -> Int や double :: (String -> String) -> String -> String として使える
```

## forall を含む型

上記の `double` 関数の型における `a` は型変数で、**任意の**型を動くことができます。forall キーワードを使ってこのことを明示すると `forall a. (a -> a) -> a -> a` となります。（forall キーワードの利用には ExplicitForAll 拡張が必要です）

さて、通常の Haskell では、 forall を含む型は通常の型とは扱いが異なります。
具体的に挙げると、関数の引数として forall を含む型は取れないし、

```haskell
hoge :: (forall a. a -> a -> a) -> Bool -- Error!
hoge f = f True False
```

データ構築子の引数の型を forall を含む型にはできないし、

```haskell
newtype CNat = CNat (forall a. a -> (a -> a) -> a) -- Error!
```

また、多相関数の型変数 (`id :: a -> a` の `a`) に forall を含む型（例：`(forall s. ST s a) -> a`）を入れて具体化することはできません。

```haskell
alias_for_runST :: (forall s. ST s a) -> a
alias_for_runST = id runST -- Error!
```

それに、 Maybe 等の型構築子に forall を含む型を与えることはできません。

```haskell
m :: Maybe (forall a. a -> a -> a) -- Error!
l :: [forall a. a -> a] -- Error!
```

つまり、このセクションの最初に書いた「**任意の**型を動くことができる」という表現にはごまかしがあって、「**forall を含まない任意の**型を動くことができる」と書くのがより正確です。

# ランクN多相

GHC では RankNTypes 拡張を有効にすると、forall を含む型を引数として受け取る関数を書くことができます。ST モナドの `runST :: (forall s. ST s a) -> a` なんかがおなじみですね。このほか、 RankNTypes 拡張の下では、データ構築子の引数の型に forall を含めることもできます。

```haskell
{-# LANGUAGE RankNTypes #-}
hoge :: (forall a. a -> a -> a) -> Bool -- OK!
hoge f = f True False

newtype CNat = CNat (forall a. a -> (a -> a) -> a) -- OK
```

ただし、相変わらず型変数 a を forall を含む型で具体化することはできないし、型構築子に forall を含む型を与えることはできません。

```haskell
alias_for_runST :: (forall s. ST s a) -> a
alias_for_runST = id runST -- Error!

m :: Maybe (forall a. a -> a -> a) -- Error!
l :: [forall a. a -> a] -- Error!
```

# 非可述多相

型変数に forall を含む型で具体化できることを、非可述的であると言います。言葉としては論理学に由来するようですが、ここでは深く掘り下げません。

非可述多相には、GHC拡張としては ImpredicativeTypes が対応します。ただし、 [GHC User's Guide](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#impredicative-polymorphism) には *highly experimental* だとか *certainly unsupported* だとか書かれているので、うまく動作しなかったり、 GHC のバージョン間で動作が変わる可能性があります。実用するコードで使うべきではないでしょう。

ImpredicativeTypes があると、

```haskell
m :: Maybe (forall a. a -> a -> a) -- OK!
l :: [forall a. a -> a] -- OK!
```

等の型を書けるようになります。 ~~見るからにキモいですね。~~

非可述多相は強力ですが、強力すぎる故に重大な代償があります。ざっくり言って、型推論が死にます。（「力の代償に何かを失う」というのはみなさんマンガやアニメでお馴染みの設定だと思うので、詳細は省きます）

（まあ、ランクN多相の時点ですでに型推論が機能しない場面は出ていますが…。）

型を明示する方法としては、型注釈の他に、GHC 8.0系で導入された明示的型適用 (TypeApplications) を使う方法があります。

[Impredicative types - Haskell Wiki](https://wiki.haskell.org/Impredicative_types) にあった例を見てみましょう：

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

-- GHC 7.6.1 ではこれで動くらしい；しかし GHC 8.0.2 および 8.2.2 ではエラー
h = f ((Just :: (forall a. [a] -> [a]) -> Maybe (forall a. [a] -> [a])) reverse)
```

例では `Just` に型注釈をつけています。しかし GHC 8 系ではこれではダメみたいで、次のように明示的型適用をしてやる必要がありました：

```haskell
h = f (Just @(forall a. [a] -> [a]) reverse)
```

型適用とは何かというと、 `Just :: forall c. c -> Maybe c` という型に含まれる型変数 `c` を直接指定できるという代物です。

Haskell に明示的型適用と非可述多相を加えたものは実質 System F と呼んでいいと思います。型推論に頼れない世界で、色々遊んでみてください。

## 関数適用演算子の特例

Haskell における関数適用演算子 `$` は、次のように定義されます：

```haskell
($) :: (b -> c) -> b -> c
($) f x = f x
```

これと ST モナド (Control.Monad.ST) の `runST :: (forall s. ST s a) -> a` 関数を組み合わせてみましょう。

というわけで `$` 演算子を介して `runST` を呼び出すこと

```haskell
runST $ do { ... }
```

を考えます。このとき、 `($) :: (b -> c) -> b -> c` の型変数への代入は `b := forall s. ST s a`, `c := a` となり、型変数 `b` の型に forall が含まれます。つまり、非可述多相が必要です。

しかし、この頻出であると考えられるパターンに非可述多相が必要というのはちょっとあんまりだと思われたのか、 Haskell 標準の `($)` は特別扱いされており、 ImpredicativeTypes なしでも `runST $ do {...}` のパターンが通るようになっています。（参考：[ImpredicativePolymorphism – GHC](https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism)）

自分で同様の演算子を作ってもこのような特別扱いは起こりませんし、関数合成演算子 `(.)` には同様の措置は取られていません。よって、

```haskell
-- オレオレ関数適用演算子
($$) :: (b -> c) -> b -> c
($$) f x = f x

{-
hoge :: a -> a
hoge x = runST $ return x -- OK without ImpredicativeTypes!
-}

fuga :: a -> a
fuga x = runST $$ return x -- Error!

piyo :: a -> a
piyo = runST . return -- Error!
```

というコードはエラーとなります。（相当のコードのコンパイルを通したかったら、 ScopedTypeVariables と TypeApplications と ImpredicativeTypes を有効にして

```haskell
fuga :: forall a. a -> a
fuga x = ($$) @(forall s. ST s a) runST (return x)

piyo :: forall a. a -> a
piyo = (.) @(forall s. ST s a) runST return
```

とすると良さそうです。）

ちなみに、 Haskell に影響を受けた言語の一つである PureScript は、このような `($)` の特別扱いはしていないようです：[documentation/Differences-from-Haskell.md at master · purescript/documentation](https://github.com/purescript/documentation/blob/master/language/Differences-from-Haskell.md#no-special-treatment-of-)

# 参考文献

- 型システム入門 (TaPL)
- [Impredicative types - Haskell Wiki](https://wiki.haskell.org/Impredicative_types)
- [GHC User's Guide](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#impredicative-polymorphism)
- [ImpredicativePolymorphism – GHC](https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism)