In functional programming, a generalized algebraic data type (GADT, also first-class phantom type,[1] guarded recursive datatype,[2] or equality-qualified type[3]) is a generalization of parametric algebraic data types.

## Contents

* 1 Overview
* 2 History
* 3 Applications
* 3.1 Higher-order abstract syntax
* 4 See also
* 5 Notes
* 6 Further reading
* 7 External links

## Overview

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 = Cons 12 (Cons 107 Nil)       -- the type of integers is List Int
strings = Cons "boat" (Cons "dock" Nil) -- the type of strings is List String

-- 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 = EEqual (EInt 2) (EInt 3)        -- the type of expr1 is Expr Bool
ret = eval expr1                        -- ret is False

They are currently implemented in the GHC compiler as a non-standard extension, used by, among others, Pugs and Darcs. OCaml supports GADT natively since version 4.00.[4]

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

## History

An early version of generalized algebraic data types were described by (Augustsson Petersson) and based on pattern matching in ALF.

Generalized algebraic data types were introduced independently by (Cheney Hinze) and prior by (Xi Chen) as extensions to ML's and Haskell's algebraic data types.[5] 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.[6]

(Sulzmann Wazny) introduced extended algebraic data types which combine GADTs together with the existential data types and type class constraints introduced by (Perry 1991), (Läufer Odersky) and (Läufer 1996).

Type inference in the absence of any programmer supplied type annotations is undecidable[7] and functions defined over GADTs do not admit principal types in general.[8] Type reconstruction requires several design trade-offs and is an area of active research (Peyton Jones, Washburn & Weirich 2004; Peyton Jones et al. 2006; Pottier & Régis-Gianas 2006; Sulzmann, Schrijvers & Stuckey 2006; Simonet & Pottier 2007; Schrijvers et al. 2009; Lin & Sheard 2010a; Lin & Sheard 2010b; Vytiniotis, Peyton Jones & Schrijvers 2010; Vytiniotis et al. 2011).

In spring 2021, Scala 3.0 is released.[9] This major update of Scala introduce the possibility to write GADTs[10] with the same syntax as ADTs, which is not the case in other programming languages according to Martin Odersky.[11]

## Applications

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.[12]

### Higher-order abstract syntax

Further information: 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, 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)

We would have run into problems 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 we would still be restricted to a single base type. Furthermore, 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.

## See also

* Type variable

## Notes

1. ↑ Cheney & Hinze 2003.
2. ↑ Xi, Chen & Chen 2003.
3. ↑ Sheard & Pasalic 2004.
4. ↑ "OCaml 4.00.1". https://ocaml.org/releases/4.00.1.html.
5. ↑ Cheney & Hinze 2003, p. 25.
6. ↑ Cheney & Hinze 2003, pp. 25–26.
7. ↑ Peyton Jones, Washburn & Weirich 2004, p. 7.
8. ↑ Schrijvers et al. 2009, p. 1.
9. ↑ Kmetiuk, Anatolii. "SCALA 3 IS HERE!🎉🎉🎉". École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland. https://www.scala-lang.org/blog/2021/05/14/scala3-is-here.html.
10. ↑ "SCALA 3 — BOOK ALGEBRAIC DATA TYPES". École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland. https://docs.scala-lang.org/scala3/book/types-adts-gadts.html#generalized-algebraic-datatypes-gadts.
11. ↑ Odersky, Martin. "A Tour of Scala 3 - Martin Odersky". Scala Days Conferences. https://www.youtube.com/watch?v=_Rnrx2lo9cw.
12. ↑ Peyton Jones, Washburn & Weirich 2004, p. 3.

## Further reading

Applications

* Augustsson, Lennart; Petersson, Kent (September 1994). Silly type families. http://web.cecs.pdx.edu/~sheard/papers/silly.pdf.
* Cheney, James; Hinze, Ralf (2003). "First-Class Phantom Types". Technical Report CUCIS TR2003-1901 (Cornell University).
* Xi, Hongwei; Chen, Chiyan; Chen, Gang (2003). Guarded Recursive Datatype Constructors. ACM Press. 224–235. doi:10.1145/604131.604150. ISBN 978-1581136289.
* Sheard, Tim; Pasalic, Emir (2004). "Meta-programming with built-in type equality". Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork 199: 49–65. doi:10.1016/j.entcs.2007.11.012.

Semantics

* Patricia Johann and Neil Ghani (2008). "Foundations for Structured Programming with GADTs".
* Arie Middelkoop, Atze Dijkstra and S. Doaitse Swierstra (2011). "A lean specification for GADTs: system F with first-class equality proofs". Higher-Order and Symbolic Computation.

Type reconstruction

* Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie (2004). "Wobbly types: type inference for generalised algebraic data types". Technical Report MS-CIS-05-25 (University of Pennsylvania). http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/MS-CIS-05-26.pdf.
* Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey (2006). "Simple Unification-based Type Inference for GADTs". Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland. http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/gadt-rigid-contexts.pdf.
* Sulzmann, Martin; Wazny, Jeremy; Stuckey, Peter J. (2006). "A Framework for Extended Algebraic Data Types". in Hagiya, M.; Wadler, P.. 3945. pp. 46–64.
* Sulzmann, Martin; Schrijvers, Tom; Stuckey, Peter J. (2006). "Principal Type Inference for GHC-Style Multi-Parameter Type Classes". in Kobayashi, Naoki. 4279. pp. 26–43.
* Schrijvers, Tom; Peyton Jones, Simon; Sulzmann, Martin; Vytiniotis, Dimitrios (2009). "Complete and Decidable Type Inference for GADTs". Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh. http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/implication_constraints.pdf.
* Lin, Chuan-kai (2010). Practical Type Inference for the GADT Type System (PDF) (Doctoral Dissertation thesis). Portland State University.

Other

* Andrew Kennedy and Claudio V. Russo. "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.

## External links

* Generalised Algebraic Datatype Page on the Haskell wiki
* Generalised Algebraic Data Types in the GHC Users' Guide
* Generalized Algebraic Data Types and Object-Oriented Programming
* GADTs – Haskell Prime – Trac
* Papers about type inference for GADTs, bibliography by Simon Peyton Jones
* Type inference with constraints, bibliography by Simon Peyton Jones
* Emulating GADTs in Java via the Yoneda lemma

* v
* t
* e

Data types

Uninterpreted|

* Bit
* Byte
* Trit
* Tryte
* Word
* Bit array

Numeric|

* Arbitrary-precision or bignum
* Complex
* Decimal
* Fixed point
* Floating point
* Double precision
* Extended precision
* Long double
* Octuple precision
* Quadruple precision
* Single precision
* Reduced precision
* Minifloat
* Half precision
* bfloat16
* Integer
* signedness
* Interval
* Rational

Pointer|

* Address
* physical
* virtual
* Reference

Text|

* Character
* String
* null-terminated

Composite|

* Algebraic data type
* generalized
* Array
* Associative array
* Class
* Dependent
* Equality
* Inductive
* Intersection
* List
* Object
* metaobject
* Option type
* Product
* Record or Struct
* Refinement
* Set
* Union
* tagged

Other|

* Boolean
* Bottom type
* Collection
* Enumerated type
* Exception
* Function type
* Opaque data type
* Recursive data type
* Semaphore
* Stream
* Top type
* Type class
* Unit type
* Void

Related
topics|

* Abstract data type
* Data structure
* Generic
* Kind
* metaclass
* Parametric polymorphism
* Primitive data type
* Protocol
* interface
* Subtyping
* Type constructor
* Type conversion
* Type system
* Type theory

See also platform-dependent and independent units of information

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Generalized algebraic data type. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Generalized_algebraic_data_type&oldid=2912786"
*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template