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 . Una restricción de este tipo normalmente implica una clase de tipo Ty una variable de tipo a , y significa que asólo se puede crear una instancia de 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 haber sido 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 aritmética e igualdad sobrecargadas. operadores con base en principios. [3] [2] En contraste con los "eqtypes" de Standard ML, sobrecargar el 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]
Las clases de tipos se definen especificando un conjunto de funciones o nombres de 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 tipo 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 conocida como en la última versión de GHC ), [5] lo que significa que el tipo de esTypeEq
Eq :: Tipo -> Restricción Se puede leer que la declaración indica que "un tipo apertenece a la clase de tipo Eqsi hay funciones denominadas (==), y (/=), de los tipos apropiados, definidas en él". Luego, un programador podría 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 aquellos aque pertenecen a la Eqclase de tipo. ( Nota : Haskell => puede denominarse "restricción de clase").
Un programador puede convertir cualquier tipo ten miembro de una clase de tipo determinada Cutilizando una declaración de instancia que defina las implementaciones de todos Clos métodos para ese tipo en particular t. Por ejemplo, si un programador define un nuevo tipo de datos t, puede hacer de este nuevo tipo una instancia Eqproporcionando una función de igualdad sobre los valores de tipo tde la forma que considere adecuada. Una vez hecho esto, podrán utilizar la función elemon [t], es decir, listas de elementos de tipo t.
Tenga en cuenta que las clases de tipos son diferentes de las clases en lenguajes de programación orientados a objetos. En particular, Eqno es un tipo: no existe un valor de tipo Eq.
Las clases de tipos están estrechamente relacionadas con el polimorfismo paramétrico. Por ejemplo, tenga en cuenta que el tipo de 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 =>".
Una clase de tipo no necesita tomar una variable de tipo , Type pero puede tomar una de cualquier tipo. Estas clases de tipos con tipos superiores a veces se denominan clases constructoras (los constructores a los que se hace referencia son constructores de tipos como Maybe, en lugar de constructores de datos como Just). Un ejemplo es la Monadclase:
clase Mónada m donde retorno :: 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 de Monades así:
Mónada :: ( Tipo -> Tipo ) -> Restricción 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 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 matrices sin caja , por ejemplo).
Al igual que los métodos múltiples [ cita necesaria ] , las clases de tipos de parámetros múltiples admiten llamar a diferentes implementaciones de un método dependiendo de los tipos de múltiples argumentos y, de hecho, de los tipos de retorno. Las clases de tipos multiparámetro no requieren buscar el método para llamar en cada llamada en tiempo de ejecución; [7] : minuto 25:12 en lugar de eso, el método a llamar se compila primero y se almacena en el diccionario de la instancia de clase de tipo, al igual que con las clases de tipo de un solo parámetro.
El código Haskell que utiliza clases de tipos multiparámetro no es portátil, 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ámetro.
En Haskell, las clases de tipos se han refinado para permitir al programador declarar dependencias funcionales entre parámetros de tipos, un concepto inspirado en la teoría de bases de datos relacionales . [8] [9] Es decir, el programador puede afirmar que una asignación determinada de algún subconjunto de parámetros de tipo determina de forma única los parámetros de tipo restantes. Por ejemplo, una mónada general mque lleva un parámetro de estado de tipo ssatisface la restricción de clase de tipo Monad.State s m. En esta restricción, existe una dependencia funcional m -> s. Esto significa que para una mónada determinada mde tipo class Monad.State, el tipo de estado accesible desde mse determina 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 motivos de complejidad. [10]
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 tipo como:
suma :: Núm. 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 Haskell de Glasgow implementa las clases de tipos internamente).
Sin embargo, hay una diferencia crucial: los parámetros implícitos son más flexibles : puedes pasar diferentes instancias de Num Int. Por el contrario, las clases de tipos imponen la llamada propiedad de coherencia , que requiere que sólo haya una elección única de instancia para cualquier tipo determinado. La propiedad de coherencia hace que las clases de tipos sean algo antimodulares, por lo que se desaconsejan las instancias huérfanas (instancias que se definen en un módulo que no contiene la clase ni el tipo de interés). Por otro lado, la coherencia añade un nivel adicional de seguridad al lenguaje, proporcionando al programador la garantía de que dos partes separadas del mismo código compartirán la misma instancia. [11]
Como ejemplo, un conjunto ordenado (de tipo Set a) requiere un orden 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 en los elementos. Sin embargo, pueden existir numerosas formas de imponer un orden total. Dado que los algoritmos de conjuntos generalmente son intolerantes a los cambios en el orden una vez que se ha construido un conjunto, pasar una instancia incompatible de Ord aa funciones que operan en el conjunto puede generar resultados incorrectos (o fallas). Por lo tanto, Ord aes crucial hacer cumplir la coherencia en este escenario particular.
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 separada. [12] [13] Si bien estas instancias se proporcionan de forma predeterminada al encontrar instancias apropiadas en el alcance que se utilizarán 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 proporcionar 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 parámetros implícitos.
Este es un ejemplo tomado de la documentación de Cats [14] :
// Una clase de tipo para proporcionar un rasgo 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 )( implícita s : Show [ A ]) = println ( s . show ( a ) ) // Una instancia para String valor implícito stringShow = new Show [ String ] { def show ( s : String ) = s } // El compilador insertó el parámetro stringShow. 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". [dieciséis]
En Standard ML , el mecanismo de los "tipos de igualdad" corresponde aproximadamente a la clase de tipo incorporada 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 tipo polimórfico se extienden sobre 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, lo 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 algo comparable al de las clases de tipos.
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 que utilizan Concepts (C++) . A modo de ilustración, el ejemplo de clase de tipo Eq de Haskell mencionado anteriormente se escribiría como
plantilla < nombre de tipo T > concepto Igual = requiere ( T a , T b ) { { a == b } -> std :: convertible_to < bool > ; { a != b } -> std :: convertible_to < bool > ; }; En Clean, las clases de tipos 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 lenguaje de programación que se puede implementar con características del lenguaje existentes, como parámetros implícitos, no como 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 tipo 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 clases de tipos ambiguos 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 ordinarios, en Coq, cualquier ley de una clase de tipo (como las leyes de mónada) que se establece dentro de la definición de clase de tipo debe demostrarse matemáticamente para cada instancia de clase de tipo antes de usarla.
Monades un ejemplo de una clase de tipo)Data.Kindapareció en la versión 8 del compilador Haskell de Glasgow.