Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Generalized algebraic data type
Résumé
In functional programming, a generalized algebraic data type (GADT, also first-class phantom type, guarded recursive datatype, or equality-qualified type) is a generalization of parametric algebraic data types.
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 GHC compiler as a non-standard extension, used by, among others, Pugs and Darcs. OCaml supports GADT natively since version 4.00.
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 and based on pattern matching in ALF.
Generalized algebraic data types were introduced independently by and prior by as extensions to ML's and Haskell's algebraic data types. 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.
introduced extended algebraic data types which combine GADTs together with the existential data types and type class constraints.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.