一般化代数データ型

関数型プログラミングにおいて、一般化代数データ型（GADT、第一級ファントム型、[ 1 ] 、保護された再帰データ型、[ 2 ]、または等価修飾型[ 3 ]とも呼ばれる）は、パラメトリック代数データ型（ADT）の一般化である。

概要

GADTでは、積コンストラクタ（Haskellではデータコンストラクタと呼ばれます）は、戻り値の型インスタンス化として、ADTの明示的なインスタンス化を提供できます。これにより、より高度な型の振る舞いを持つ関数を定義できます。Haskell 2010のデータコンストラクタの場合、戻り値は、コンストラクタの適用時にADTパラメータのインスタンス化によって暗黙的に示される型のインスタンス化を持ちます 

-- GADTデータではないパラメトリックADT List a = Nil | Cons a ( List a )整数::リストInt整数= Cons 12 ( Cons 107 Nil )文字列::リスト文字列文字列= 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）に非標準拡張機能として実装されており、PugやDarcなどで使用されています。OCamlはバージョン4.00以降、GADTをネイティブにサポートしています。[ 4 ]

GHC 実装では、存在量化された型パラメータとローカル制約のサポートが提供されます。

歴史

一般化代数データ型の初期バージョンは、AugustssonとPetersson（1994）によって記述され、 ALFのパターンマッチングに基づいていました

一般化代数データ型は、Cheney & Hinze (2003)によって独立に、またそれ以前にはXi, Chen & Chen (2003)によってMLおよびHaskellの代数データ型の拡張として導入されました。[ 5 ]両者は本質的には等価です。これらは、依存型とを除けば、 RocqのCalculus of Inductive Constructionsやその他の依存型言語に見られる帰納的データ型族（または帰納的データ型）に類似していますが、後者にはGADT では強制されない追加の正値制約があります。 [ 6 ]

Sulzmann、Wazny、Stuckey (2006)は、GADT を存在データ型および型クラス制約と組み合わせた拡張代数データ型を導入しました。

プログラマが型注釈を一切提供しない場合の型推論は決定不能であり[ 7 ] 、GADT上で定義された関数は一般に主型を受け入れない。 [ 8 ]型の再構築にはいくつかの設計上のトレードオフが必要であり、活発に研究されている分野である（Peyton Jones、Washburn＆Weirich 2004 ; Peyton Jones他 2006）。

2021年春にScala 3.0がリリースされました。[ 9 ] Scalaのこのメジャーアップデートでは、代数データ型と同じ構文でGADTを記述できるようになりました。 [ 10 ] Martin Odersky氏によると、これは他のプログラミング言語では不可能なことです。[ 11 ]

応用

GADTの応用としては、ジェネリックプログラミング、プログラミング言語（高階抽象構文）のモデリング、データ構造の不変条件の維持、埋め込みドメイン固有言語における制約の表現、オブジェクトのモデリングなどがある。[ 12 ]

高階抽象構文

GADTの重要な応用は、高階抽象構文を型安全に埋め込むことです。以下は、任意の基本型、積型（タプル）、および固定小数点コンビネータの集合を用いた単純型ラムダ計算の埋め込みです 

データLam :: * -> *ここで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 ( eval y == 0なら1 、そうでなければeval y * ( eval f ) ( eval y - 1 ))))) eval ( fact )( 10 )

通常の代数的データ型を使用した場合、問題が発生したでしょう。型パラメータを削除すると、リフトされた基本型が存在量化され、評価器を記述できなくなります。型パラメータをApp (Lam (\x -> Lam (\y -> App x y))) (Lift True)使用しても、評価器は依然として1つの基本型に制限されます。さらに、 のような不適切な式は構築可能でしたが、GADTでは型が不正です。適切な類似例は ですApp (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True))。これは、 の型xが でありLam (a -> b)、データ構築子の型から推論されるためですLam。

参照

注記

  1. ^ Cheney & Hinze 2003
  2. ^シー、チェン、チェン、2003 年。
  3. ^シアード＆パサリック 2004 .
  4. ^ "OCaml 4.00.1" . ocaml.org .
  5. ^チェイニー & ヒンゼ 2003、p. 25.
  6. ^チェイニー & ヒンゼ 2003、25–26 ページ。
  7. ^ペイトン・ジョーンズ、ウォッシュバーン & ワイリッヒ、2004 年、p. 7.
  8. ^ Schrijvers et al. 2009 年、p. 1.
  9. ^クメティウク、アナトリイ。「Scala 3 が来た！」。スカララング.org。エコール・ポリテクニック・フェデラーレ・ローザンヌ (EPFL) スイス、ローザンヌ。2021 年5 月 19 日に取得。
  10. ^ "Scala 3 – 書籍代数データ型" .スカララング.org。エコール・ポリテクニック・フェデラーレ・ローザンヌ (EPFL) スイス、ローザンヌ。2021 年5 月 19 日に取得。
  11. ^ Odersky, Martin. 「Scala 3 ツアー – Martin Odersky」 . youtube.com . Scala Days カンファレンス. 2021年12月19日時点のオリジナルよりアーカイブ。 2021年5月19日閲覧。
  12. ^ペイトン・ジョーンズ、ウォッシュバーン & ワイリッヒ、2004 年、p. 3.

さらに詳しい情報

応用
セマンティクス
型の再構築
その他
WikibooksにはHaskell/GADTに関する書籍があります
「 https://en.wikipedia.org/w/index.php?title=一般化代数データ型&oldid =1330547446」より取得