World Library  
Flag as Inappropriate
Email this Article

Generalized algebraic data type

Article Id: WHEBN0006766624
Reproduction Date:

Title: Generalized algebraic data type  
Author: World Heritage Encyclopedia
Language: English
Subject: Functional programming, Data types, Abstract data type, Principal type, Higher-order abstract syntax
Collection: Composite Data Types, Data Types, Dependently Typed Programming, Functional Programming, Type Theory
Publisher: World Heritage Encyclopedia
Publication
Date:
 

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 the algebraic data types of Haskell and ML, applying to parametric types.

With this extension, the parameters of the return type of a data constructor can be freely chosen when declaring the constructor, while for algebraic data types in Haskell 98, the type parameter of the return value is inferred from data types of parameters; 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]

Contents

  • History 1
  • Features 2
  • Applications 3
    • Higher-order abstract syntax 3.1
  • Notes 4
  • Further reading 5
  • External links 6

History

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

Generalized algebraic data types were introduced independently by (Cheney & Hinze 2003) and prior by (Xi, Chen & Chen 2003) 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 & Stuckey 2006) 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 1994) 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 on-going 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).

Features

Non-uniform return parameter type
Existentially quantified type parameters
Local constraints

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

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

And a type safe evaluation function:

eval :: Lam t -> t
eval (Lift v)    = v
eval (Tup e1 e2) = (eval e1, eval e2)
eval (Lam f)     = \x -> eval (f (Lift x))
eval (App e1 e2) = (eval e1) (eval e2)
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)))))

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.

Notes

  1. ^ Cheney & Hinze 2003.
  2. ^ Xi, Chen & Chen 2003.
  3. ^ Sheard & Pasalic 2004.
  4. ^ http://caml.inria.fr/pub/distrib/ocaml-4.00/notes/Changes
  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. ^ Peyton Jones, Washburn & Weirich 2004, p. 3.

Further reading

Applications
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
  •  
  •  
  •  
  •  
  •  
  • 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
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 


Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.