データ型と型シノニムの拡張(和訳)
コンストラクタなしのデータ型
EmptyDataDecls
6.8.1以降
空のデータ型の定義を許可する.
EmptyDataDecls拡張を有効にすると,コンストラクタを持たないデータ型を宣言することができる.
code: data1.hs
data S -- S :: Type
data T -- T :: Type -> Type
構文的には,宣言にはコンストラクタの部分がない.型はどのような種類の型に対してもパラメータ化できるが,その種がTypeではない場合は,明示的な種注釈をする必要がある(明示的に量化された種を参照せよ).
このようなデータ型には1つの値,つまりボトムしかない.それでも,それらは「幽霊型」を定義するときに役立つ.
-XEmptyDataDeriving拡張機能と組み合わせて,空のデータ宣言で標準型クラスのインスタンスを派生させることもできる(空のデータ型のインスタンスの導出を参照せよ).
データ型コンテキスト
DatatypeContexts
7.0.1以降
dataによる宣言でのコンテキストを許可する.
Haskellではデータ型にコンテキストを与えることができる.例えば,
code: data2.hs
data Eq a => Set a = NilSet | ConsSet a (Set a)
のような宣言をした場合,値コンストラクタの方は次のようになる.
code: data3.hs
NilSet :: Set a
ConsSet :: Eq a => a -> Set a -> Set a
これは一般に誤った機能と見なされ,言語仕様から削除される予定である.GHCでは,これは廃止予定のDatatypeContexts拡張によって制御される.
中置型コンストラクタ,型クラス,型変数
GHCでは,式のように,型コンストラクタ,型クラス,型変数を演算子にし,中置にしたりすることができる.すなわち:
型コンストラクタまたは型クラスは,予約されていない任意の演算子にできる.型で使用される記号は常に大文字の識別子のようなもので,それらは決して変数ではない.これは:から始まることが必要とされる値コンストラクタの字句構文とは異なることに注意すること.
データ型と型の同義語の宣言は追加の引数が必要な場合は括弧付きで中置で書くことができる.例えば
code: data4.hs
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
型と型クラス制約は,中置で書くことができる.例えば
code: data5.hs
x :: Int :*: Bool
f :: (a :=: b) => a -> b
バッククォートは型コンストラクタと型変数の両方に対して式と同様に機能する.例:Int \`Either\` Bool,Int \`a\` Bool.同様に,括弧も同じように機能する.例:(:*:) Int Bool.
値コンストラクタと同じように型コンストラクタまたは型クラスに対してinfixを宣言することができる.ただし,infix宣言でこの2つを区別することはできない.infix宣言は,値コンストラクタと対応する型コンストラクタのinfixを設定する.例えば:
code: data6.hs
infixl 7 T, :*:
型コンストラクタTと値コンストラクタTの両方に対して,また同様に:*:. Int \`a\` Boolに対してinfixを設定する.
->はinfixr 0である.(これは変わるかも.どうあるべきかはっきりしていない).
型演算子
TypeOperators
ExplicitNameSpacesを含む
6.8.1以降
演算子名を持つ型の使用と定義を許可する.
型では,(+)のような演算子記号は,通常,aと同様に型変数として扱われる.したがってHaskell 98では,次のようになる.
code: data7.hs
type T (+) = ((+), (+))
-- Just like: type T a = (a, a)
f :: T Int -> Int
f (x, y) = x
ご覧のとおり、このように演算子を使用することはあまり便利ではない.またHaskell 98では,中置文字を書くことさえできない.
TypeOperators拡張はこの動作を変更する.
演算子記号は型変数ではなく型コンストラクタになる.
型の中の演算子記号は,定義と使用の両方で、中置で書くことができる.例えば:
code: data8.hs
data a + b = Plus a b
type Foo = Int + Bool
インポートリストとエクスポートリストには、あいまいさが生じる可能性がある.たとえば,import M((+))と書くと, 関数(+)と型コンストラクタ (+)のどちらを意味するかわからない.デフォルトは前者を表すが,ExplicitNameSpaces(TypeOperatorsで暗黙的に有効になる)では,GHCではキーワードtypeを前に付けることで後者を指定できる.
code: data9.hs
import M( type (+) )
型演算子のinfixは,通常のinfix宣言を使用して設定できるが,中置型コンストラクタ,型クラス,型変数の場合と同様に,関数と型コンストラクタは単一のInfixを共有する.
自由化された型シノニム
LiberalTypeSynonyms
ExplicitForAllを含む.
6.8.1以降
型シノニムの定義に関するHaskell 98の規則の多くを緩和する.
型シノニムは型レベルではマクロに似ているが,Haskell 98は個々の型シノニム宣言に多くの規則を課している. LiberalTypeSynonyms拡張では,型シノニムを展開した後初めて,GHCは型検査を行う.つまり,GHCはHaskell 98よりも型シノニムについて非常に自由度が高い.
型シノニムでforall(多重定義を含む)を書くことができる.
code: data10.hs
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)
g f = f 3 True
UnboxedTuplesも使用する場合は,Unboxedなタプルの型シノニムで書くことができる.
code: data11.hs
h :: Int -> Pr
型シノニムをforall型に適用することができる.
code: data12.hs
type Foo a = a -> a -> Bool
F :: Foo (forall b . b -> b)
型シノニムを展開した後,fは(GHCでは)有効な型を持つ.
code: data13.hs
F :: (forall b. b -> b) -> (forall b. b -> b) -> Bool
型シノニムを部分的に適用された型シノニムに適用できる.
code: data14.hs
type Generic i o = forall x. i x -> o x
type Id x = x
foo :: Generic Id []
型シノニムを展開した後,fooは(GHCでは)有効な型を持つようになる.
code: data15.hs
GHCは現在,型シノニムを拡張する前に種検査を行ってる(もっとも変更される可能性があるが).
型シノニムを拡張した後,GHCは型の妥当性検査を行い,単に種検査では検出されない次のような不正形式を探す.
forallを含む型に適用される型コンストラクタ(ImpredicativeTypesがオフの場合)
部分適用した型シノニム
したがって,たとえば、これは拒否される.
code: data16.hs
type Pr = forall a. a
h = ...
GHCはforallを含む型に適用される型コンストラクタを許可しないためである.
存在量化
明示的な値コンストラクタの型注釈によるデータ型宣言
GADTSyntax
7.2.1以降
データ型定義でGADT構文の使用を許可する.(ただしGADT自体は使用できない.これについてはGADTを参照せよ)
GADTSyntaxが有効になっているとき,GHCは明示的に値コンストラクタの型シグネチャを与えることによって,代数的データ型を宣言することができる.例えば:
code: gsyn1.hs
data Maybe a where
Nothing :: Maybe a
Just :: a -> Maybe a
一般化された代数的データ型(GADT)で説明されている一般化された代数的データ型はこの形式でしか宣言できないため,この形式は「GADTスタイル宣言」と呼ばれる.
GADTスタイルの構文は存在型(存在量化された値コンストラクタ)を一般化していることに注意せよ.たとえば,これら2つの宣言は等価である.
code: gsyn2.hs
data Foo = forall a. MkFoo a (a -> Bool)
data Foo' where
MkFoo :: a -> (a -> Bool) -> Foo'
標準のHaskell 98構文で宣言できるデータ型はGADTスタイルの構文を使って宣言することもできる.どちらを使うのかは主に見た目の好みにすぎないが,GADTスタイルの宣言は1つの重要な点が異なる.それは値コンストラクタに対する型クラス制約の扱いである.具体的には,値コンストラクタに型クラスのコンテキストが与えられると,そのコンテキストはパターンマッチングによって利用可能になる.例えば:
code: gsyn3.hs
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)制約が発生する.(insertの定義のように)MkSetのパターンマッチングで(Eq a)コンテキストが利用できるようになるというのが新しい機能である.実装の面では,MkSetコンストラクタはMkSetに渡される(Eq a)辞書を格納する隠しフィールドを持っている.そのため,パターンマッチング時にその辞書がマッチの右辺で使用可能になる.この例では,等価辞書を使用してelemの呼び出しによって生まれたEq制約が満たされるため,insertの型自体にはEq制約がない.
たとえば,1つの応用例は辞書を具体化することである:
code: gsyn4.hs
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)辞書と同等である。
これらすべては存在と型クラスの構文を使用して宣言された値コンストラクタに当てはまる.たとえば,上記のNumInstデータ型は,次のような同等の宣言ができる.
code: gsync5.hs
data NumInst a = Num a => MkNumInst (NumInst a)
Num制約の型変数aは全称量化されているので,存在量化されたデータ型の宣言の時とは異なり,forallがないことに注意すること.値コンストラクタは,全称型と存在型の両方の変数を持つことができる.たとえば,次の2つの宣言は同じである.
code: gsync6.hs
data T1 a = forall b. (Num a, Eq b) => MkT1 a b
data T2 b where
MkT2 :: (Num a, Eq b) => a -> b -> T2 a
このような振る舞いはすべて,Haskell 98のデータ型宣言に関する特殊なコンテキスト処理(Haskell 98レポートのセクション4.2.1)とは対照的である.Haskell 98では定義
code: gsync7.hs
data Eq a => Set' a = MkSet' a
により与えられるMkSet'が前述のMkSetと同じ型である.しかし,(Eq a)制約を利用可能にする代わりに,MkSet'のパターンマッチングには(Eq a)制約が必要である.GHCはこの奇妙な振る舞いを忠実に実装している.しかしGADTスタイルの宣言では,GHCの振る舞いははるかに直感的であるだけでなく,はるかに便利だ.
この節の残りの部分では,GADTスタイルのデータ型宣言についてさらに詳しく説明する.
各値コンストラクタの返り値の型は定義されている型コンストラクタで始まっていなければならない.もしすべての値コンストラクタの返り値の型がT a1 ... anという形式であり、a1 ... anがdistinct type variablesであれば、そのデータ型は通常のものであり,そうでなければ一般化されたデータ型(GADTs)である.
他の型シグネチャと同様に,複数の値コンストラクタに単一の型シグネチャを付けることができる.この例では,T1とT2に単一の型シグネチャを付ける.
code: gsync8.hs
data T a where -- The 'a' has no scope
T1, T2 :: b -> T b -- Means forall b. b -> T b
T3 :: T a -- Means forall a. T a
各値コンストラクタの型シグネチャは独立しており,いつものとおり,暗黙のうちに全称量化されている.特に,data T a whereヘッダ内の型変数にはスコープがなく,値コンストラクタが異なれば全称量化された型変数も異なる.
値コンストラクタの型シグネチャは型クラスの制約に言及してもよい(値コンストラクタが違えば型クラス制約も異なって良い).例えば,これは許される.
code: gsync9.hs
data T a where
T1 :: Eq b => b -> b -> T b
T2 :: (Show c, Ix c) => c -> c -> T c パターンマッチングのとき,これらの制約はマッチング本体の制約を解除するために使用できる.例えば:
code: gsync10.hs
f :: T a -> String
f (T1 x y) | x == y = "yes"
| otherwise = "no"
f (T2 a b) = show a
ここで、fがオーバーロードされていないことに注意せよ.T1のパターンマッチにより==の使用から発生するEq制約が導出される.T2のパターンマッチでも同様に,showの使用から発生するShow制約も導出される.
Haskell 98スタイルのデータ型宣言とは異なり,data Set a whereヘッダの型変数aはスコープを持たない.実際,代わりに種シグネチャを書くことができる.
code: gsync11.hs
data Set :: Type -> Type where
2つを混ぜることすら許される:
code: gsync12.hs
data Bar a :: (Type -> Type) -> Type where
(もし与えられていれば)型変数は明示的に種付けしても良いので,Fooのヘッダを次のように書くこともできる:
code: gsync13.hs
data Bar a (b :: Type -> Type) where
値コンストラクタの型シグネチャの型の明らかな場所に,正格性注釈をつけられる.
code: gsync14.hs
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句を使用できる.たとえば,これら2つの宣言は等価である:
code: gsync15.hs
data Maybe1 a where {
Nothing1 :: Maybe1 a;
Just :: a -> Maybe1 a
} deriving (Eq, Ord)
data Maybe2 a = Nothing2 | Just2 a
deriving(Eq, Ord)
型シグネチャは返り値の型に現れない量化された型変数を持つことがある.
code: gsync16.hs
data Foo where
MkFoo :: a -> (a -> Bool) -> Foo
Nil :: Foo
ここでは型変数aはどちらの値コンストラクタの返り値型にも現れない.値コンストラクタの型で全称量化されているが,そのような型変数はしばしば「存在型」と呼ばれる.実際,上記の宣言は存在量化されたされた値コンストラクタのdata Fooとまったく同じ型宣言をしている.
もちろん、その型はコンテキストも含んでも良い.
code: gsync17.hs
data Showable where
MkShowable :: Show a => a -> Showable
GADTスタイルのデータ型宣言にレコード構文を使用できる.
code: gsync18.hs
data Person where
Adult :: { name :: String, children :: Person } -> Person Child :: Show a => { name :: !String, funny :: a} -> Person
いつものように,フィールドfを持つそれぞれの値コンストラクタに対して,フィールドfの型は同じでなければならない(モジュロアルファ変換).上記のChildコンストラクタは,レコードがない場合と同様に、型シグニチャがコンテキスト,存在量化された型変数,正確性注釈を持てることを示している(注:レコード構文と正確性注釈のために,ダブルコロンに続く「型」は実際には型ではない.この形式の「型」は,値コンストラクタの型シグネチャでのみ使用できる).
レコードの更新はGADTスタイルの宣言では次の性質をもつフィールドのみ許可される:フィールドの型は存在量化された型変数に言及しない.
Haskell 98風のレコード構文を使って宣言された存在型の場合のように,レコードセレクタ関数はwell-typedなセレクタを持つフィールドに対してのみ生成される.次がGADTスタイルの構文によるそのセクションの例である:
code: gsync19.hs
data Counter a where
NewCounter :: { _this :: self
, _inc :: self -> self
, _display :: self -> IO ()
, tag :: a
} -> Counter a
前と同じように,ここではtag用のセレクタ関数が1つだけ生成される.にもかかわらず,あなたはまだパターンマッチとレコード構築にすべてのフィールド名を使うことができる.
GADTスタイルのデータ型宣言では,値コンストラクタが中置であることを指定する明白な方法はない.そのため,Showを導出しようとすると違いが生じる.(中置に宣言された値コンストラクタから導出されたShowは中置に表示される.)これを踏まえて,GHCは次のような設計を実装している:
GADTスタイルのデータ型宣言で中置に宣言されたデータコンストラクタを中置に表示する必要十分条件は,(a) 演算子記号である.(b)2つの引数がある.(c)プログラマ提供のinfix宣言がある.例えば:
code: gsync20.hs
infix 6 (:--:)
data T a where
(:--:) :: Int -> Bool -> T Int
一般化された代数データ型
GADTs
MonoLocalBinds, GADTSyntaxを含む
6.8.1以降
一般化された代数データ型(GADT)の使用を許可する.
一般化された代数データ型は,コンストラクタがより豊富な返り値の型を持つことを可能にすることで,通常の代数データ型を一般化する.これが一例である:
code: gadts1.hs
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ではないことに注意すること.この一般性により,これらの条件に対してwell-typedなeval関数を書くことができる.
code: gadts2.hs
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 and eval e1 else eval e2
eval (Pair e1 e2) = (eval e1, eval e2)
GADTに関する重要な点は、パターンマッチによって型が篩いにかけられることである.例えば,等式の右辺に
code: gadts3.hs
eval :: Term a -> a
eval (Lit i) = ...
型aはIntにふるい分けられている.それがポイントである.型規則の正確な仕様は,このユーザーマニュアルが目指すものを超えているが,その設計はGADTのための単純な統一ベースの型推論(ICFP 2006)で説明されているものにかなり忠実に従う.一般の原則は次のとおりである.型の絞り込みは,ユーザー指定の型注釈に基づいてのみ実行される.したがって,evalに型シグネチャが指定されていないと,型のふるい分けは行われず,多くの不明瞭なエラーメッセージが表示される.しかし、篩はかなり一般的である.たとえば,次のようになる: code: gsdts4.hs
eval :: Term a -> a -> a
eval (Lit i) j = i+j
パターンが一致すると (値コンストラクタLitの型より)型aがIntに絞り込まれ,その絞り込みはjの型,およびcase式の返り値の型にも適用される.したがって,i + jは有効である.
これらおよび他の多くの例は,Hongwei XiおよびTim Sheardによる論文にある.Wikiにはより長い紹介がある.また,Ralf Hinzeの幽霊型の楽しみ(訳注:関数プログラミングの楽しみ12章)もまた多くの例を挙げている.なお,論文はGHCで実装されているものとは異なる表記法を使用しているかもしれないことに注意すること. このセクションの残りの部分では,GADTをサポートするGHCの拡張について概説する.この拡張機能はGADTsで有効になる.GADTsはGADTSyntaxとMonoLocalBindsも有効にする.
GADTは、GADTスタイルの構文(明示的な値コンストラクタの型シグネチャによるデータ型の宣言)を使用してのみ宣言できる.データ宣言のための古いHaskell 98構文はいつも普通のデータ型を宣言をする.各値コンストラクタの返り値の型は,定義されている型コンストラクタで始まらなければならないが、GADTの場合,型コンストラクタへの引数は任意のモノタイプにすることができる.たとえば,上記のTermデータ型では、各値コンストラクタの型はTerm tyで終わらなければならないが,tyは型変数である必要はない.(e.g. Lit値コンストラクタ)
GADTスタイルの構文を使用して通常の代数データ型を宣言しても良い.GADTをGADTにするのは構文ではなく,むしろ返り値の型がT a bだけではない値コンストラクタの存在である.
GADTにderiving句を使用することはできない.通常のデータ型に対してのみ.
「明示的な値コンストラクタの型シグネチャによるデータ型の宣言」で述べたように,レコード構文はサポートされている.例えば:
code: gadts5.hs
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だが,それらのセレクタ関数は実際には異なる型を持つ.
code: gsdts6.hs
num :: Term Int -> Term Int
arg :: Term Bool -> Term Int
たとえばcase式の中でGADTで定義された値コンストラクタに対するパターンマッチが行う場合,次の規則を満たす必要がある.
検査される型はrigidでなければならない.
case式全体の型はrigidでなけばならない.
caseの選択肢のいずれかに記載されている任意の自由変数の型はrigidでなければならない.
型をその束縛の場所でコンパイラが完全に知っている場合,その型はrigidという.変数がrigidであることを確認する最も簡単な方法は,それに型シグネチャを与えることである.より正確な詳細についてはGADTのための単純な統一ベースの型推論を参照せよ.GHCによって実施される基準は付録に示されている.