generalized algebraic data type

In a GADT, the product constructors (called data constructors in Haskell) can provide an explicit instantiation of the ADT as the type instantiation of their return value. This allows defining functions with a more advanced type behaviour. For a data constructor of Haskell 2010, the return value has the type instantiation implied by the instantiation of the ADT parameters at the constructor's application.

-- A parametric ADT that is not a GADT

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

-- A GADT

data Expr a where

EBool :: Bool -> Expr Bool

EInt :: Int -> Expr Int

EEqual :: Expr Int -> Expr Int -> Expr Bool

eval :: 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

They are currently implemented in the Glasgow Haskell Compiler (GHC) as a non-standard extension, used by, among others, Pugs and Darcs. OCaml supports GADT natively since version 4.00.{{cite web|title=OCaml 4.00.1|url=https://ocaml.org/releases/4.00.1.html|website=ocaml.org}}

The GHC implementation provides support for existentially quantified type parameters and for local constraints.

An early version of generalized algebraic data types were described by {{harvtxt|Augustsson|Petersson|1994}} and based on pattern matching in ALF.

Generalized algebraic data types were introduced independently by {{harvtxt|Cheney|Hinze|2003}} and prior by {{harvtxt|Xi|Chen|Chen|2003}} as extensions to the algebraic data types of ML and Haskell.{{sfn|Cheney|Hinze|2003|p=25}} Both are essentially equivalent to each other. They are similar to the inductive families of data types (or inductive datatypes) found in Coq's Calculus of Inductive Constructions and other dependently typed languages, modulo the dependent types and except that the latter have an additional positivity restriction which is not enforced in GADTs.{{sfn|Cheney|Hinze|2003|pp=25–26}}

{{harvtxt|Sulzmann|Wazny|Stuckey|2006}} introduced extended algebraic data types which combine GADTs together with the existential data types and type class constraints.

Type inference in the absence of any programmer supplied type annotation, is undecidable{{sfn|Peyton Jones|Washburn|Weirich|2004|p=7}} and functions defined over GADTs do not admit principal types in general.{{sfn|Schrijvers|Peyton Jones|Sulzmann|Vytiniotis|2009|p=1}} Type reconstruction requires several design trade-offs and is an area of active research ({{harvnb|Peyton Jones|Washburn|Weirich|2004}}; {{harvnb|Peyton Jones|Vytiniotis|Weirich|Washburn|2006}}.

In spring 2021, Scala 3.0 was released.{{cite web |last1=Kmetiuk |first1=Anatolii |title=Scala 3 Is Here! |url=https://www.scala-lang.org/blog/2021/05/14/scala3-is-here.html |website=scala-lang.org |publisher=École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland |access-date=19 May 2021}} This major update of Scala introduced the possibility to write GADTs{{cite web |title=Scala 3 – Book Algebraic Data Types |url=https://docs.scala-lang.org/scala3/book/types-adts-gadts.html#generalized-algebraic-datatypes-gadts |website=scala-lang.org |publisher=École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland |access-date=19 May 2021 |ref=gadt-scala3}} with the same syntax as algebraic data types, which is not the case in other programming languages according to Martin Odersky.{{cite web |last1=Odersky |first1=Martin |title=A Tour of Scala 3 – Martin Odersky |url=https://www.youtube.com/watch?v=_Rnrx2lo9cw |archive-url=https://ghostarchive.org/varchive/youtube/20211219/_Rnrx2lo9cw |archive-date=2021-12-19 |url-status=live |website=youtube.com |publisher=Scala Days Conferences |access-date=19 May 2021 |ref=scala3-tour}}{{cbignore}}

Applications of GADTs include generic programming, modelling programming languages (higher-order abstract syntax), maintaining invariants in data structures, expressing constraints in embedded domain-specific languages, and modelling objects.{{sfn|Peyton Jones|Washburn|Weirich|2004|p=3}}

{{further|Higher-order abstract syntax}}

An important application of GADTs is to embed higher-order abstract syntax in a type safe fashion. Here is an embedding of the simply typed lambda calculus with an arbitrary collection of base types, product types (tuples) and a fixed point combinator:

data Lam :: * -> * where

Lift :: a -> Lam a -- ^ lifted value

Pair :: Lam a -> Lam b -> Lam (a, b) -- ^ product

Lam :: (Lam a -> Lam b) -> Lam (a -> b) -- ^ lambda abstraction

App :: Lam (a -> b) -> Lam a -> Lam b -- ^ function application

Fix :: Lam (a -> a) -> Lam a -- ^ fixed point

And a type safe evaluation function:

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

The factorial function can now be written as:

fact = Fix (Lam (\f -> Lam (\y -> Lift (if eval y == 0 then 1 else eval y * (eval f) (eval y - 1)))))

eval(fact)(10)

Problems would have occurred using regular algebraic data types. Dropping the type parameter would have made the lifted base types existentially quantified, making it impossible to write the evaluator. With a type parameter, it is still restricted to one base type. Further, ill-formed expressions such as App (Lam (\x -> Lam (\y -> App x y))) (Lift True) would have been possible to construct, while they are type incorrect using the GADT. A well-formed analogue is App (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True)). This is because the type of x is Lam (a -> b), inferred from the type of the Lam data constructor.

• Type variable

{{Reflist}}

{{Refbegin|2}}

; Applications

• {{cite web|first1=Lennart|last1=Augustsson|author-link1=Lennart Augustsson|first2=Kent|last2=Petersson|title=Silly type families|url=http://web.cecs.pdx.edu/~sheard/papers/silly.pdf|date=September 1994}}
• {{cite journal|first1=James|last1=Cheney|author-link1=James Cheney (computer scientist)|first2=Ralf|last2=Hinze|author-link2=Ralf Hinze|year=2003|title=First-Class Phantom Types|journal=Technical Report CUCIS TR2003-1901|publisher=Cornell University|hdl=1813/5614}}
• {{cite book|first1=Hongwei|last1=Xi|author-link=Hongwei Xi|first2=Chiyan|last2=Chen|author-link2=Chiyan Chen|first3=Gang|last3=Chen|title=Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages |chapter=Guarded recursive datatype constructors |year=2003|pages=224–235|publisher=ACM Press|doi=10.1145/604131.604150|isbn=978-1581136289|citeseerx=10.1.1.59.4622|s2cid=15095297}}
• {{cite journal|first1=Tim|last1=Sheard|author-link=Tim Sheard|first2=Emir|last2=Pasalic|author-link2=Emir Pasalic|year=2004|title=Meta-programming with built-in type equality|journal=Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork|volume=199|pages=49–65|doi=10.1016/j.entcs.2007.11.012|doi-access=free}}

; Semantics

• Patricia Johann and Neil Ghani (2008). "[https://strathprints.strath.ac.uk/33726/1/ghani_popl08.pdf Foundations for Structured Programming with GADTs]".
• Arie Middelkoop, Atze Dijkstra and S. Doaitse Swierstra (2011). "[https://www.researchgate.net/profile/S-Swierstra/publication/220606952_A_lean_specification_for_GADTs_System_F_with_first-class_equality_proofs/links/0c960529dac172f57d000000/A-lean-specification-for-GADTs-System-F-with-first-class-equality-proofs.pdf A lean specification for GADTs: system F with first-class equality proofs]". Higher-Order and Symbolic Computation.

; Type reconstruction

• {{cite journal|first1=Simon|last1=Peyton Jones|author-link1=Simon Peyton Jones|first2=Geoffrey|last2=Washburn|author-link2=Geoffrey Washburn|first3=Stephanie|last3=Weirich|author-link3=Stephanie Weirich|year=2004|title=Wobbly types: type inference for generalised algebraic data types|journal=Technical Report MS-CIS-05-25|publisher=University of Pennsylvania|url=http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/MS-CIS-05-26.pdf}}
• {{cite journal|first1=Simon|last1=Peyton Jones|author-link1=Simon Peyton Jones|first2=Dimitrios|last2=Vytiniotis|author-link2=Dimitrios Vytiniotis|first3=Stephanie|last3=Weirich|author-link3=Stephanie Weirich|first4=Geoffrey|last4=Washburn|author-link4=Geoffrey Washburn|year=2006|title=Simple Unification-based Type Inference for GADTs|journal=Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland|url=http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/gadt-rigid-contexts.pdf}}
• {{cite conference |first1=Martin|last1=Sulzmann|author-link1=Martin Sulzmann|first2=Jeremy|last2=Wazny|author-link2=Jeremy Wazny|first3=Peter J.|last3=Stuckey|author-link3=Peter J. Stuckey|title=A Framework for Extended Algebraic Data Types |book-title=8th International Symposium on Functional and Logic Programming (FLOPS 2006)|editor1-first=M.|editor1-last=Hagiya|editor2-first=P.|editor2-last=Wadler|editor2-link=Phil Wadler|series=Lecture Notes in Computer Science|volume=3945|pages=46–64|year=2006}}
• {{cite conference |first1=Martin|last1=Sulzmann|author-link1=Martin Sulzmann|first2=Tom|last2=Schrijvers|author-link2=Tom Schrijvers|first3=Peter J.|last3=Stuckey|author-link3=Peter J. Stuckey|title=Principal Type Inference for GHC-Style Multi-Parameter Type Classes |book-title=Programming Languages and Systems: 4th Asian Symposium (APLAS 2006) |editor-first=Naoki |editor-last=Kobayashi |series=Lecture Notes in Computer Science|volume=4279|pages=26–43|year=2006}}
• {{cite book|first1=Tom|last1=Schrijvers|author-link1=Tom Schrijvers|first2=Simon|last2=Peyton Jones|author-link2=Simon Peyton Jones|first3=Martin|last3=Sulzmann|author-link3=Martin Sulzmann|first4=Dimitrios|last4=Vytiniotis|title=Proceedings of the 14th ACM SIGPLAN international conference on Functional programming|chapter=Complete and decidable type inference for GADTs|author-link4=Dimitrios Vytiniotis|year=2009|pages=341–352|doi=10.1145/1596550.1596599|isbn=9781605583327|s2cid=11272015|chapter-url=http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/implication_constraints.pdf}}
• {{cite thesis|first1=Chuan-kai|last1=Lin|title=Practical Type Inference for the GADT Type System|url=http://sites.google.com/site/chklin/research/dissertation.pdf?attredirects=0|degree=Doctoral Dissertation|publisher=Portland State University|year=2010|access-date=2011-08-08|archive-date=2016-06-11|archive-url=https://web.archive.org/web/20160611160430/https://sites.google.com/site/chklin/research/dissertation.pdf?attredirects=0|url-status=dead}}

; Other

• Andrew Kennedy and Claudio V. Russo. "[https://www.researchgate.net/profile/Claudio_Russo/publication/213880929_Generalized_algebraic_data_types_and_object-oriented_programming/links/5724878d08aee491cb3a3ebf/Generalized-algebraic-data-types-and-object-oriented-programming.pdf Generalized algebraic data types and object-oriented programming]". In Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications. ACM Press, 2005.

{{Refend}}

{{wikibooks|Haskell/GADT}}

• [http://www.haskell.org/haskellwiki/Generalised_algebraic_datatype Generalised Algebraic Datatype Page] on the Haskell wiki
• [http://haskell.org/ghc/docs/7.0-latest/html/users_guide/data-type-extensions.html#gadt Generalised Algebraic Data Types] in the GHC Users' Guide
• [http://lambda-the-ultimate.org/node/1134 Generalized Algebraic Data Types and Object-Oriented Programming]
• [http://prime.haskell.org/wiki/GADTs GADTs – Haskell Prime – Trac]
• [http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/ Papers about type inference for GADTs], bibliography by Simon Peyton Jones
• [http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/ Type inference with constraints], bibliography by Simon Peyton Jones
• [https://gist.github.com/jbgi/208a1733f15cdcf78eb5 Emulating GADTs in Java via the Yoneda lemma]

{{Data types}}

Category:Functional programming

Category:Dependently typed programming

Category:Type theory

Category:Composite data types

Category:Data types