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 polimórficos paramétricos . 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 necesita 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 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 Glasgow Haskell Compiler (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, lo que restringe los tipos que apueden abarcar hasta aquellos aque pertenecen a la Eqclase de tipo. (Haskell => puede denominarse una "restricción de clase").
Cualquier tipo tpuede convertirse en 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 tse define un nuevo tipo de datos, este nuevo tipo puede convertirse en una instancia de Eqproporcionando una función de igualdad sobre los valores de tipo tde cualquier manera que sea útil. Una vez hecho esto, la función elempuede utilizarse en [t], es decir, listas de elementos de tipo t.
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, 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 =>".
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 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 tipo permiten múltiples parámetros de tipo, por lo que las clases de tipo pueden verse como relaciones entre tipos. [6] Por ejemplo, en la biblioteca estándar de GHC , la clase expresa una interfaz de matriz inmutable general. En esta clase, la restricción de clase de tipo significa que es un tipo de matriz que contiene elementos de tipo . (Esta restricción de polimorfismo se utiliza para implementar tipos de matriz no encapsulados , por ejemplo).IArrayIArray a eae
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.
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]
Las clases de tipos y los parámetros implícitos son muy similares en naturaleza, 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 requiere 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. Sin embargo, la coherencia agrega otro nivel de seguridad a un lenguaje, brindando 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 forma predeterminada al encontrar instancias apropiadas en el ámbito para ser utilizadas como parámetros 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]
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.
Una noción análoga para datos sobrecargados (implementada en GHC ) es la de familia de tipos . [18]
En C++ , especialmente C++20 , se admiten clases de tipos mediante el uso de Conceptos (C++) . A modo de ejemplo, 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.
Data.Kindapareció en la versión 8 del compilador Glasgow Haskell