The generalized algebraic data type (GADT ) is one of the types of algebraic data types , which is characterized by the fact that its constructors can return values not of the type associated with it [1] . Designed under the influence of works on inductive families among researchers of dependent types [2] .
Such types are implemented in several programming languages, in particular in the OCaml languages (starting with version 4) [3] , Idris [4] , Agda [5] and Haskell , moreover, in the latter it is not part of the language standard, but is implemented only in one from the GHC compiler extensions. The Haskell language imitates an inductive family ( English inductive family ), representing them as types indexed by other types [5] .
They are used in generalized programming , modeling of higher-order abstract syntax of programming languages and object modeling, preservation of invariants of data structures , expression of constraints in built-in domain-specific languages [6] .
History
An early version of generalized algebraic data types was described by Lennart Auguston and Kent Peterson in 1994 and was based on a comparison with the sample in the ALF theorem proof system [7] .
In a modern form, GADTs were introduced independently in 2003 by Cheney and Hinze, and before that, Xi , Chen, and Chen as extensions of the algebraic data types ML and Haskell [8] [9] . The introduced generalized types turned out to be equivalent to each other and similar to inductive families of data types (or inductive data types) used in Coq in calculus of constructions [10] .
In 2006, advanced algebraic data types were developed that combined generalized algebraic data types with and restrictions introduced by Perry, Läufer, and Odersky in the mid-1990s.
Type inference in the absence of type declarations specified by the programmer is an algorithmically insoluble task , and functions defined on generalized ADTs in the general case may not accept the main types ( English principal type ) [11] [12] .
Reconstruction of the type requires several compromises in the design and is the subject of research as of 2011.
Haskell example
The following example defines a generic Type Type , which presents several types [13] :
data Type :: * -> * where
Char :: Type Char
Int :: Type Int
List :: Type a -> Type [ a ]
For this type, one can compose an ad-hoc polymorphic summation function:
sum :: Type a -> a -> Int
sum Char _ = 0
sum Int n = n
sum ( List a ) xs = foldr ( + ) 0 ( map ( sum a ) xs )
Which can be used for types supported by Type , for example, for the type [Int] :
sum ( List Int ) [ 1 , 2 , 4 ]
Notes
- ↑ Koopman, Plasmeijer, Swierstra, 2009 , pp. 178-179.
- ↑ Schmid, Kitzelmann, Plasmeijer, 2010 .
- ↑ Xavier Leroy. The state of OCaml, 2012 (inaccessible link) . OCaml Users and Developers Workshop 4 (September 14, 2012). Date of treatment December 13, 2014. Archived January 2, 2015.
- ↑ Idris Example
- ↑ 1 2 Bove, Ana and Dybjer, Peter and Norell, Ulf (2009). " A Brief Overview of Agda --- A Functional Language with Dependent Types " in TPHOLs '09 . Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics : 73–78, Munich, Germany: Springer-Verlag. DOI : 10.1007 / 978-3-642-03359-9_6 . Bove: 2009: BOA: 1616077.1616085. Retrieved 2013-12-06 .
- ↑ Peyton Jones, Washburn, Weirich, 2004 .
- ↑ Augustsson, Petersson, 1994 .
- ↑ Cheney, Hinze, 2003 , p. 25.
- ↑ Xi, Chen, Chen, 2003 .
- ↑ Cheney, Hinze, 2003 , p. 25-26.
- ↑ Peyton Jones, Washburn, Weirich, 2004 , p. 7.
- ↑ Schrijvers, Peyton Jones, Sulzmann, Vytiniotis, 2009 .
- ↑ Hagiya, M. and Wadler, P. Functional and Logic Programming: 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings. - Springer, 2006 .-- P. 17-18. - ISBN 9783540334385 .
Literature
- Koopman, P .; Plasmeijer, R .; Swierstra, D. Advanced Functional Programming: 6th International School, AFP 2008, Heijen, The Netherlands, May 19-24, 2008, Revised Lectures. - Springer, 2009 .-- 331 p. - ISBN 9783642046513 .
- Peyton Jones, Simon; Washburn, Geoffrey; Weirich, Stephanie. Wobbly types: type inference for generalized algebraic data types (English) // Technical Report MS-CIS-05-25. - University of Pennsylvania, 2004.
- Augustsson, Lennart; Petersson, Kent. Silly type families . - 1994.
- Cheney, James; Hinze, Ralf. First-Class Phantom Types (English) // Technical Report CUCIS TR2003-1901. - Cornell University, 2003.
- Xi, Hongwei; Chen, Chiyan; Chen, Gang. Guarded Recursive Datatype Constructors // Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03). - ACM Press, 2003. - P. 224–235 . - DOI : 10.1145 / 604131.604150 .
- Sheard, Tim; Pasalic, Emir. Meta-programming with built-in type equality (English) // Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork. - 2004. - DOI : 10.1016 / j.entcs.2007.11.11.012 .
- Schmid, U. and Kitzelmann, E. and Plasmeijer, R. Approaches and Applications of Inductive Programming: Third International Workshop, AAIP 2009, Edinburgh, UK, September 4, 2009, Revised Papers. - Springer, 2010 .-- P. 114-115. - ISBN 9783642119309 .
- Peyton Jones, Simon; Vytiniotis, Dimitrios; Weirich, Stephanie; Washburn, Geoffrey. Simple Unification-based Type Inference for GADTs // Proceedings of the ACM International Conference on Functional Programming (ICFP'06), Portland. - 2006.
- Schrijvers, Tom, Peyton Jones, Simon, Sulzmann, Martin, Vytiniotis, Dimitrios. Complete and Decidable Type Inference for GADTs (Eng.) // Proceedings of the ACM International Conference on Functional Programming (ICFP'09), Edinburgh. - 2009.