ゆうれい，いぞん，そんざい，ﾗｧｩﾝｸﾄｩｩﾎﾟﾘﾓｫﾌｨｼﾞｩﾑｯ

ゆうれい，いぞん，そんざい，ﾗｧｩﾝｸﾄｩｩﾎﾟﾘﾓｫﾌｨｼﾞｩﾑｯ
我々が型をつけるとき，基本的に型はある種の条件を表すものとして扱うことが多い．例えば， Int であれば値は整数であるという条件だし， Num a => a であれば Num クラスのインスタンスである型 a という条件を表している．
であるならば，プログラム上の様々な条件を型にしたいのは静的型付き言語を扱うプログラマにとって自然な欲求であろう．
GHCはこういった欲求に答えるため様々な型ハックをサポートしている．ここではそういった型ハックの一部を扱うことにする．

型タグ
事前条件と事後条件が型でわかるようにしたいとする．たとえば，暗号化を考えてみよう．暗号化する前と暗号化した後を型で区別したいというのは自然な発想だろう．そういった場合，一番最初にたどり着く発想は単純に newtype で同じ内部表現を持つ別の型にしてしまうことである．(以下の例は拝借したもの)(拝借元を忘れる1敗)
type1.hs
	newtype Plain = Plain ByteString
	  deriving (Show, Eq)
	newtype Encrypted = Encrypted ByteString
	  deriving (Show, Eq)
	encrypt :: Plain -> Encrypted
	encrypt m = ...
こうすれば，暗号化済みの値を取るべきところに間違って暗号化前の値を突っ込んでしまったりしても，コンパイルエラーが起きる．しかし，この方法では Plain ,  Encrypted 両方を受け取るような関数を作る場合，型クラスを持ち出す必要がある．内部表現は一致しているのに型を合わせるためだけに型クラスを持ち出すのはいささか面倒である．

そこで，もう一つの本質的に同じ方法として，型タグを使った方法がある．
type2.hs
	data Plain     = Plain
	data Encrypted = Encrypted
	 
	newtype Message a = Message ByteString
	  deriving (Show, Eq)
	encrypt :: Message Plain -> Message Encrypted
	encrypt m = ...
この場合， Plain ,  Encrypted 両方で使えるような関数を定義する際， Message がパラメトリックなため，わざわざ型クラスを実装する必要ない．
type3.hs
	append :: Message a -> Message a -> Message a
	append x y = coerce $ (coerce @_ @ByteString x) ++ (coerce @_ @ByteString y) 
この実装であれば，実装しているうちにステータスが増えたときも，型クラスと違いインスタンスの追加などの手間がかからず， newtype を使ったときよりも拡張性に優れている．
また，型タグを使った方法はもっと多くのステータスを持つ場合に有効である．例えば，IDを型に持ち上げたい時，IDが何番まであるかは実装時にはわからない．こういったとき，型タグとして型レベル自然数を使えば，(実装上の上限があるとはいえ)任意個のステータスを持った型を表現することができる． また，複数の条件を型にしたい時，その組み合わせは爆発的に増える．
こういった理由から，プログラム上の条件を型として表現する場合，型タグを使う使った方法が newtype を用いて新しい型を定義する方法よりも一般に良いとされている．

余談
 type2.hs の定義では Plain や Encrypted に値コンストラクタがあるが，これらの型は型タグとして使用されることだけを想定しているため，ライブラリ作成者の意図しない使用を制限するためにも値コンストラクタは存在しないほうが良い．幸い，GHCでは EmptyDataDecls 拡張によって値コンストラクタを省略したデータ型宣言をすることができる．これは現在のGHCではデフォルトで有効になっている．

幽霊型
 type2.hs の Message の定義を見てみよう．型変数 a に入る型は，右側のに現れない．つまり，型変数 a に何が入ろうが Message の内部表現が ByteString であることに変わりはない．このような振る舞いをする型変数を幽霊型 (Phantom type)と呼ぶ．これはこの論文で作られた造語である．論文ではEDSLに静的な型をつけることで，静的に書いた言語の正当性をある程度保証している．
ここでは型変数のことを幽霊型，型変数に入る型のこと型タグとする．

データ型の昇格
 type2.hs の Message の実装には問題がある．それは期待されない型が型タグとして扱えてしまうことである．つまり， Message Int は，上記の実装では合法である．我々は， Message の型タグとして， Plain と Encrypted のみを期待しているので，これら以外を受け取らないように制限したい．素朴な考えとして， Message の型変数 a に型の型のようなもので注釈をつけられるとよさそうである．そのようなものは種(kind)と呼ばれている．
Haskellではデフォルトでは引数のない型コンストラクタを表す * と，関数型の種バージョンの k1 -> k2 といった形のものと，制約を表す Constraint 種しか存在しないが，GHC拡張にはデータ型を種へ，値コンストラクタを型へ昇格する DataKinds という拡張がある．これを使えば，種と，その種を持つ型を定義することができる．
type4.hs
	{-# LANGUAGE DataKinds #-}
	data Status = Plain | Encrypted
	  deriving (Show, Eq)
この時， Status 種を持つ型， Plain ， Encrypted と Status 型を持つ値， Plain ， Encrypted の2つが生成される．ここで注意すべきは，この2つの間になんの関連性も無いことである．型 Plain ， Encrypted は対応する値コンストラクタは存在しない．つまり，値 Plain を使っても型 Plain を作ることはできない．これら2つが生成されるため，型コンストラクタと値コンストラクタを同じ名前にするというHaskellの悪しき風習に従ってデータ型を定義した場合，昇格された値コンストラクタと，元の型コンストラクタがだぶる．この場合，昇格された値コンストラクタの先頭に ' をつけることで区別することができる(e. g.  'Plain )．(昇格された値コンストラクタに ' ついていない場合，GHCはwarningを吐く)

これでユーザ定義された制限された種を作ることができた．後は Message の型変数 a に種注釈をつければよい．デフォルトではこのような注釈はできないが，GHC拡張の KindSignatures を有効にすれば可能になる．
最終的に定義はこうなる．
type5.hs
	{-# LANGUAGE DataKinds      #-}
	{-# LANGUAGE KindSignatures #-}
	 
	data Status = Plain | Encrypted
	  deriving (Show, Eq)
	newtype Message (a :: Status) = Message ByteString
	  deriving (Show, Eq)
こうすれば， Message Int のような型はコンパイル時に弾かれるようになる．

存在型
複数の Message を Vector に格納することを考えよう．残念ながら Vector には同じ型のものしかいれることができないため， Message Plain と Message Excrypted を一緒に Vector に入れることはできない．そこで，この2つの Message 型を同一の型として扱うことができないだろうか？こういった要求に答えるのが存在型である．
type6.hs
	{-# LANGUAGE ExistentialQuantification #-}
	{-# LANGUAGE FlexibleContexts          #-}
	 
	data SomeMessage = forall a. Show (Message a) => SM (Message a)  -- 存在型
	 
	hoge :: Vector SomeMessage -> Vector Bool
	hoge = ...
 SomeMessage が存在型である．ここで注目すべきは，幽霊型の時は逆に，右辺の型変数 a が左辺に現れないことである．この型変数を存在量化された型変数と呼び，この型変数により内部表現が変わろうとも型が変わらないということ表している．型変数を存在量化するには forall キーワードを使って， forall a b.  といったようにする必要がある．
普通，存在型にはコンテキスト(型クラス制約)が含まれる．というのも，パターンマッチして存在型の中の値を取り出したとき，型の情報は失われているので何もできない．しかし， SomeMessage の例のようにコンテキストも一緒に存在型の中に入れておけば，存在型の中の型がどのようなことができるかの情報が残り，コンテキストにある型クラスのメソッドと，それらをつかった多相な関数が扱えるようになる．
存在型は非常に有用だが，パフォーマンスがよろしくない．基本的にコンテキストも中に含めるうえ，中の型の情報も外に露出しないため，型クラスの特殊化の恩恵を受けることができず要出典，辞書渡しのオーバーヘッドがかかる．何回も存在型のパターンマッチが行われる今回のようなプログラムは書くべきではないだろう(荒業として，型で諸々保証してパターンマッチをせずに unsafeCoerce でｶﾞｯとやるなども使われたりする． MagicDict を参照せよ)．

高階Kind多相
存在型の節で，パターンマッチしても型の情報が失われているので何もできないといったがちょっとまってほしい， id のような中の型に依存しないような関数であれば(意味があるかはおいておいて)適用できるのではなかろうか．次のような関数を書いてみよう．
type7.hs
	foo :: (a -> b) -> SomeMessage -> b
	foo f (SM x) = f x
試してみるとわかるが，この関数は残念ながらコンパイルできない．というのも，ここでの型変数 a や b はこの関数の呼び出しのときに具体化されてしまうので， f :: a -> b は真に任意の型を受け入れられる関数ではないためである．真に多相な型変数を書く手段として， RankNTypes 拡張がある．これを使うと， type7.hs は以下のようになる．
type8.hs
	foo :: (forall a. a -> b) -> SomeMessage -> b
	foo f (SM x) = f x
このように書くと，型変数 a のスコープはかっこの中に限定される．つまり，型変数 a は関数の外に影響を受けないことが保証されるため，関数 f の引数は多相的であることが強いられる．これによって，任意の型を引数に取る多相な関数を表現することができる．
通常こちらも存在型と同様にこれだけでは意味があまりないので，コンテキストこみで扱われることが多い．

依存型
事前条件や事後条件を型として表す際，値に依存する場合がある．有名な例としては，長さ付き配列がある．長さ付き配列において，型は配列の長さによって変わりうる．このように値によって変わるような型を依存型と呼ぶ．
Haskellでは(フルの)依存型をサポートしていないが，データ型の昇格と型族，singleton typeなどなどを使うことでがんばれば依存型の機能の一部をエミュレートすることができる．
詳しくは #依存型と型族 で話すことにする．