Type de données algébrique généralisé - Generalized algebraic data type

En programmation fonctionnelle , un type de données algébrique généralisé ( GADT , également type fantôme de première classe , type de données récursif gardé ou type qualifié par l'égalité ) est une généralisation des types de données algébriques paramétriques .

Aperçu

Dans un GADT, les constructeurs de produits (appelés constructeurs de données dans Haskell ) peuvent fournir une instanciation explicite de l'ADT en tant qu'instanciation de type de leur valeur de retour. Cela permet de définir des fonctions avec un comportement de type plus avancé. Pour un constructeur de données de Haskell 2010, la valeur de retour a le type instanciation impliqué par l'instanciation des paramètres ADT au niveau de l'application du constructeur. 

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

Ils sont actuellement implémentés dans le compilateur GHC en tant qu'extension non standard, utilisée, entre autres, par Pugs et Darcs . OCaml supporte GADT nativement depuis la version 4.00.

L'implémentation GHC prend en charge les paramètres de type quantifiés existentiellement et les contraintes locales.

Histoire

Une première version des types de données algébriques généralisées a été décrite par Augustsson & Petersson (1994) et basée sur l' appariement de formes dans ALF .

Les types de données algébriques généralisées ont été introduites de manière indépendante par Cheney et Hinze (2003) et avant par Xi, Chen et Chen (2003) comme des extensions de ML 's et Haskell de types de données algébriques . Les deux sont essentiellement équivalents l'un à l'autre. Ils sont similaires aux familles inductives de types de données (ou types de données inductifs ) trouvées dans le calcul des constructions inductives de Coq et d'autres langages à typage dépendant , modulo les types dépendants et sauf que ces derniers ont une restriction de positivité supplémentaire qui n'est pas appliquée dans les GADT .

Sulzmann, Wazny & Stuckey (2006) ont introduit des types de données algébriques étendus qui combinent les GADT avec les types de données existentiels et les contraintes de classe de types introduites par Perry (1991) , Läufer & Odersky (1994) et Läufer (1996) .

L'inférence de type en l'absence de toute annotation de type fournie par le programmeur est indécidable et les fonctions définies sur les GADT n'admettent pas les types principaux en général. La reconstruction de type nécessite plusieurs compromis de conception et est un domaine de recherche active ( 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 et Sheard 2010a ; Lin et Sheard 2010b ; Vytiniotis, Peyton Jones et Schrijvers 2010 ; Vytiniotis et al. 2011 ).

Au printemps 2021, Scala 3.0 sort. Cette mise à jour majeure de Scala introduit la possibilité d'écrire des GADT avec la même syntaxe que les ADT , ce qui n'est pas le cas dans d'autres langages de programmation selon Martin Odersky .

Applications

Les applications des GADT incluent la programmation générique , la modélisation des langages de programmation ( syntaxe abstraite d'ordre supérieur ), le maintien d' invariants dans les structures de données , l'expression de contraintes dans des langages intégrés spécifiques à un domaine et la modélisation d'objets.

Syntaxe abstraite d'ordre supérieur

Informations complémentaires : syntaxe abstraite d'ordre supérieur

Une application importante de GADTs est d'intégrer la syntaxe abstraite d'ordre supérieur dans un SÛR type de mode. Voici un plongement du calcul lambda simplement typé avec une collection arbitraire de types de base , de tuples et d'un combinateur à virgule fixe : 

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

Et une fonction d'évaluation de type sûr : 

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))

La fonction factorielle peut maintenant s'écrire sous la forme : 

fact = Fix (Lam (\f -> Lam (\y -> Lift (if eval y == 0 then 1 else eval y * (eval f) (eval y - 1)))))
eval(fact)(10)

Nous aurions rencontré des problèmes en utilisant des types de données algébriques réguliers. La suppression du paramètre de type aurait rendu les types de base levés quantifiés existentiellement, rendant impossible l'écriture de l'évaluateur. Avec un paramètre de type, nous serions toujours limités à un seul type de base. De plus, des expressions mal formées telles qu'il App (Lam (\x -> Lam (\y -> App x y))) (Lift True)aurait été possible de construire, alors qu'elles sont de type incorrect à l'aide du GADT. Un analogue bien formé est App (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True)). En effet, le type de x est Lam (a -> b), déduit du type du Lamconstructeur de données.

Voir également

Remarques

Lectures complémentaires

Applications
Sémantique
Reconstitution de type
Autre

Liens externes