Tipo de datos algebraicos generalizados

En programación funcional , un tipo de datos algebraico generalizado ( GADT , también tipo fantasma de primera clase , ^{[ 1 ]} tipo de datos recursivo protegido , ^{[ 2 ]} o tipo calificado de igualdad ^{[ 3 ]} ) es una generalización de un tipo de datos algebraico paramétrico (ADT).

En un GADT, los constructores de producto (denominados constructores de datos en Haskell ) pueden proporcionar una instanciación explícita del ADT como instanciación de tipo de su valor de retorno. Esto permite definir funciones con un comportamiento de tipo más avanzado. Para un constructor de datos de Haskell 2010, el valor de retorno tiene la instanciación de tipo implícita en la instanciación de los parámetros del ADT en la aplicación del constructor.

-- Un ADT paramétrico que no es un GADT Lista de datos a = Nil | Cons a ( Lista a )enteros :: Lista Int enteros = Cons 12 ( Cons 107 Nil )cadenas :: Lista Cadena cadenas = Cons "barco" ( Cons "muelle" Nil )-- Un GADT de datos Expr a donde EBool :: Bool -> Expr Bool EInt :: Int -> Expr Int EEqual :: Expr Int -> Expr Int -> Expr Booleval :: 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 -- Falso

Actualmente se implementan en el compilador Glasgow Haskell (GHC) como una extensión no estándar, utilizada, entre otros, por Pugs y Darcs . OCaml admite GADT de forma nativa desde la versión 4.00. ^{[ 4 ]}

La implementación de GHC ofrece soporte para parámetros de tipo cuantificados existencialmente y para restricciones locales.

Una versión temprana de los tipos de datos algebraicos generalizados fue descrita por Augustsson y Petersson (1994) y se basaba en la coincidencia de patrones en ALF .

Los tipos de datos algebraicos generalizados fueron introducidos independientemente por Cheney y Hinze (2003) y previamente por Xi, Chen y Chen (2003) como extensiones de los tipos de datos algebraicos de ML y Haskell . ^{[ 5 ]} Ambos son esencialmente equivalentes entre sí. Son similares a las familias inductivas de tipos de datos (o tipos de datos inductivos ) que se encuentran en el Cálculo de Construcciones Inductivas de Rocq y otros lenguajes con tipos dependientes , módulo los tipos dependientes y excepto que estos últimos tienen una restricción de positividad adicional que no se aplica en los GADT. ^{[ 6 ]}

Sulzmann, Wazny y Stuckey (2006) introdujeron tipos de datos algebraicos extendidos que combinan GADT con tipos de datos existenciales y restricciones de clase de tipos .

La inferencia de tipos en ausencia de cualquier anotación de tipo proporcionada por el programador es indecidible ^{[ 7 ]} y las funciones definidas sobre GADT no admiten tipos principales en general. ^{[ 8 ]} La reconstrucción de tipos requiere varias compensaciones de diseño y es un área de investigación activa ( Peyton Jones, Washburn y Weirich 2004 ; Peyton Jones et al. 2006 ).

En la primavera de 2021, se lanzó Scala 3.0. ^{[ 9 ]} Esta importante actualización de Scala introdujo la posibilidad de escribir GADT ^{[ 10 ]} con la misma sintaxis que los tipos de datos algebraicos, lo cual no ocurre en otros lenguajes de programación según Martin Odersky . ^{[ 11 ]}

Las aplicaciones de GADT incluyen la programación genérica , el modelado de lenguajes de programación ( sintaxis abstracta de orden superior ), el mantenimiento de invariantes en estructuras de datos , la expresión de restricciones en lenguajes específicos de dominio embebidos y el modelado de objetos. ^{[ 12 ]}

datos Lam :: * -> * donde Lift :: a -> Lam a -- ^ valor elevado Pair :: Lam a -> Lam b -> Lam ( a , b ) -- ^ producto Lam :: ( Lam a -> Lam b ) -> Lam ( a -> b ) -- ^ abstracción lambda App :: Lam ( a -> b ) -> Lam a -> Lam b -- ^ aplicación de función Fix :: Lam ( a -> a ) -> Lam a -- ^ punto fijo

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

hecho = Arreglar ( Lam ( \ f -> Lam ( \ y -> Levantar ( si eval y == 0 entonces 1 sino eval y * ( eval f ) ( eval y - 1 ))))) eval ( hecho )( 10 )

• Variable de tipo

• Página sobre tipos de datos algebraicos generalizados en la wiki de Haskell
• Tipos de datos algebraicos generalizados en la Guía del usuario de GHC
• Tipos de datos algebraicos generalizados y programación orientada a objetos
• GADTs  – Haskell Prime  – Trac Archivado el 4 de abril de 2019 en Wayback Machine
• Artículos sobre inferencia de tipos para GADT , bibliografía de Simon Peyton Jones
• Inferencia de tipos con restricciones , bibliografía de Simon Peyton Jones
• Emulando GADTs en Java mediante el lema de Yoneda