stringtranslate.com

Clase de tipo

En informática , una clase de tipo es una construcción de sistema de tipos que admite polimorfismo ad hoc . Esto se logra agregando restricciones a las variables de tipo en tipos paramétricamente polimórficos . Dicha restricción generalmente involucra una clase de tipo Ty una variable de tipo a , y significa que asolo se puede instanciar en un tipo cuyos miembros admitan las operaciones sobrecargadas asociadas con T.

Las clases de tipos se implementaron por primera vez en el lenguaje de programación Haskell después de ser propuestas por primera vez por Philip Wadler y Stephen Blott como una extensión de "eqtypes" en Standard ML , [1] [2] y fueron concebidas originalmente como una forma de implementar operadores aritméticos y de igualdad sobrecargados de una manera basada en principios. [3] [2] A diferencia de los "eqtypes" de Standard ML, la sobrecarga del operador de igualdad mediante el uso de clases de tipos en Haskell no requiere una modificación extensa de la interfaz del compilador o del sistema de tipos subyacente. [4]

Descripción general

Las clases de tipos se definen especificando un conjunto de nombres de funciones o constantes, junto con sus respectivos tipos, que deben existir para cada tipo que pertenece a la clase. En Haskell, los tipos se pueden parametrizar; una clase de tipos Eqdestinada a contener tipos que admitan igualdad se declararía de la siguiente manera:

clase Eq a donde ( == ) :: a -> a -> Bool ( /= ) :: a -> a -> Bool                 

donde aes una instancia de la clase de tipo Eqy adefine las firmas de función para 2 funciones (las funciones de igualdad y desigualdad), cada una de las cuales toma 2 argumentos de tipo ay devuelve un valor booleano.

La variable de tipo atiene tipo ( también se conoce como en la última versión de GHC ), [5] lo que significa que el tipo de esTypeEq

Eq :: Tipo -> Restricción    

La declaración puede interpretarse como que "un tipo apertenece a una clase de tipos Eqsi existen funciones denominadas (==), y (/=), de los tipos apropiados, definidas en ella". Un programador podría entonces definir una función elem(que determina si un elemento está en una lista) de la siguiente manera:

elem :: Eq a => a -> [ a ] ​​-> Bool elem y [] = False elem y ( x : xs ) = ( x == y ) || elemento y xs                       

La función elemtiene el tipo a -> [a] -> Boolcon el contexto Eq a, que restringe los tipos que apueden abarcar hasta aquellos aque pertenecen a la Eqclase de tipo. ( Nota : Haskell => puede denominarse una "restricción de clase").

Un programador puede convertir cualquier tipo ten miembro de una clase de tipo dada Cmediante una declaración de instancia que defina implementaciones de todos los Cmétodos de para el tipo en particular t. Por ejemplo, si un programador define un nuevo tipo de datos t, puede convertir este nuevo tipo en una instancia de Eqproporcionando una función de igualdad sobre los valores de tipo tde la forma que considere adecuada. Una vez que haya hecho esto, puede utilizar la función elemen [t], es decir, listas de elementos de tipo t.

Tenga en cuenta que las clases de tipo son diferentes de las clases en los lenguajes de programación orientados a objetos. En particular, Eqno es un tipo: no existe nada parecido a un valor de tipo Eq.

Las clases de tipos están estrechamente relacionadas con el polimorfismo paramétrico. Por ejemplo, observe que el tipo elemespecificado anteriormente sería el tipo paramétricamente polimórfico a -> [a] -> Boolsi no fuera por la restricción de clase de tipo " Eq a =>".

Polimorfismo de tipo superior

Una clase de tipo no necesita tomar una variable de tipo de tipo Type , sino una de cualquier tipo. Estas clases de tipo con tipos superiores a veces se denominan clases constructoras (los constructores a los que se hace referencia son constructores de tipo como Maybe, en lugar de constructores de datos como Just). Un ejemplo es la Monadclase:

clase Mónada m donde retorna :: a -> m a ( >>= ) :: m a -> ( a -> m b ) -> m b                     

El hecho de que m se aplique a una variable de tipo indica que tiene tipo Type -> Type, es decir, toma un tipo y devuelve un tipo, el tipo Monades así:

Mónada :: ( Tipo -> Tipo ) -> Restricción      

Clases de tipos multiparamétricos

Las clases de tipos permiten múltiples parámetros de tipo, por lo que las clases de tipos pueden verse como relaciones entre tipos. [6] Por ejemplo, en la biblioteca estándar de GHCIArray , la clase expresa una interfaz de matriz inmutable general. En esta clase, la restricción de clase de tipo IArray a esignifica que aes un tipo de matriz que contiene elementos de tipo e. (Esta restricción de polimorfismo se utiliza para implementar tipos de matriz no encapsulados , por ejemplo).

Al igual que los métodos múltiples [ cita requerida ] , las clases de tipos multiparamétricos admiten la llamada a diferentes implementaciones de un método según los tipos de argumentos múltiples y, de hecho, los tipos de retorno. Las clases de tipos multiparamétricos no requieren buscar el método al que llamar en cada llamada en tiempo de ejecución; [7] : minuto 25:12  en lugar de eso, el método al que llamar se compila primero y se almacena en el diccionario de la instancia de la clase de tipos, al igual que con las clases de tipos de un solo parámetro.

El código Haskell que utiliza clases de tipos multiparámetros no es portable, ya que esta característica no forma parte del estándar Haskell 98. Las implementaciones populares de Haskell, GHC y Hugs , admiten clases de tipos multiparámetros.

Dependencias funcionales

En Haskell, las clases de tipos se han refinado para permitir al programador declarar dependencias funcionales entre parámetros de tipo, un concepto inspirado en la teoría de bases de datos relacionales . [8] [9] Es decir, el programador puede afirmar que una asignación dada de algún subconjunto de los parámetros de tipo determina de forma única los parámetros de tipo restantes. Por ejemplo, una mónada m general que lleva un parámetro de estado de tipo ssatisface la restricción de clase de tipo Monad.State s m. En esta restricción, hay una dependencia funcional m -> s. Esto significa que para una mónada dada mde clase de tipo Monad.State, el tipo de estado accesible desde mestá determinado de forma única. Esto ayuda al compilador en la inferencia de tipos , así como al programador en la programación dirigida por tipos.

Simon Peyton-Jones se ha opuesto a la introducción de dependencias funcionales en Haskell por razones de complejidad. [10]

Clases de tipos y parámetros implícitos

Las clases de tipos y los parámetros implícitos son de naturaleza muy similar, aunque no exactamente iguales. Una función polimórfica con una restricción de clase de tipos como:

suma :: Num a => [ a ] ​​-> a       

puede tratarse intuitivamente como una función que acepta implícitamente una instancia de Num:

suma_ :: Num_ a -> [ a ] ​​-> a       

La instancia Num_ aes esencialmente un registro que contiene la definición de instancia de Num a. (De hecho, así es como el compilador Glasgow Haskell implementa las clases de tipos).

Sin embargo, existe una diferencia crucial: los parámetros implícitos son más flexibles : se pueden pasar diferentes instancias de Num Int. Por el contrario, las clases de tipos aplican la denominada propiedad de coherencia , que exige que solo haya una única opción de instancia para cualquier tipo dado. La propiedad de coherencia hace que las clases de tipos sean algo antimodulares, por lo que las instancias huérfanas (instancias que se definen en un módulo que no contiene ni la clase ni el tipo de interés) están fuertemente desaconsejadas. Por otro lado, la coherencia añade un nivel adicional de seguridad al lenguaje, proporcionando al programador una garantía de que dos partes disjuntas del mismo código compartirán la misma instancia. [11]

Por ejemplo, un conjunto ordenado (de tipo Set a) requiere un ordenamiento total de los elementos (de tipo a) para funcionar. Esto se puede evidenciar mediante una restricción Ord a, que define un operador de comparación sobre los elementos. Sin embargo, puede haber numerosas formas de imponer un orden total. Dado que los algoritmos de conjuntos generalmente son intolerantes a los cambios en el ordenamiento una vez que se ha construido un conjunto, pasar una instancia incompatible de Ord aa funciones que operan en el conjunto puede conducir a resultados incorrectos (o fallas). Por lo tanto, hacer cumplir la coherencia de Ord aen este escenario particular es crucial.

Las instancias (o "diccionarios") en las clases de tipos de Scala son simplemente valores ordinarios en el lenguaje, en lugar de un tipo de entidad completamente independiente. [12] [13] Si bien estas instancias se suministran de manera predeterminada al encontrar instancias apropiadas en el ámbito para ser utilizadas como parámetros reales implícitos para parámetros formales implícitos declarados explícitamente, el hecho de que sean valores ordinarios significa que se pueden suministrar explícitamente para resolver la ambigüedad. Como resultado, las clases de tipos de Scala no satisfacen la propiedad de coherencia y son efectivamente un azúcar sintáctico para los parámetros implícitos.

Este es un ejemplo tomado de la documentación de Cats [14] :

// Una clase de tipo para proporcionar la característica de representación textual Show [ A ] { def show ( f : A ): String }      // Una función polimórfica que funciona solo cuando hay una instancia implícita de Show[A] disponible def log [ A ]( a : A )( implicit s : Show [ A ]) = println ( s . show ( a ))      // Una instancia para String implícito val stringShow = new Show [ String ] { def show ( s : String ) = s }           // El parámetro stringShow fue insertado por el compilador. scala > log ( "una cadena" ) una cadena  

Coq (versión 8.2 en adelante) también admite clases de tipos al inferir las instancias apropiadas. [15] Las versiones recientes de Agda 2 también proporcionan una característica similar, llamada "argumentos de instancia". [16]

Otros enfoques para la sobrecarga de operadores

En el aprendizaje automático estándar , el mecanismo de "tipos de igualdad" corresponde aproximadamente al tipo incorporado class de Haskell Eq, pero el compilador deriva automáticamente todos los operadores de igualdad. El control del proceso por parte del programador se limita a designar qué componentes de tipo en una estructura son tipos de igualdad y qué variables de tipo en un rango de tipos polimórficos abarcan más de los tipos de igualdad.

Los módulos y funtores de SML y OCaml pueden desempeñar un papel similar al de las clases de tipos de Haskell, siendo la principal diferencia el papel de la inferencia de tipos, que hace que las clases de tipos sean adecuadas para el polimorfismo ad hoc . [17] El subconjunto orientado a objetos de OCaml es otro enfoque que es de alguna manera comparable al de las clases de tipos.

Nociones relacionadas

Una noción análoga para datos sobrecargados (implementada en GHC ) es la de familia de tipos . [18]

En C++, en particular, C++20 tiene soporte para clases de tipos mediante el uso de Conceptos (C++) . A modo de ilustración, el ejemplo de Haskell mencionado anteriormente de la clase de tipos Eq se escribiría como

plantilla < typename T > concepto Igual = requiere ( T a , T b ) { { a == b } -> std :: convertible_to < bool > ; { a != b } -> std :: convertible_to < bool > ; };                        

Las clases de tipos Clean son similares a Haskell, pero tienen una sintaxis ligeramente diferente.

Rust admite rasgos , que son una forma limitada de clases de tipos con coherencia. [19]

Mercury tiene clases de tipos, aunque no son exactamente iguales que en Haskell. [ se necesita más explicación ]

En Scala , las clases de tipos son un modismo de programación que se puede implementar con características del lenguaje existentes, como parámetros implícitos, no una característica del lenguaje separada per se. Debido a la forma en que se implementan en Scala, es posible especificar explícitamente qué instancia de clase de tipos usar para un tipo en un lugar particular del código, en caso de ambigüedad. Sin embargo, esto no es necesariamente un beneficio ya que las instancias de clase de tipos ambiguas pueden ser propensas a errores.

El asistente de pruebas Coq también ha admitido clases de tipos en versiones recientes. A diferencia de los lenguajes de programación comunes, en Coq, todas las leyes de una clase de tipos (como las leyes de las mónadas) que se establecen dentro de la definición de la clase de tipos deben demostrarse matemáticamente para cada instancia de la clase de tipos antes de usarlas.

Véase también

Referencias

  1. ^ Morris, John G. (2013). Clases de tipos y cadenas de instancias: un enfoque relacional (PDF) (PhD). Departamento de Ciencias de la Computación, Universidad Estatal de Portland. doi :10.15760/etd.1010.
  2. ^ ab Wadler, P.; Blott, S. (1989). "Cómo hacer que el polimorfismo ad hoc sea menos ad hoc". Actas del 16.º Simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación (POPL '89) . Association for Computing Machinery. págs. 60–76. doi :10.1145/75277.75283. ISBN . 0897912942.S2CID 15327197  .
  3. ^ Kaes, Stefan (marzo de 1988). "Sobrecarga paramétrica en lenguajes de programación polimórficos". Proc. 2º Simposio Europeo sobre Lenguajes de Programación . doi : 10.1007/3-540-19027-9_9 .
  4. ^ Appel, AW; MacQueen, DB (1991). "ML estándar de Nueva Jersey". En Maluszyński, J.; Wirsing, M. (eds.). Implementación de lenguaje de programación y programación lógica. PLILP 1991. Apuntes de clase en informática. Vol. 528. Springer. págs. 1–13. CiteSeerX 10.1.1.55.9444 . doi :10.1007/3-540-54444-5_83. ISBN .  3-540-54444-5.
  5. ^ El tipo de Data.Kindapareció en la versión 8 del compilador Glasgow Haskell
  6. ^ Página de Haskell MultiParamTypeClasses .
  7. ^ En GHC, el núcleo C utiliza las firmas de tipo del Sistema F de Girard y Reynolds para identificar un caso tipificado para su procesamiento en las fases de optimización. -- Simon Peyton-Jones "Into the Core - Squeezing Haskell into Nine Constructors" Conferencia de usuarios de Erlang, 14 de septiembre de 2016
  8. ^ Jones, Mark P. (2000). "Clases de tipos con dependencias funcionales". En Smolka, G. (ed.). Lenguajes y sistemas de programación. ESOP 2000. Apuntes de clase en informática. Vol. 1782. Springer. págs. 230–244. CiteSeerX 10.1.1.26.7153 . doi :10.1007/3-540-46425-5_15. ISBN.  3-540-46425-5.
  9. ^ Página de Haskell DependenciasFuncionales .
  10. ^ Peyton-Jones, Simon (2006). "MPTCs y dependencias funcionales". Lista de correo Haskell-prime .
  11. ^ Kmett, Edward. Clases de tipos frente al mundo. Boston Haskell Meetup. Archivado desde el original el 21 de diciembre de 2021.
  12. ^ Oliveira, Bruno CdS; Moors, Adriaan; Odersky, Martin (2010). "Clases de tipos como objetos e implícitos" (PDF) . Actas de la Conferencia Internacional ACM sobre Lenguajes y Aplicaciones de Sistemas de Programación Orientada a Objetos (OOPSLA '10) . Association for Computing Machinery. págs. 341–360. CiteSeerX 10.1.1.205.2737 . doi :10.1145/1869459.1869489. ISBN .  9781450302036. Número de identificación del sujeto  207183083.
  13. ^ "La guía del neófito en Scala Parte 12: Clases de tipos - Daniel Westheide".
  14. ^ typelevel.org, Gatos de Scala
  15. ^ Castéran, P.; Sozeau, M. (2014). "Una introducción sencilla a las clases de tipos y relaciones en Coq" (PDF) . CiteSeerX 10.1.1.422.8091 . 
  16. ^ "Modelado de clases de tipos con argumentos de instancia".
  17. ^ Dreyer, Derek; Harper, Robert; Chakravarty, Manuel MT (2007). "Clases de tipos modulares". Actas del 34.º Simposio anual ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación (POPL '07). pp. 63–70. Véase p. 63. doi :10.1145/1190216.1190229. ISBN 978-1595935755.S2CID 1828213.TR  -2006-03.
  18. ^ "GHC/Familias de tipos - HaskellWiki".
  19. ^ Turon, Aaron (2017). "Especialización, coherencia y evolución de las API".

Enlaces externos