ゆうれい，いぞん，そんざい，ﾗｧｩﾝｸﾄｩｩﾎﾟﾘﾓｫﾌｨｼﾞｩﾑｯ
我々が型をつけるとき，基本的に型はある種の条件を表すものとして扱うことが多い．例えば，Intであれば値は整数であるという条件だし，Num a => aであればNumクラスのインスタンスである型aという条件を表している．
であるならば，プログラム上の様々な条件を型にしたいのは静的型付き言語を扱うプログラマにとって自然な欲求であろう．
GHCはこういった欲求に答えるため様々な型ハックをサポートしている．ここではそういった型ハックの一部を扱うことにする．
型タグ
事前条件と事後条件が型でわかるようにしたいとする．たとえば，暗号化を考えてみよう．暗号化する前と暗号化した後を型で区別したいというのは自然な発想だろう．そういった場合，一番最初にたどり着く発想は単純にnewtypeで同じ内部表現を持つ別の型にしてしまうことである．(以下の例は拝借したもの)(拝借元を忘れる1敗)
code: type1.hs
newtype Plain = Plain ByteString
deriving (Show, Eq)
newtype Encrypted = Encrypted ByteString
deriving (Show, Eq)
encrypt :: Plain -> Encrypted
encrypt m = ...
こうすれば，暗号化済みの値を取るべきところに間違って暗号化前の値を突っ込んでしまったりしても，コンパイルエラーが起きる．しかし，この方法ではPlain, Encrypted両方を受け取るような関数を作る場合，型クラスを持ち出す必要がある．内部表現は一致しているのに型を合わせるためだけに型クラスを持ち出すのはいささか面倒である．
そこで，もう一つの本質的に同じ方法として，型タグを使った方法がある．
code: 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がパラメトリックなため，わざわざ型クラスを実装する必要ない．
code: 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という拡張がある．これを使えば，種と，その種を持つ型を定義することができる．
code: 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を有効にすれば可能になる．
最終的に定義はこうなる．
code: 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型を同一の型として扱うことができないだろうか？こういった要求に答えるのが存在型である．
code: 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のような中の型に依存しないような関数であれば(意味があるかはおいておいて)適用できるのではなかろうか．次のような関数を書いてみよう．
code: type7.hs
foo :: (a -> b) -> SomeMessage -> b
foo f (SM x) = f x
試してみるとわかるが，この関数は残念ながらコンパイルできない．というのも，ここでの型変数aやbはこの関数の呼び出しのときに具体化されてしまうので，f :: a -> bは真に任意の型を受け入れられる関数ではないためである．真に多相な型変数を書く手段として，RankNTypes拡張がある．これを使うと，type7.hsは以下のようになる．
code: type8.hs
foo :: (forall a. a -> b) -> SomeMessage -> b
foo f (SM x) = f x
このように書くと，型変数aのスコープはかっこの中に限定される．つまり，型変数aは関数の外に影響を受けないことが保証されるため，関数fの引数は多相的であることが強いられる．これによって，任意の型を引数に取る多相な関数を表現することができる．
通常こちらも存在型と同様にこれだけでは意味があまりないので，コンテキストこみで扱われることが多い．
依存型
事前条件や事後条件を型として表す際，値に依存する場合がある．有名な例としては，長さ付き配列がある．長さ付き配列において，型は配列の長さによって変わりうる．このように値によって変わるような型を依存型と呼ぶ．
Haskellでは(フルの)依存型をサポートしていないが，データ型の昇格と型族，singleton typeなどなどを使うことでがんばれば依存型の機能の一部をエミュレートすることができる．