ในการเขียนโปรแกรมเชิงฟังก์ชันประเภทข้อมูลพีชคณิตทั่วไป ( GADTหรือ^{ประเภท}แฟนทอมชั้นหนึ่ง [ ^{1 ]}ประเภทข้อมูลเรียกซ้ำแบบมีเงื่อนไข [ ^{2 ] หรือ}ประเภทที่มีคุณสมบัติความเท่าเทียมกัน^{[ 3 ]} ) เป็นการวางนัยทั่วไปของประเภทข้อมูลพีชคณิตแบบพารามิเตอร์ (ADT)

ใน GADT นั้น ตัวสร้างผลิตภัณฑ์ (เรียกว่าตัวสร้างข้อมูลในHaskell ) สามารถให้การสร้างอินสแตนซ์ของ ADT อย่างชัดเจนได้ โดยใช้การสร้างอินสแตนซ์ของประเภทให้กับค่าที่ส่งคืน ซึ่งช่วยให้สามารถกำหนดฟังก์ชันที่มีพฤติกรรมประเภทที่ซับซ้อนยิ่งขึ้นได้ สำหรับตัวสร้างข้อมูลใน Haskell 2010 ค่าที่ส่งคืนจะมีประเภทที่กำหนดโดยนัยจากการสร้างอินสแตนซ์ของพารามิเตอร์ ADT ในการประยุกต์ใช้ตัวสร้าง

-- ADT แบบพาราเมตริกที่ไม่ใช่ GADT รายการข้อมูลa = Nil | Cons a ( รายการa )จำนวนเต็ม:: รายการจำนวนเต็ม= Cons 12 ( Cons 107 Nil )​strings :: List String strings = Cons "boat" ( Cons "dock" Nil )-- ข้อมูลGADT Expr a ที่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 -- เท็จ

ปัจจุบันมีการนำไปใช้ในGlasgow Haskell Compiler (GHC) ในรูปแบบส่วนขยายที่ไม่เป็นมาตรฐาน ซึ่งใช้โดยPugsและDarcsเป็นต้นOCamlรองรับ GADT โดยตรงตั้งแต่เวอร์ชัน 4.00 ^{[ 4 ]}

การใช้งาน GHC ให้การสนับสนุนพารามิเตอร์ประเภทที่ระบุปริมาณเชิงการมีอยู่ และข้อจำกัดเฉพาะที่

Augustsson & Petersson (1994) ได้ อธิบาย รูปแบบข้อมูลพีชคณิตทั่วไปในเวอร์ชันแรกๆโดยอิงจากการจับคู่รูปแบบในALF

ประเภทข้อมูลพีชคณิตทั่วไปได้รับการแนะนำโดยอิสระโดยCheney & Hinze (2003) ^และก่อนหน้านั้นโดยXi, Chen & Chen (2003)ในฐานะส่วนขยายของประเภทข้อมูลพีชคณิตของMLและHaskell [ ^{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 ที่สำคัญอย่างหนึ่งคือการฝังไวยากรณ์นามธรรมลำดับสูงใน ลักษณะ ที่ปลอดภัยต่อประเภทข้อมูลต่อไปนี้คือการฝังแคลคูลัสแลมบ์ดาแบบกำหนดประเภทข้อมูลอย่างง่ายด้วยชุดประเภทข้อมูลพื้นฐานประเภทผลคูณ ( ทูเปิล ) และตัวรวมจุดคงที่แบบใดก็ได้ :

data 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 )

หากใช้ชนิดข้อมูลพีชคณิตทั่วไป ปัญหาจะเกิดขึ้น การตัดพารามิเตอร์ชนิดข้อมูลออกจะทำให้ชนิดข้อมูลพื้นฐานที่ยกขึ้นมานั้นมีปริมาณเชิงการมีอยู่ ทำให้ไม่สามารถเขียนตัวประเมินได้ แม้จะมีพารามิเตอร์ชนิดข้อมูล แต่ก็ยังคงจำกัดอยู่เพียงชนิดข้อมูลพื้นฐานเดียว นอกจากนี้ นิพจน์ที่ไม่ถูกต้อง เช่น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ตัวสร้างข้อมูล

• ประเภทตัวแปร

Wikibooks มีหนังสือเกี่ยวกับหัวข้อHaskell/GADT

• หน้าข้อมูลประเภทพีชคณิตทั่วไป (Generalised Algebraic Datatype) บน วิกิของ Haskell
• ประเภทข้อมูลพีชคณิตทั่วไปในคู่มือผู้ใช้ GHC
• ประเภทข้อมูลพีชคณิตทั่วไปและการเขียนโปรแกรมเชิงวัตถุ
• GADTs – Haskell Prime – Trac เก็บถาวรเมื่อ 2019-04-04 ที่Wayback Machine
• เอกสารเกี่ยวกับการอนุมานประเภทสำหรับ GADTบรรณานุกรมโดยSimon Peyton Jones
• การอนุมานประเภทด้วยข้อจำกัดบรรณานุกรมโดยSimon Peyton Jones
• การจำลอง GADT ใน Java โดยใช้เลมมาของโยเนดะ