型構築子やクラスは、コロンで始まる演算子であっても良い。例えば:*:。字句的な構文はデータ構築子の場合と同じである。

データ型と型シノニムの宣言は中置形でも行える。引数がさらに必要なら括弧を使う。例。

  data a :*: b = Foo a b
  type a :+: b = Either a b
  class a :=: b where ...

  data (a :**: b) x = Baz a b x
  type (a :++: b) y = Either (a,b) y

型およびクラス制約は中置形で書いても良い。

	x :: Int :*: Bool
        f :: (a :=: b) => a -> b
  

型変数は(修飾されていない)演算子であっても良い。例えば+などである。字句構文は変数演算子の場合と同じであるが、「(.)」、「(!)」、「(*)」は除外される。束縛位置では、演算子は括弧で括らねばならない。以下のように。

   type T (+) = Int + Int
   f :: T Either
   f = Left 3
 
   liftA2 :: Arrow (~>)
	  => (a -> b -> c) -> (e ~> a) -> (e ~> b) -> (e ~> c)
   liftA2 = ...

バッククオートは、型構築子と型変数のどちらについても、式の場合と同様に働く。例えば、Int `Either` BoolとかInt `a` Boolのように書ける。同様に、括弧も同じように働く。例えば、(:*:) Int Boolのようにである。

型構築子やクラスについて、データ構築子の場合と同じように結合性を宣言することができる。しかし、結合性宣言中でこの二つを区別することはできない。一つの結合性宣言で、データ構築子の結合性と型構築子の結合性が同時に設定される。

  infixl 7 T, :*:

上記は、型構築子Tとデータ構築子Tの両方の結合性を設定している。:*:についても同様である。Int `a` Bool.

関数の矢印はinfixrで結合性0である。(これは変わるかもしれない。どうするべきかわからないので)

次のように、型シノニム中にforall(多重定義が関係しても良い)を書くことができる。

  type Discard a = forall b. Show b => a -> b -> (a, String)

  f :: Discard a
  f x y = (x, show y)

  g :: Discard Int -> (Int,String)    -- ランク2の型
  g f = f 3 True

-XUnboxedTuplesも使っているなら、型シノニム中に非ボックス化型を書くことができる。

  type Pr = (# Int, Int #)

  h :: Int -> Pr
  h x = (# x, x #)

型シノニムをforall型に適用できる。

  type Foo a = a -> a -> Bool
 
  f :: Foo (forall b. b->b)

この型シノニムを展開すると、fの型は(GHCでは)合法なものになる。

  f :: (forall b. b->b) -> (forall b. b->b) -> Bool

部分適用された型シノニムに型シノニムを適用することができる。

  type Generic i o = forall x. i x -> o x
  type Id x = x
  
  foo :: Generic Id []

この型シノニムを展開すると、fooの型は(GHCでは)合法なものになる。

  foo :: forall x. x -> [x]

型構築子がforall付きの型に適用されている。

矢印の左側に非ボックス化タプルがある。

部分適用された型シノニムがある。

各データ構築子の結果の型は、定義しようとしている型構築子で始まっていなければならない。構築子の結果の型が全てT a1 ... anという形(ただしa1 .. anは相異なる型変数)なら、それは通常のデータ型であり、そうでなければ一般化されたデータ型(7.4.7. 一般化代数データ型(GADT))である。

通常の型シグネチャの場合と同様、複数の構築子に一つのシグネチャを与えることができる。この例では、T1とT2に一つのシグネチャを与えている。

  data T a where
    T1,T2 :: a -> T a
    T3 :: T a

それぞれの構築子の型シグネチャは独立していて、通常通り暗黙に全称量化される。特に、「data T a where」のような頭部にある型変数にはスコープがなく、別々の構築子には異なる全称量化の型変数があっても良い。

  data T a where        -- この「a」にはスコープがない
    T1,T2 :: b -> T b   -- 意味は forall b. b -> T b
    T3 :: T a           -- 意味は forall a. T a

構築子のシグネチャは型クラス制約に言及してもよいし、それが構築子間で異なっていてもよい。例えば、これは問題ない。

  data T a where
    T1 :: Eq b => b -> b -> T b
    T2 :: (Show c, Ix c) => c -> [c] -> T c

パターン照合の際には、照合の本体における制約を果たす(discharge)ために、これらの制約が利用できるようになる。例を挙げる。

  f :: T a -> String
  f (T1 x y) | x==y      = "yes"
             | otherwise = "no"
  f (T2 a b)             = show a

fは多重定義されていないことに注意。==を使用したことから発生したEq制約は、T1上のパターン照合によって果たされている。showを使用したことから発生したShow制約についても同様である。

Haskell 98様式のデータ型宣言と異なり、「data Set a where」というヘッダに出てくる型変数にはスコープがない。実際、代わりに類シグネチャを書くこともできる。

  data Set :: * -> * where ...

あるいは、この二つを混ぜるのでも良い。

  data Bar a :: (* -> *) -> * where ...

型変数(与えられるなら)は明示的に類付けされていても良いので、Fooのヘッダを以下のように書くこともできる。

  data Bar a (b :: * -> *) where ...

正確性注釈は、構築子の型の中の当然の場所に付けることができる。

  data Term a where
      Lit    :: !Int -> Term Int
      If     :: Term Bool -> !(Term a) -> !(Term a) -> Term a
      Pair   :: Term a -> Term b -> Term (a,b)

GADT様式のデータ型宣言でderiving節を使うことができる。例えば、以下の二つの宣言は同等である。

  data Maybe1 a where {
      Nothing1 :: Maybe1 a ;
      Just1    :: a -> Maybe1 a
    } deriving( Eq, Ord )

  data Maybe2 a = Nothing2 | Just2 a 
       deriving( Eq, Ord )

型シグネチャには、結果の型に現れない型変数があってもよい。

  data Foo where
     MkFoo :: a -> (a->Bool) -> Foo
     Nil   :: Foo

ここで、型変数aはどちらの構築子の結果の型にも現れない。構築子の型において全称量化されているが、こういう型変数はよく「存在的」であると言われる。実際、上の宣言は、7.4.5. 存在量化されたデータ構築子 のdata Fooと全く同じ型を宣言している。

もちろん、その型にクラス文脈が含まれていてもよい。

  data Showable where
    MkShowable :: Show a => a -> Showable

GADT様式のデータ型宣言においてレコード構文を使うこともできる。

  data Person where
      Adult :: { name :: String, children :: [Person] } -> Person
      Child :: Show a => { name :: !String, funny :: a } -> Person

通常と同じように、fというフィールドを持つ全ての構築子に関して、フィールドfの型が(α変換を法として)等しくなければならない。上記のChild構築子を見ると分かるとおり、シグネチャには、レコードでない場合と同様に、文脈、存在量化された変数、正格性注釈があってもよい。(注意: 二つのコロンの後にある「型」は、レコード構文と正格性注釈を含むので正確には「型」でない。この形の「型」は構築子のシグネチャにのみ現れることができる。)

レコード更新は、以下の性質を持つフィールドについてのみ、GADT様式の宣言でも許される。「そのフィールドの型が存在的な型変数に言及しないこと」

Haskell 98風のレコード構文で存在型を宣言する場合(7.4.5.3. レコード構築子)と同様に、レコード選択関数は、選択関数にうまく型が付くフィールドについてのみ生成される。以下は、存在的レコードの節の例をGADT様式にしたものである。

data Counter a where
    NewCounter { _this    :: self
               , _inc     :: self -> self
               , _display :: self -> IO ()
               , tag      :: a
               }
        :: Counter a

前と同じように、ここで生成される選択関数は唯一つ、tagについてものである。ただし、パターン照合とレコード構築では、相変わらず全てのフィールド名を使うことができる。

GADTは、GADT様式の構文(7.4.6. 構築子のシグネチャを明示してデータ型を宣言する)でなければ宣言できない。Haskell 98の古いデータ宣言の構文では、常に通常のデータ型が宣言される。各構築子の結果の型は定義しようとしている型構築子で始まっていなければならないが、GADTについては、その型への引数は任意のmonotypeで良い。例えば、上のTerm型において、各構築子の型はTerm tyで終わっていなければならないが、tyが型変数である必要はない。(例えば構築子Lit)。

GADT様式の構文を使って通常の代数的データ型を宣言することは可能である。GADTをGADTたらしめるのは構文ではなく、結果の型が単なるT a bでないような構築子の存在である。

GADTについてderiving節を使うことはできない。通常のデータ型だけである。

7.4.6. 構築子のシグネチャを明示してデータ型を宣言するで述べたように、レコード記法にも対応している。例えば以下のように。

  data Term a where
      Lit    { val  :: Int }      :: Term Int
      Succ   { num  :: Term Int } :: Term Int
      Pred   { num  :: Term Int } :: Term Int
      IsZero { arg  :: Term Int } :: Term Bool	
      Pair   { arg1 :: Term a
             , arg2 :: Term b
             }                    :: Term (a,b)
      If     { cnd  :: Term Bool
             , tru  :: Term a
             , fls  :: Term a
             }                    :: Term a

ただし、GADTについては以下の制約が追加される。フィールドfを持つ全ての構築子は、(α変換を法として)同じ結果型を持たねばならない。だから、上の例なら、numフィールドとargフィールドをまとめて一つの名前にすることはできない。フィールド型はどちらもTerm Intだが、実は選択関数は異なる型を持っている。

  num :: Term Int -> Term Int
  arg :: Term Bool -> Term Int

GADTから得られたデータ構築子に対してパターン照合を行なう(例えばcase式で)場合、以下の規則が適用される。

型が「固い(rigid)」というのは、それが束縛された地点において、コンパイラにとって完全に既知であることをいう。ある変数の型が固い型であることを確実にしたいなら、もっとも簡単な方法はそれに型シグネチャを与えることである。より精密な詳細についてはSimple unification-based type inference for GADTsを見よ。GHCに実装されている基準はAppendixに載っている。