存在量化された型

　Haskellでは存在量化された型というものを定義することができ、下のような「何でも突っ込める箱」を書くことができる。
　すごいね。

{-# LANGUAGE ExistentialQuantification #-}

{- |
>>> [ Something 1, Something "str", Something [ 1, 2, 3 ] ]
[1,"str",[1,2,3]]
-}
data Something = forall a. Show a => Something a
instance Show Something where
    show (Something a) = show a

目次

1. 存在量化された型とは？
2. 利用例
3. 二つの記法
4. まとめ

存在量化された型とは？

全称量化された型

　Haskellでは量化された型というものを定義することができる。普段使っているのは、下のような全称量化された型だろう。

data Identity a = Identity { runIdentity :: a }

　上の構文は、下の二つの関数を導入する。

Identity :: forall a. a -> Identity a
runIdentity :: forall a. Identity a -> a

　runIdentityは、任意の型aについてIdentity aからaを取り出すことのできる関数だ。

存在量化された型

　全称量化された型とは別に、存在量化された型というものを定義することができる。

{-# LANGUAGE ExistentialQuantification #-}
data Something = forall a. Something { runSomething :: a }

　上の構文は、下の二つの関数を導入すると連想できる。

Something :: forall a. a -> Something
runSomething :: exists a. Something -> a -- 実際には導入されない。またHaskellには`exists`のようなキーワードは存在しない

　Identityの値コンストラクタと比較すると、全称量化された型との違いはaが左辺にしか現れないということだけだ。しかしrunIdentityとrunSomethingの違いはより大きいように見える。
　runSomethingの型を「Somethingから取り出せる何らかの型aが存在する」と読むとわかりやすい。Somethingは何らかの型を内包していることは確実だが、いかなる型をも入れることができるので、取り出す側はどんな型が出てくるか知ることができないのだ。
　したがってHaskellでは、存在量化された型の中身を取り出す関数を表現することはできない。

利用例

　「何でも突っ込めるが中身を取り出すことはできない型」はどのように役立てられているのだろうか。
　一番わかりやすいのは例外型としての需要だ。

SomeException

　Eitherで失敗を表現する関数を複数使おうと思ったときに、下のような問題にぶつかったことはないだろうか？

mayFailA :: Either FailureA SuccessA
mayFailB :: SuccessA -> Either FailureB SuccessB

mayFailC :: Either ? SuccessB
mayFailC = mayFailA >>= mayFailB -- あれ、Leftの型が合わない……

　いかにもモナドの美しいパワーを発揮できそうな場面なのに、失敗を表現する型が合わないせいでそれが叶わないのだ。
　mayFailCの失敗を表現する型はmayFailAとmayFailBのそれの直和であるが、これをdo文で混ぜて使うには、mayFailAとmayFailBをラップして型を揃える必要があるのだ。
　そこで、Control.Exceptionには下のようなSomeExceptionが用意されている。

data SomeException = forall e. Exception e => SomeException e

　このSomeExceptionはException型クラスを実装している型であれば何でも突っ込むことができる上、自身もException型クラスを実装している。そのため、Eitherで失敗を表現するときはLeftの型をこのSomeExceptionにしておき、内部では自作の例外型をSomeExceptionでラップして投げるという使い方ができる。
　例外を提供するパッケージではSomeExceptionの中身によって例外ハンドラを切り替えることができる仕組みを提供しているため、例外ハンドリングをする上でも型の恩恵を損なうことはない。例外についてはHaskellの例外処理事情という記事が詳しい。

mayFailA :: Either SomeException SuccessA
mayFailB :: SuccessA -> Either SomeException SuccessB

mayFailC :: Either SomeException SuccessB
mayFailC = mayFailA >>= mayFailB -- OK!

開かれた型

　もう一つの例では、後からコンストラクタを追加できるような型を疑似的に作ってみよう。まずは通常の方法で、JSON文字列にエンコードできるJsonValue型を作ってみた。

newtype ObjectKey = ObjectKey String
data JsonValue = IntValue Int | StringValue String | ArrayValue [ JsonValue ] | ObjectValue [ (ObjectKey, JsonValue) ]

encodeJsonValue :: JsonValue -> String
encodeJsonValue (IntValue n) = show n
encodeJsonValue (StringValue s) = show s
encodeJsonValue (ArrayValue xs) = "[" <> intercalate "," (fmap encodeJsonValue xs) <> "]"
encodeJsonValue (ObjectValue xs) = "{" <> intercalate "," (fmap encodeObjectPair xs) <> "}"
    where
    encodeObjectPair (ObjectKey key, jsonValue) = show key <> ":" <> encodeJsonValue jsonValue

　このJsonValue型は表現しうる値を全てコンストラクタで表現している。例えばNullを足そうと思ったらコンストラクタに変更を加えなくてはならないのだ。
　そこで、存在型を使って、表現しうる値を外部から足せるようなJson型を考えてみる。
　まずは骨格を作る。

{-# LANGUAGE ExistentialQuantification #-}

class JsonEncode a where
    encodeJson :: a -> String

data Json = forall a. JsonEncode a => Json a
instance JsonEncode Json where
    encodeJson (Json a) = encodeJson a

　そうしたら、どのモジュールでもどのパッケージでも後から自由に肉付けをしていくことができる。

newtype JsonInt = JsonInt Int
instance JsonEncode JsonInt where
    encodeJson (JsonInt a) = show a

newtype JsonString = JsonString String
instance JsonEncode JsonString where
    encodeJson (JsonString a) = show a

newtype JsonArray = JsonArray [ Json ]
instance JsonEncode JsonArray where
    encodeJson (JsonArray xs) = "[" <> intercalate "," (fmap encodeJson xs) <> "]"

encodeObjectPair' :: (ObjectKey, Json) -> String
encodeObjectPair' (ObjectKey key, json) = show key <> ":" <> encodeJson json

newtype ObjectKey = ObjectKey String
newtype JsonObject = JsonObject [ (ObjectKey, Json) ]
instance JsonEncode JsonObject where
    encodeJson (JsonObject xs) = "{" <> intercalate "," (fmap encodeObjectPair' xs) <> "}"

　存在型Jsonは後から定義された全ての型の和集合のようになっていて、ちょうど型と値コンストラクタの関係に似たものになっている。

記法

　ここでは存在量化された型を書く方法を紹介する。存在量化された型は二つの方法で書くことができる。

ExistentialQuantification

　この記事で使った記法はこちらの方法だ。
　その名の通り存在量化修飾子を書けるようになる。使うにはプラグマが必要になる。

{-# LANGUAGE ExistentialQuantification #-}

data Something = forall a. Something a

GADTs

　こちらは使った人も多いと思う。GADTsとはGeneralized algebraic data typesの略であり、より一般化された代数的データ型を定義できるようになる拡張だ。
　これをExplicitForAll拡張と組み合わせることで、GADTsで存在量化された型を表現することができる。

{-# LANGUAGE ExplicitForAll, GADTs #-}

data Something' where
    Something' :: forall a. a -> Something'

まとめ

　1. 存在量化された型とは、直観的には「何でも突っ込める箱」である。これを使うと複数の独立した型を統合することができる。
　2. 存在量化された型の中身を知る手段はないため、実用には型クラスを使って中身の型を制限することが必要である。
　3. 実用としては、疑似的に後からコンストラクタを追加できるような型を表現したり、疑似的に型クラス(* -> Constraint)を型(*)に落とし込むようなことをすることができる。

　もう少しきちんとした説明は、Haskell/存在量化された型で読むことができる。