Generalized algebraic data type
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.
Overview
In a GADT, the product constructors (called
-- 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
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
Generalized algebraic data types were introduced independently by
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
Higher-order abstract syntax
An important application of GADTs is to embed
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
Notes
- ^ Cheney & Hinze 2003.
- ^ Xi, Chen & Chen 2003.
- ^ Sheard & Pasalic 2004.
- ^ "OCaml 4.00.1". ocaml.org.
- ^ Cheney & Hinze 2003, p. 25.
- ^ Cheney & Hinze 2003, pp. 25–26.
- ^ Peyton Jones, Washburn & Weirich 2004, p. 7.
- ^ Schrijvers et al. 2009, p. 1.
- ^ Kmetiuk, Anatolii. "SCALA 3 IS HERE!🎉🎉🎉". scala-lang.org. École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland. Retrieved 19 May 2021.
- ^ "SCALA 3 — BOOK ALGEBRAIC DATA TYPES". scala-lang.org. École Polytechnique Fédérale Lausanne (EPFL) Lausanne, Switzerland. Retrieved 19 May 2021.
- ^ Odersky, Martin. "A Tour of Scala 3 - Martin Odersky". youtube.com. Scala Days Conferences. Archived from the original on 2021-12-19. Retrieved 19 May 2021.
- ^ Peyton Jones, Washburn & Weirich 2004, p. 3.
Further reading
- Applications
- Augustsson, Lennart; Petersson, Kent (September 1994). "Silly type families" (PDF).
- hdl:1813/5614.
- S2CID 15095297.
- .
- 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" (PDF). Technical Report MS-CIS-05-25. University of Pennsylvania.
- Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey (2006). "Simple Unification-based Type Inference for GADTs" (PDF). Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland.
- Wadler, P. (eds.). 8th International Symposium on Functional and Logic Programming (FLOPS 2006). Lecture Notes in Computer Science. Vol. 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 (ed.). Programming Languages and Systems: 4th Asian Symposium (APLAS 2006). Lecture Notes in Computer Science. Vol. 4279. pp. 26–43.
- S2CID 11272015.
- 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