-XEmptyDataDeclsフラグ(または同等のLANGUAGEプラグマ)が指定されていると、構築子なしでデータ型を宣言できるようになる。例えば、以下のようにである。
data S -- S :: * data T a -- T :: * -> *
構文的にいうと、この宣言は「= constrs」の部分を欠いている。このように定義される型は多相的でも良く、さらにどのような種について多相的でも良いが、種が*でないなら、明示的な種注釈を使う必要がある。(7.13.5. 明示的に種付けされた量化を見よ)
このようなデータ型はボトムというただ一つの値しか持たないが、「幽霊型(phantom type)」を定義するときには便利なことがある。
Haskellは、データ型に文脈を与えることを許している。例えば以下のように。
data Eq a => Set a = NilSet | ConsSet a (Set a)
これは、以下の型を持つ構築子を与える。
NilSet :: Set a ConsSet :: Eq a => a -> Set a -> Set a
これはまずい機能だと広く考えられており、言語から削除される予定である。GHCでは、この機能はDatatypeContextsという非推奨の拡張で制御される。
GHCでは、型構築子、クラス、型変数を演算子として定義し、式と同じように中置記法で書くことが許される。具体的には、以下のようにである。
型構築子やクラスは、コロンで始まる演算子であっても良い。例えば:*:。字句的な構文はデータ構築子の場合と同じである。
データ型と型シノニムの宣言は中置形でも行える。引数がさらに必要なら括弧を使う。例。
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
バッククオートは、型構築子と型変数のどちらについても、式の場合と同様に働く。例えば、Int `Either` BoolとかInt `a` Boolのように書ける。同様に、括弧も同じように働く。例えば、(:*:) Int Boolのようにである。
型構築子やクラスについて、データ構築子の場合と同じように結合性を宣言することができる。しかし、結合性宣言中でこの二つを区別することはできない。一つの結合性宣言で、データ構築子の結合性と型構築子の結合性が同時に設定される。
infixl 7 T, :*:
上記は、型構築子Tとデータ構築子Tの両方の結合性を設定している。:*:についても同様である。Int `a` Bool.
関数の矢印はinfixrで結合性0である。(これは変わるかもしれない。どうするべきかわからないので)
通常、型の中では、(+)のような演算子記号はaと同じような型変数として扱われる。よって、Haskell 98では次のように書ける。
type T (+) = ((+), (+)) -- これと同じ: type T a = (a,a) f :: T Int -> Int f (x,y)= x
見ての通り、演算子をこのように使えてもあまり便利でなく、さらにHaskell 98はこれらを中置形で書くことすら許さない。
-XTypeOperators言語はこの振る舞いを変える。
演算子記号は型変数でなく型構築子になる。
型としての演算子記号は、定義と使用の両方で中置形で書ける。例えば、
data a + b = Plus a b type Foo = Int + Bool
これによって、インポートリストとエクスポートリストにおいて曖昧性が発生し得る。例えば、import M( (+) )と書いた場合、これは(+)という関数のことなのか、それとも(+)という型構築子のことなのだろうか。デフォルトは前者であるが、-XExplicitNamespaces(これは-XExplicitTypeOperatorsによって自動的に有効になる)を有効にすると、GHCは後者を、typeというキーワードを前置することで表わせるようにする。次のように。
import M( type (+) )
型演算子の結合性は通常の結合性宣言で設定できるが、7.4.3. 中置型構築子、中置クラス、中置型変数と同様に、関数と型構築子は同じ結合性を共有する。
型シノニムは型の世界でのマクロに似ているが、Haskell 98は型シノニムの個々の宣言にたくさんの規則を課している。拡張-XLiberalTypeSynonymsが有効だと、GHCはいろいろな検査を型シノニムを展開した後にしか行わない。つまり、型シノニムについてGHCはHaskell 98よりもずっと制限を緩くすることができる。
次のように、型シノニム中に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]
GHCは現在、型シノニムを展開する前に種検査を行っている。(ただしこれも変えることはできるだろう)
型シノニムを展開した後、GHCは、以下のような、種検査では発見できない誤りを見つけるために、型に対して妥当性検査を行う。
型構築子がforall付きの型に適用されている。(XImpredicativeTypesが無効の場合)
部分適用された型シノニムがある。
従って、例えば、以下のものは拒絶される。
type Pr = forall a. a h :: [Pr] h = ...
これは、型構築子をforall付きの型に適用することをGHCが許していないからである。
データ型の宣言において存在量化を使うという考えはPerryによって提案され、Hope+に実装された。(Nigel Perry, The Implementation of Practical Functional Programming Languages, PhD Thesis, University of London, 1991)。数年の間Lennart AugustssonのhbcというHaskellコンパイラで利用でき、非常に便利なことが明らかになった。ここに考え方を示す。次のような宣言があったとしよう。
data Foo = forall a. MkFoo a (a -> Bool)
| Nil
データ型Fooは、次のような型を持つ二つの構築子を持っている。
MkFoo :: forall a. a -> (a -> Bool) -> Foo Nil :: Foo
MkFooの型において、型変数aがデータ型自体(ただのFooである)のなかに現れないことに注意せよ。例えば、以下の式は正しい。
[MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]
ここで、(MkFoo 3 even)は、一つの整数と、整数をBoolに写す関数evenを梱包しており、(MkFoo 'c' isUpper)は、一つの文字と、対応する関数を梱包している。これらはどちらもFoo型のものであり、一つのリストに入れることができる。
Foo型の値に対してできることは何だろうか？特に、MkFooに対してパターン照合を行うと何が起きるだろうか？
f (MkFoo val fn) = ???
ここで、valとfnについて判っているのは、valの型とfnの引数の型が同じだということだけなので、できることは(実質的に)fnをvalに適用して真偽値を得ることだけである。以下のように。
f :: Foo -> Bool f (MkFoo val fn) = fn val
結局できたことは、不特定の型の値を、それを操作するいくつかの関数と一緒に梱包して、梱包物の集まりを統一的に扱うことである。この方法で、オブジェクト指向っぽいプログラミングのかなりの部分を行うことができる。
これが存在量化とどう関係するのだろうか？これは単に、MkFooが以下の(ほぼ)同型な型を持っているというだけのことである。
MkFoo :: (exists a . (a, a -> Bool)) -> Foo
しかし、Haskellプログラマは上に挙げた通常の全称量化された型を考えれば十分である。こうすれば、存在量化のための構文要素を新しく加える必要がない。
簡単な拡張として、構築子の前に任意の文脈を置くことを可能にするというのがある。
data Baz = forall a. Eq a => Baz1 a a
| forall b. Show b => Baz2 b (b -> b)
これらの二つの構築子は、予想される通りの型を持つ。
Baz1 :: forall a. Eq a => a -> a -> Baz Baz2 :: forall b. Show b => b -> (b -> b) -> Baz
ただし、Baz1に関するパターン照合では、照合された値を等値比較できるし、Baz2に関するパターン照合では、照合された最初の値を文字列に変換することができる(関数を適用することもできる)。従って以下のプログラムは合法である。
f :: Baz -> String
f (Baz1 p q) | p == q = "Yes"
| otherwise = "No"
f (Baz2 v fn) = show (fn v)
操作的にいうと、辞書渡し式の実装では、構築子Baz1とBaz2はEqとShowの辞書をそれぞれ記憶しておかなければならず、パターン照合の時にはそれを展開する。
以下のように、存在量化とレコード構文を併用することができる。
data Counter a = forall self. NewCounter
{ _this :: self
, _inc :: self -> self
, _display :: self -> IO ()
, tag :: a
}
ここでtagは公開フィールドであり、正しく型のついた選択関数であるtag :: Counter a -> aが付属している。型selfは外部からは隠蔽されている。_this、_inc、_displayを関数として適用しようとするとコンパイル時エラーになる。言い替えると、GHCは、フィールドの型が、存在量化された型変数に言及していない場合に限り、そのフィールドへの選択関数を定義する。(この例では選択関数が定義されていないフィールドにアンダースコアを用いているが、これは単なるプログラミングの上での様式であり、GHCは関知しない)
これらの隠されたフィールドを利用するには、ヘルパ関数をいくつか作らないといけない。
inc :: Counter a -> Counter a
inc (NewCounter x i d t) = NewCounter
{ _this = i x, _inc = i, _display = d, tag = t }
display :: Counter a -> IO ()
display NewCounter{ _this = x, _display = d } = d x
ここで、異なる実装を持つ複数のカウンタを定義することができる。
counterA :: Counter String
counterA = NewCounter
{ _this = 0, _inc = (1+), _display = print, tag = "A" }
counterB :: Counter String
counterB = NewCounter
{ _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }
main = do
display (inc counterA) -- "1" と表示する
display (inc (inc counterB)) -- "##"と表示する
レコードの更新構文が存在的データ型(およびGADT)に対してサポートされている。
setTag :: Counter a -> a -> Counter a
setTag obj t = obj{ tag = t }
レコード更新についての規則はこうである。更新されるフィールドの型は、データ構築子の型変数のうち、全称量化されたものにしか言及してはならない。GADTについては、フィールドは、構築子の結果の型の中で単純な型変数引数として現れるものにしか言及してはならない。例を挙げる。
data T a b where { T1 { f1::a, f2::b, f3::(b,c) } :: T a b } -- cは存在的
upd1 t x = t { f1=x } -- 正: upd1 :: T a b -> a' -> T a' b
upd2 t x = t { f3=x } -- 誤 (f3の型はcに言及するが、これは存在量化されている)
data G a b where { G1 { g1::a, g2::c } :: G a [c] }
upd3 g x = g { g1=x } -- 正: upd3 :: G a b -> c -> G c b
upd4 g x = g { g2=x } -- 誤 (f2の型はcに言及するが、これはG1の結果の型において
-- 単純な型変数の形の引数でない)
存在量化された構築子を使う上で、何種類かの制約がある。
パターン照合では、個々の存在量化された型変数について、新しい、相互に異なる型が導入される。これらの型は他の型と単一化されることはなく、パターン照合のスコープの外に抜け出すこともできない。例えば、以下の断片は正しくない。
f1 (MkFoo a f) = a
ここでは、aがf1の結果なので、MkFooで束縛された型が「抜け出して(escape)」いる。なぜこれが間違っているか納得する方法の一つは、f1がどういう型を持つか問うことである。
f1 :: Foo -> a -- おかしい！
結果型の「a」とはなんだ？もちろん次のようなことを言いたい訳ではない。
f1 :: forall a. Foo -> a -- 間違い
これは、元のプログラムが間違っているというだけのことである。下記はまた別の種類の誤りである。
f2 (Baz1 a b) (Baz1 p q) = a==q
a==bとかp==qと言うのは構わないが、a==qは間違っている。二つのBaz1構築子に由来する異なった型を等値比較しているからである。
存在量化された構築子に関するパターン照合をletやwhereグループの束縛で行うことはできない。従って次は不正である。
f3 x = a==b where { Baz1 a b = x }
代わりに、case式を使うこと。
f3 x = case x of Baz1 a b -> a==b
一般に、存在量化された構築子についてパターン照合できるのは、case式においてと、関数定義のパターンにおいてのみである。この制約は実は実装上の理由による。束縛グループを型検査するのは既に悪夢であり、存在型はさらに問題をややこしくする。さらに、モジュールの最上位での存在的パターン束縛には意味がない。存在量化された型が抜け出すのを防ぐ方法がはっきりしないからである。このため、今のところ、述べやすい制約が科せられている。私はこの制約がどれくらい厄介か見定めているところである。
newtype宣言に存在量化を使うことはできない。よって以下は不正である。
newtype T = forall a. Ord a => MkT a
理由: Tの値はOrd tの辞書とt型の値の組で表現されねばならないが、これはnewtypeは具体的な表現形式を持つべきではないという考えに反する。newtypeの代わりにdataを使うことで、全く同じ効果・効率を得ることができる。多重定義が関係しないときは、存在量化されたnewtypeを許す根拠がある。代わりにdataを使うと実際に実装コストが掛かるからである。しかし、単一フィールドの存在量化構築子はあまり使い道がない。このため、何か説得力のある理由がない限り、この単純な制約(newtypeでは存在的なもの禁止)が有効である。
derivingを使って、存在量化されたデータ構築子のあるデータ型のインスタンスを定義することはできない。 理由: 大抵の場合、これは意味をなさない。例。
data T = forall a. MkT [a] deriving( Eq )
標準的な方法でEqを導出するには、二つのMkT構築子の内容を等値比較する必要がある。
instance Eq T where (MkT a) == (MkT b) = ???
しかしaとbの型は異なるので、比較することができない。導出されたインスタンスが意味をなすような例を考えることも不可能ではないが、このような宣言をまとめて禁止した方が単純だと考えられる。自分でインスタンスを定義しましょう！
GADTSyntax拡張が有効な場合、GHCは、構築子の型シグネチャを明示的に与えることで代数的データ型を宣言することを許す。例えば、次のように。
data Maybe a where
Nothing :: Maybe a
Just :: a -> Maybe a
この形式は「GADT様式の宣言」と呼ばれる。これは、一般化代数データ型(7.4.8. 一般化代数データ型(GADT)に記述がある)が、この形式でしか宣言できないからである。
GADT様式の構文は存在型(7.4.6. 存在量化されたデータ構築子 )の一般化になっていることに注意。例えば、以下の二つの宣言は同等である。
data Foo = forall a. MkFoo a (a -> Bool)
data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }
標準のHaskell-98の構文で宣言できるデータ型は全てGADT様式でも宣言できる。どちらを選ぶかは大部分スタイルの問題だが、GADT様式の宣言が通常と異なる重要な点が一つある。データ構築子に関するクラス制約の扱いが異なるのである。具体的に言うと、構築子に型クラス文脈が与えられたとき、パターン照合によってその文脈が使えるようになる。例を示す。
data Set a where
MkSet :: Eq a => [a] -> Set a
makeSet :: Eq a => [a] -> Set a
makeSet xs = MkSet (nub xs)
insert :: a -> Set a -> Set a
insert a (MkSet as) | a `elem` as = MkSet as
| otherwise = MkSet (a:as)
mkSetを構築子として使う(例えばmakeSetの定義)と、期待通り(Eq a)の制約が生じる。新機能は、MkSetについてのパターン照合(insertの定義にあるようなもの)の際、文脈(Eq a)が使えるようになるということである。実装の言葉で言うと、MkSetには、渡された(Eq a)の辞書を持っておくための隠れたフィールドがある。それで、パターン照合の際には、照合の右辺からその辞書を使うことができる。この例では、こうして得られたEqの辞書を、elemの呼び出しによって生成されたEq制約を満足させるのに使うので、insertの型自体にはEq制約が現れない。
例えば、応用の一つとして、辞書をオブジェクト化するというのがある。
data NumInst a where MkNumInst :: Num a => NumInst a intInst :: NumInst Int intInst = MkNumInst plus :: NumInst a -> a -> a -> a plus MkNumInst p q = p + q
ここで、NumInst a型の値は、(Num a)の辞書を明示的にしたものと同等である。
これは全て、7.4.6.2. 存在型と型クラスの構文を使って宣言された構築子についても当てはまる。例えば、上のデータ型NumInstは次のように定義しても同等である。
data NumInst a = Num a => MkNumInst (NumInst a)
存在型を定義する場合と違ってforallがないことに注意。これは、Numが、データ型の全称量化された型変数aを制約するからである。ひとつの構築子に、全称と存在の両方の型変数があってもよい。例えば、以下の二つの宣言は同等である。
data T1 a = forall b. (Num a, Eq b) => MkT1 a b data T2 a where MkT2 :: (Num a, Eq b) => a -> b -> T2 a
これらの振る舞いは全て、Haskell 98の、データ型宣言における文脈の奇妙な扱い(Haskell 98レポートの4.2.1節)と対照を為す。Haskell 98では、次の定義によって、上のMkSetと同じ型のMkSet'が得られる。
data Eq a => Set' a = MkSet' [a]
しかし、MkSet'についてのパターン照合では、(Eq a)の制約が使えるようになるのでなく、(Eq a)の制約を要求するのだ。変な振る舞いだが、GHCはこれを忠実に実装している。しかし、GADT様式の宣言なら、GHCの振る舞いはずっと有用で、同時にずっと直感的である。
この節の残りの部分では、GADT様式のデータ型宣言について、さらなる詳細を与える。
各データ構築子の結果の型は、定義しようとしている型構築子で始まっていなければならない。構築子の結果の型が全てT a1 ... anという形(ただしa1 .. anは相異なる型変数)なら、それは通常のデータ型であり、そうでなければ一般化されたデータ型(7.4.8. 一般化代数データ型(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.6. 存在量化されたデータ構築子 の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.6.3. レコード構築子)と同様に、レコード選択関数は、選択関数にうまく型が付くフィールドについてのみ生成される。以下は、存在的レコードの節の例をGADT様式にしたものである。
data Counter a where
NewCounter :: { _this :: self
, _inc :: self -> self
, _display :: self -> IO ()
, tag :: a
} -> Counter a
前と同じように、ここで生成される選択関数は唯一つ、tagについてものである。ただし、パターン照合とレコード構築では、相変わらず全てのフィールド名を使うことができる。
GADT様式のデータ型宣言では、データ構築子が中置であるかを指定する自明な方法が存在しない。これはその型にShowを自動導出する際に問題になる。(中置で宣言されたデータ構築子はshowによって中置で表示される。)そこでGHCは以下の設計を実装している。GADT様式で宣言されたデータ構築子がShowによって中置で表示されるのは、(a)演算子記号であり、(b)引数を二つ取り、(c)プログラマによって与えられた結合性宣言を持つ、場合、かつそれに限る。例を挙げる。
infix 6 (:--:) data T a where (:--:) :: Int -> Bool -> T Int
一般化代数データ型は、通常の代数的データ型を拡張して、構築子がより多様な型を持てるようにしたものである。以下は例である。
data Term a where
Lit :: Int -> Term Int
Succ :: Term Int -> Term Int
IsZero :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
Pair :: Term a -> Term b -> Term (a,b)
通常のデータ型の場合と違って、構築子の結果の型がTerm aだとは限らないことに注意。この一般化のお陰で、Termについて、正しく型の付いたeval関数を書くことができる。
eval :: Term a -> a eval (Lit i) = i eval (Succ t) = 1 + eval t eval (IsZero t) = eval t == 0 eval (If b e1 e2) = if eval b then eval e1 else eval e2 eval (Pair e1 e2) = (eval e1, eval e2)
GADTの鍵となる点は、パターン照合によって型の精密化が起こることである。以下の例を考える。
eval :: Term a -> a eval (Lit i) = ...
等式の右辺では、aが精密化されてIntになる。これこそが売りである。型付け規則の正確な規定は利用の手引きが目指すところではないが、設計は、Simple unification-based type inference for GADTs, (ICFP 2006)で述べられているものによく倣っている。 一般的な原則はこうである。精密化は、ユーザ供給の型注釈を基にしてのみ起こる。従って、もしevalに型シグネチャが与えられなければ、型精密化は起こらず、大量の不明瞭なエラーが発生することだろう。一方、精密化はかなり一般的である。例えば、以下のものがあったとしよう。
eval :: Term a -> a -> a eval (Lit i) j = i+j
このパターン照合で、型aが精密化されて(構築子Litの型にしたがって)Intになる。この精密化はjの型とこのcase式の結果の型にも及ぶ。だからi+jという加算は合法である。
これらの例と、他の多くの例が、Hongwei XiとTim Sheardによる論文群で与えられている。wikiにはもっと長い入門文書があるし、Ralf HinzeのFun with phantom typesにもいくつか例がある。 これらの論文ではGHCに実装されているのと異なる記法を使っていることがあるので注意。
この節の残りの部分では、GADTをサポートするGHCの拡張について概観する。この拡張は-XGADTsで有効になる。-XGADTsフラグを使うと、-XRelaxedPolyRecも同時に設定される。
GADTは、GADT様式の構文(7.4.7. 構築子のシグネチャを明示してデータ型を宣言する)でなければ宣言できない。Haskell 98の古いデータ宣言の構文では、常に通常のデータ型が宣言される。各構築子の結果の型は定義しようとしている型構築子で始まっていなければならないが、GADTについては、その型への引数は任意のmonotypeで良い。例えば、上のTerm型において、各構築子の型はTerm tyで終わっていなければならないが、tyが型変数である必要はない。(例えば構築子Lit)。
GADT様式の構文を使って通常の代数的データ型を宣言することは可能である。GADTをGADTたらしめるのは構文ではなく、結果の型が単なるT a bでないような構築子の存在である。
GADTについてderiving節を使うことはできない。通常のデータ型だけである。
7.4.7. 構築子のシグネチャを明示してデータ型を宣言するで述べたように、レコード記法にも対応している。例えば以下のように。
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式で)場合、以下の規則が適用される。
検査対象(訳注: scrutinee; case式ならcaseとinの間に書かれる式のこと)の型は固い型でなければならない。
case式全体の型は固い型でなければならない。
caseの各分岐で言及される自由変数の型はすべて固い型でなければならない。
型が「固い(rigid)」というのは、それが束縛された地点において、コンパイラにとって完全に既知であることをいう。ある変数の型が固い型であることを確実にしたいなら、もっとも簡単な方法はそれに型シグネチャを与えることである。より精密な詳細についてはSimple unification-based type inference for GADTsを見よ。GHCに実装されている基準はAppendixに載っている。