Loading article…
関数型プログラミングでは、一般化代数データ型（GADT、別名ファーストクラスファントム型[ 1 ] 、ガード付き再帰データ型[ 2 ]、または等価修飾型[ 3 ]）は、パラメトリック代数データ型（ADT）の一般化です。
GADTでは、積コンストラクタ（Haskellではデータコンストラクタと呼ばれる）は、戻り値の型インスタンス化としてADTの明示的なインスタンス化を提供できます。これにより、より高度な型動作を持つ関数を定義できます。Haskell 2010のデータコンストラクタの場合、戻り値の型インスタンス化は、コンストラクタの適用時にADTパラメータがインスタンス化されることで暗黙的に決定されます。
-- GADTデータではないパラメトリック ADT List a = Nil | Cons a ( List a )integers :: List Int integers = Cons 12 ( Cons 107 Nil )strings :: List String strings = Cons "boat" ( Cons "dock" Nil )-- GADTデータExpr a where EBool :: Bool -> Expr Bool EInt :: Int -> Expr Int EEqual :: Expr Int -> Expr Int -> Expr Booleval :: Expr a -> a eval e = case e of EBool a -> a EInt a -> a EEqual a b -> ( eval a ) == ( eval b )expr1 :: Expr Bool expr1 = EEqual ( EInt 2 ) ( EInt 3 )ret = eval expr1 -- Falseこれらは現在、グラスゴーハスケルコンパイラ（GHC）に非標準拡張機能として実装されており、PugsやDarcsなどで使用されています。OCamlはバージョン4.00以降、GADTをネイティブにサポートしています。[ 4 ]
GHCの実装では、存在量化型パラメータとローカル制約がサポートされています。
一般化代数データ型の初期バージョンは、Augustsson & Petersson (1994)によって記述され、 ALFのパターンマッチングに基づいています。
一般化代数データ型は、MLとHaskellの代数データ型の拡張として、CheneyとHinze (2003)およびそれ以前にXi、ChenとChen (2003)によって独立に導入されました。[ 5 ]両者は本質的に同等です。これらは、Rocqの帰納的構成の計算やその他の依存型言語に見られる帰納的データ型ファミリー(または帰納的データ型)に似ていますが、依存型を除けば、後者には GADT では強制されない追加の正値制約があります。[ 6 ]
Sulzmann、Wazny 、 Stuckey（2006）は、GADTと存在型データ型および型クラス制約を組み合わせた拡張代数型データ型を導入した。
プログラマが提供する型注釈がない場合の型推論は決定不能であり[ 7 ] 、GADT上で定義された関数は一般に主型を許容しない[ 8 ] 。型再構築にはいくつかの設計上のトレードオフが必要であり、活発な研究分野である（Peyton Jones、Washburn & Weirich 2004 ; Peyton Jones et al. 2006）。
2021年春にScala 3.0がリリースされました。[ 9 ]このScalaのメジャーアップデートでは、代数的データ型と同じ構文でGADT [ 10 ]を記述できる機能が導入されました。Martin Odersky氏によると、これは他のプログラミング言語では見られない機能です。[ 11 ]
GADTの応用例としては、汎用プログラミング、プログラミング言語のモデリング（高階抽象構文）、データ構造における不変条件の維持、組み込みドメイン固有言語における制約の表現、オブジェクトのモデリングなどが挙げられる。[ 12 ]
GADTの重要な応用例の一つは、高階抽象構文を型安全な方法で埋め込むことです。以下は、任意の基本型、積型（タプル）、および不動点コンビネータの集合を用いた単純型ラムダ計算の埋め込みです。
データLam :: * -> * where Lift :: a -> Lam a -- ^ リフトされた値Pair :: Lam a -> Lam b -> Lam ( a , b ) -- ^ 積Lam :: ( Lam a -> Lam b ) -> Lam ( a -> b ) -- ^ ラムダ抽象化App :: Lam ( a -> b ) -> Lam a -> Lam b -- ^ 関数適用Fix :: Lam ( a -> a ) -> Lam a -- ^ 固定点そして、型安全な評価関数：
eval :: Lam t -> t eval ( Lift v ) = v eval ( Pair l r ) = ( eval l , eval r ) eval ( Lam f ) = \ x -> eval ( f ( Lift x )) eval ( App f x ) = ( eval f ) ( eval x ) eval ( Fix f ) = ( eval f ) ( eval ( Fix f ))階乗関数は次のように表すことができます。
fact = Fix ( Lam ( \ f -> Lam ( \ y -> Lift ( if eval y == 0 then 1 else eval y * ( eval f ) ( eval y - 1 ))))) eval ( fact )( 10 )通常の代数的データ型を使用すると問題が発生します。型パラメータを削除すると、リフトされた基底型が存在量化され、評価器を記述できなくなります。型パラメータを使用すると、基底型は 1 つに制限されます。さらに、 のような不正な式App (Lam (\x -> Lam (\y -> App x y))) (Lift True)を構築できますが、GADT を使用すると型が不正になります。適切な類似式は ですApp (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True))。これは、 の型xがデータ コンストラクタLam (a -> b)の型から推論される であるためですLam。