Hispanopedia WikiEn programación funcional , un tipo de datos algebraicos generalizados ( GADT , también tipo fantasma de primera clase , [1] tipo de datos recursivos protegidos , [2] o tipo calificado por igualdad [3] ) es una generalización de un tipo de datos algebraicos paramétricos (ADT).
Descripción general
En un GADT, los constructores de productos (llamados constructores de datos en Haskell ) pueden proporcionar una instanciación explícita del ADT como la 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 por la instanciación de los parámetros del ADT en la aplicación del constructor.
-- Un ADT paramétrico que no es un
dato GADT Lista 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 dato GADT Expr a donde EBool :: Bool -> Expr Bool EInt :: Int -> Expr Int EEqual :: Expr Int -> Expr Int -> Expr Bool
eval :: Expr a -> a eval e = caso e de 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 soporta GADT de forma nativa desde la versión 4.00. [4]
La implementación de GHC proporciona soporte para parámetros de tipo cuantificados existencialmente y para restricciones locales.
Historia
Augustsson y Petersson (1994) describieron una versión temprana de los tipos de datos algebraicos generalizados y se basaron en la coincidencia de patrones en ALF .
Los tipos de datos algebraicos generalizados fueron introducidos independientemente por Cheney y Hinze (2003) y antes 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 Coq y otros lenguajes de tipado dependiente , 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 junto con los tipos de datos existenciales y las restricciones de clase de tipo .
La inferencia de tipos en ausencia de cualquier anotación de tipos suministrada 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 lanza Scala 3.0. [9] Esta importante actualización de Scala introduce la posibilidad de escribir GADT [10] con la misma sintaxis que los tipos de datos algebraicos, lo que no es el caso en otros lenguajes de programación según Martin Odersky . [11]
Aplicaciones
Las aplicaciones de los GADT incluyen programación genérica , modelado de lenguajes de programación ( sintaxis abstracta de orden superior ), mantenimiento de invariantes en estructuras de datos , expresión de restricciones en lenguajes específicos de dominio integrados y modelado de objetos. [12]
Sintaxis abstracta de orden superior
Una aplicación importante de los GADT es la incorporación de una sintaxis abstracta de orden superior de forma segura para los tipos . A continuación, se muestra una incorporación del cálculo lambda de tipos simples con una colección arbitraria de tipos base, tipos de producto ( tuplas ) y un combinador de punto fijo :
datos Lam :: * -> * donde Elevación :: a -> Lam a -- ^ valor elevado Par :: Lam a -> Lam b -> Lam ( a , b ) -- ^ producto Lam :: ( Lam a -> Lam b ) -> Lam ( a -> b ) -- ^ abstracción lambda Aplicación :: Lam ( a -> b ) -> Lam a -> Lam b -- ^ función aplicación Arreglo :: Lam ( a -> a ) -> Lam a -- ^ punto fijo
Y una función de evaluación de tipo seguro:
eval :: Lam t -> t eval ( Elevación v ) = v eval ( Par l r ) = ( eval l , eval r ) eval ( Lam f ) = \ x -> eval ( f ( Elevación x )) eval ( App f x ) = ( eval f ) ( eval x ) eval ( Fijar f ) = ( eval f ) ( eval ( Fijar f ))
La función factorial ahora se puede escribir como:
hecho = Fix ( Lam ( \ f -> Lam ( \ y -> Lift ( si eval y == 0 entonces 1 de lo contrario eval y * ( eval f ) ( eval y - 1 ))))) eval ( hecho )( 10 )
Se habrían producido problemas utilizando tipos de datos algebraicos regulares. Si se hubiera eliminado el parámetro de tipo, los tipos base elevados se habrían cuantificado existencialmente, lo que haría imposible escribir el evaluador. Con un parámetro de tipo, sigue estando restringido a un tipo base. Además, App (Lam (\x -> Lam (\y -> App x y))) (Lift True)habría sido posible construir expresiones mal formadas como , aunque son de tipo incorrecto utilizando la GADT. Un análogo bien formado es App (Lam (\x -> Lam (\y -> App x y))) (Lift (\z -> True)). Esto se debe a que el tipo de xes Lam (a -> b), inferido a partir del tipo del Lamconstructor de datos.
Véase también
Notas
- ^ Cheney y Hinze 2003.
- ^ Xi, Chen y Chen 2003.
- ^ Sheard y Pasalic 2004.
- ^ "OCaml 4.00.1". ocaml.org .
- ^ Cheney y Hinze 2003, pág. 25.
- ^ Cheney y Hinze 2003, págs. 25-26.
- ^ Peyton Jones, Washburn y Weirich 2004, pág. 7.
- ^ Schrijvers y col. 2009, pág. 1.
- ^ Kmetiuk, Anatolii. "¡Scala 3 ya está aquí!". scala-lang.org . École Polytechnique Fédérale Lausanne (EPFL) Lausana, Suiza . Consultado el 19 de mayo de 2021 .
- ^ "Scala 3: tipos de datos algebraicos de libros". scala-lang.org . École Polytechnique Fédérale Lausanne (EPFL) Lausana, Suiza . Consultado el 19 de mayo de 2021 .
- ^ Odersky, Martin. "Un recorrido por Scala 3 – Martin Odersky". youtube.com . Conferencias Scala Days. Archivado desde el original el 19 de diciembre de 2021 . Consultado el 19 de mayo de 2021 .
- ^ Peyton Jones, Washburn y Weirich 2004, pág. 3.
Lectura adicional
- Aplicaciones
- Augustsson, Lennart ; Petersson, Kent (septiembre de 1994). "Familias tipo tontas" (PDF) .
- Cheney, James; Hinze, Ralf (2003). "Tipos Phantom de primera clase". Informe técnico CUCIS TR2003-1901 . Universidad de Cornell. hdl :1813/5614.
- Xi, Hongwei; Chen, Chiyan; Chen, Gang (2003). "Constructores de tipos de datos recursivos protegidos". Actas del 30.º simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . ACM Press. págs. 224–235. CiteSeerX 10.1.1.59.4622 . doi :10.1145/604131.604150. ISBN . 978-1581136289.S2CID 15095297 .
- Sheard, Tim; Pasalic, Emir (2004). "Metaprogramación con igualdad de tipos incorporada". Actas del Cuarto Taller Internacional sobre Marcos Lógicos y Metalenguajes (LFM'04), Cork . 199 : 49–65. doi : 10.1016/j.entcs.2007.11.012 .
- Semántica
- Patricia Johann y Neil Ghani (2008). "Fundamentos para la programación estructurada con GADT".
- Arie Middelkoop, Atze Dijkstra y S. Doaitse Swierstra (2011). "Una especificación simplificada para GADT: sistema F con pruebas de igualdad de primera clase". Computación simbólica y de orden superior .
- Reconstrucción de tipos
- Peyton Jones, Simon ; Washburn, Geoffrey; Weirich, Stephanie (2004). "Tipos inestables: inferencia de tipos para tipos de datos algebraicos generalizados" (PDF) . Informe técnico MS-CIS-05-25 . Universidad de Pensilvania.
- Peyton Jones, Simon ; Vytiniotis, Dimitrios; Weirich, Stephanie ; Washburn, Geoffrey (2006). "Inferencia de tipos basada en unificación simple para GADT" (PDF) . Actas de la Conferencia internacional sobre programación funcional (ICFP'06) de la ACM, Portland .
- Sulzmann, Martin; Wazny, Jeremy; Stuckey, Peter J. (2006). "Un marco para tipos de datos algebraicos extendidos". En Hagiya, M.; Wadler, P. (eds.). 8º Simposio Internacional sobre Programación Funcional y Lógica (FLOPS 2006) . Apuntes de clase en Ciencias de la Computación . Vol. 3945. págs. 46–64.
- Sulzmann, Martin; Schrijvers, Tom; Stuckey, Peter J. (2006). "Inferencia de tipos principales para clases de tipos multiparamétricos de estilo GHC". En Kobayashi, Naoki (ed.). Lenguajes y sistemas de programación: 4.º Simposio asiático (APLAS 2006) . Apuntes de clase en informática. Vol. 4279. págs. 26–43.
- Schrijvers, Tom; Peyton Jones, Simon ; Sulzmann, Martin; Vytiniotis, Dimitrios (2009). "Inferencia de tipos completa y decidible para GADT" (PDF) . Actas de la 14.ª conferencia internacional ACM SIGPLAN sobre programación funcional . págs. 341–352. doi :10.1145/1596550.1596599. ISBN . 9781605583327.S2CID11272015 .
- Lin, Chuan-kai (2010). Inferencia de tipos práctica para el sistema de tipos GADT (PDF) (Tesis doctoral). Universidad Estatal de Portland. Archivado desde el original (PDF) el 2016-06-11 . Consultado el 2011-08-08 .
- Otro
- Andrew Kennedy y Claudio V. Russo. "Tipos de datos algebraicos generalizados y programación orientada a objetos". En Actas de la 20.ª conferencia anual ACM SIGPLAN sobre programación, sistemas, lenguajes y aplicaciones orientadas a objetos . ACM Press, 2005.
Enlaces externos
- Página de 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
- GADT – Haskell Prime – Trac
- 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
- Emulación de GADT en Java mediante el lema de Yoneda