「高階多相型ってなんですの？」
TaPLを読んだわけでもなくSystemFを理解したわけでもなくただキーワードに惹かれて高階多相型について最近調べていたのですが、面白い例を見つけたのでまとめてみようと思います。
##なんでも入るリスト
みなさんはJavaScriptを書きますか？僕はJavaScriptが大好きです。JavaScriptでは例えば以下のような配列を作ることができます。
var array = [1, 2, "three", false, {"five":6}];
では同じようなことをHaskellでも出来るでしょうか？
list = [1, 2, "three", False, ("five", 6)]
Couldn't match expected type ‘[Char]’ with actual type ‘Bool’
うーん、怒られてしまいますね。どうにかしてこのリストを正しく型付けできないでしょうか？
そこで出てくるのが高階多相型です！
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
data Any = forall a. Any a
list :: [Any]
list = [Any 1, Any 2, Any "three", Any False, Any ("five", 6)]
実行はできませんが実際これがghciで正常にロードできるのを確認してみてください！
このリストなんでも入ると言っておきながらAnyというデータ構築子で中身を一回包んでいますね。データ構築子を使っていいなら例えばMaybe型だって全てMaybe aの型にできるので同じようなリストを作れそうなものです。
list = [Just 1, Just 2, Just "three", Just False, Just ("five", 6)]
Couldn't match expected type ‘[Char]’ with actual type ‘Bool’
しかしさっきと全く同じエラーで怒られてしまいます。なんでだろうとセルフ型推論して見ると、まずリストの先頭はJust 1で型はたぶんNum a => Maybe aです。次の要素も型は同じで、その次の要素はJust "three"で型はMaybe [Char]になっています。これは型が違いますね！
ではなぜAny型では成功したのでしょうか。Maybe型とAny型の定義をもう一度並べてみます。
data Any = forall a. Any a
data Maybe a = Nothing | Just a
何が違うかわかりますか？一番の違いは型変数が左辺に現れているかどうか、つまりそもそも型のカインドが違うのです！
ghci> :k Any
Any :: *
ghci> :k Maybe
Maybe :: * -> *
Maybe a はNothingもしくはJust aを値としてとります。この時Just aのaの型はMaybe aの型として決まってしまっています。それに対してAnyはforall a. Any aを値としてとります。読み方は任意の型aに対してAny aはAny型の値となる、です。なのでAny型のデータ構築子Anyに適用する値はどんな型のものでも大丈夫なのです！そしてそれら全てがAny型という一つの型に型付けされるからコンパイラに怒られなくて済むというわけです。
さてここまではいいのですが、いざlist :: [Any]を何かに使ってみようとすると少し困ったことがわかります。Anyでくるんだ値はパターンマッチで取り出せばいいのですが、取り出したあとにそれがどういう型の値かわからないので使いようがありません。数値として扱えるのかprintで表示できるのか==で評価できるのかさえわかりません。
ですのでもう少し使いやすくするためにAny型より少し制約を強めた型を作ってみましょう
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
data Printable = forall a. Show a => Printable a
instance Show Printable where
show (Printable a) = show a
list :: [Printable]
list = [Printable 1, Printable 2, Printable "three", Printable False, Printable ("five", 6)]
main = print list
$ runhaskell Main.hs
[1,2,"three",False,("five",6)]
やった！ごちゃまぜのリストを表示することができました！！すごいぞ高階多相型！！！
Printable型の定義は
data Printable = forall a. Show a => Printable a
こうなっています。読み方は任意の型aに対してもしそれがShowクラスのインスタンスならPrintable aはPrintable型の値となる、です。Showクラスのインスタンスで無い型の値をPrintableで包むことはできません。Printable型をShowクラスのインスタンスにするのは簡単で単純に中身を取り出してshowを適用すればいいだけですね！
##高階多相型が必要になる時
面白いことが出来るのはわかったけど実際に使いどころはあるのだろうか？ネットの海をさまよっているとstackoverflowでこんな質問を見つけました。Polymorphism within higher-order functions?. なるほどこれは高階多相型が役に立っている！この章ではこのstackoverflowの内容を元に高階多相型の使用例を解説したいと思います。
data Value = I Int
| S String
| NoValue
例えば簡単なプログラミング言語を作ろうと思った時など上のように"値"を一括りにするような型が欲しくなったりします。例えばこのValue型を比較するためにderiving EqなどでEqクラスのインスタンスにすると
I 1 == I 1 -- True
S "test" == S "test" -- True
I 1 == I 2 -- False
S "apple" == S "orange" -- False
となりますが
I 1 == S "test" -- False
S "test" == NoValue -- False
のようにデータ構築子が違う時もFalseを返してしまい、データ構築子が同じで中身が違うからFalseなのかそもそもデータ構築子が違うのか見分けがつかなくなってしまいます。
そこで新しい比較演算子equal :: Value -> Value -> Maybe Boolを用意してデータ構築子がそもそも違うときはNothingを返して、データ構築子が同じなら中身を比較してJustに包んで返すようにしましょう。
equal :: Value -> Value -> Maybe Bool
equal (I x) (I y) = Just (x == y)
equal (S x) (S y) = Just (x == y)
equal _ _ = Nothing
unequal :: Value -> Value -> Maybe Bool
unequal (I x) (I y) = Just (x == y)
unequal (S x) (S y) = Just (x == y)
unequal _ _ = Nothing
ついでにunequalも作りました。でもこれValue型の型構築子が増えるたびにすべての関数の定義を修正するのはあまり嬉しくないですよね。実際の動作は==や/=の部分であとはそれをMaybe型で包んでるだけなのでもう少しうまく書けそうです。なのでhelper :: (Eq a) => (a -> a -> Bool) -> Value -> Value -> Maybe Boolのような関数をつかって比較関数を生成できるようにしてやりましょう
helper :: (Eq a) => (a -> a -> Bool) -> Value -> Value -> Maybe Bool
helper f (I x) (I y) = Just (f x y)
helper f (S x) (S y) = Just (f x y)
helper _ _ _ = Nothing
equal :: Value -> Value -> Maybe Bool
equal = helper (==)
unequal :: Value -> Value -> Maybe Bool
unequal = helper (/=)
どうです！しかしこれはコンパイルが通りません。
No instance for (Eq a0) arising from a use of ‘helper’
The type variable ‘a0’ is ambiguous
と言って怒られてしまいます。それもそのはずで、
helper f (I x) (I y) = Just (f x y)
の時fはInt -> Int -> Boolと型付けされ
helper f (S x) (S y) = Just (f x y)
の時fはString -> String -> Boolと型付けされるので
helper :: (Eq a) => (a -> a -> Bool) -> Value -> Value -> Maybe Bool
という型では定義の中でaが一貫して同じ型である必要があるのでコンパイルエラーになります。そこで高階多相型の出番です！
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
data Value = I Int
| S String
| NoValue
helper :: (forall a. Eq a => a -> a -> Bool) -> Value -> Value -> Maybe Bool
helper f (I x) (I y) = Just (f x y)
helper f (S x) (S y) = Just (f x y)
helper _ _ _ = Nothing
equal :: Value -> Value -> Maybe Bool
equal = helper (==)
unequal :: Value -> Value -> Maybe Bool
unequal = helper (/=)
思わず全部のコードを書いてしましました。大事なのはhelperの型ですね。
helper :: (forall a. Eq a => a -> a -> Bool) -> Value -> Value -> Maybe Bool
この型だと
helper f (I x) (I y) = Just (f x y)
helper f (S x) (S y) = Just (f x y)
の定義でfの型はEq a => a -> a -> Boolと型付けされます。これは==や/=の型そのものですね！なので制約を受けること無く使うことができるのです。
以上2つの例を通して高階多相型を見てきました。これはとても便利そうですね。自分もまだ学び始めたところなのでまだまだ面白い使い方を知ってるよとかいや高階多相型はそうじゃないんだと教えてくださる方がいらしたら是非教えてください！