Help us understand the problem. What is going on with this article?

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

More than 1 year has passed since last update.

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

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

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

多相

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

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 を含む型は取れないし、

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

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

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

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

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

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

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 を含めることもできます。

{-# 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 を含む型を与えることはできません。

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 には highly experimental だとか certainly unsupported だとか書かれているので、うまく動作しなかったり、 GHC のバージョン間で動作が変わる可能性があります。実用するコードで使うべきではないでしょう。

ImpredicativeTypes があると、

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

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

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

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

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

Impredicative types - Haskell Wiki にあった例を見てみましょう:

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 系ではこれではダメみたいで、次のように明示的型適用をしてやる必要がありました:

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

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

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

関数適用演算子の特例

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

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

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

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

runST $ do { ... }

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

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

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

-- オレオレ関数適用演算子
($$) :: (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 を有効にして

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

参考文献

Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
Comments
No comments
Sign up for free and join this conversation.
If you already have a Qiita account
Why do not you register as a user and use Qiita more conveniently?
You need to log in to use this function. Qiita can be used more conveniently after logging in.
You seem to be reading articles frequently this month. Qiita can be used more conveniently after logging in.
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
ユーザーは見つかりませんでした