Clase de tipo

En informática , una clase de tipo es una construcción del sistema de tipos que admite el polimorfismo ad hoc en un lenguaje de programación . 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 tipoa , y significa que asolo se puede instanciar a un tipo cuyos miembros admitan las operaciones sobrecargadas asociadas con T.

Las clases de tipos se implementaron por primera vez en el lenguaje Haskell después de ser propuestas inicialmente por Philip Wadler y Stephen Blott como una extensión de eqtypesStandard ML , ^{[ 1 ] [ 2 ]} y fueron concebidas originalmente como una forma de implementar operadores aritméticos y de igualdad sobrecargados de manera sistemática. ^{[ 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 del frontend del compilador ni 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 pueden ser parametrizados; una clase de tipos Eqdestinada a contener tipos que admiten 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 Eq, y 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${\displaystyle *}$(${\displaystyle *}$también se conoce como Typeen la última versión del Glasgow Haskell Compiler (GHC), ^{[ 5 ]} lo que significa que el tipo de Eqes

Eq :: Tipo -> Restricción

La declaración puede interpretarse como que un "tipo apertenece a la clase de tipos Eqsi existen funciones con los nombres (==), y (/=), de los tipos apropiados, definidas en él". 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 a aquellos aque pertenecen a la Eqclase de tipos. (Haskell =>puede denominarse una 'restricción de clase').

Cualquier tipo tpuede convertirse en miembro de una clase de tipo determinada Cmediante una declaración de instancia que defina las implementaciones de todos los Cmétodos de para el tipo dado t. Por ejemplo, si se define un nuevo tipo de datos t, este nuevo tipo puede convertirse en una instancia Eqproporcionando una función de igualdad sobre valores de tipo tde cualquier forma 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 tipos son diferentes de las clases en los lenguajes de programación orientados a objetos . Específicamente, Eqno es un tipo: no existe tal cosa como 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 si no fuera por la restricción de clase de tipo " ".a -> [a] -> BoolEq a =>

Una clase de tipo no necesita tomar una variable de tipo de tipoType , sino que puede tomar 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 Monad m donde return :: a -> m a ( >>= ) :: m a -> ( a -> m b ) -> m b

Eso mse aplica a una variable de tipo indica que tiene tipo Type -> Type, es decir, toma un tipo y devuelve un tipo, el tipo de Monades, por lo tanto:

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

Las clases de tipos permiten múltiples parámetros de tipo , por lo que pueden considerarse 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 sin empaquetar , por ejemplo).IArrayIArray a eae

Al igual que los multimétodos , las clases de tipos con múltiples parámetros admiten la llamada a diferentes implementaciones de un método dependiendo de los tipos de múltiples argumentos, e incluso de los tipos de retorno. Las clases de tipos con múltiples parámetros no requieren buscar el método a llamar en cada llamada en tiempo de ejecución; ^{[ 7 ] : minuto 25:12} en lugar de que el método a llamar se compila primero y se almacena en el diccionario de la instancia de la clase de tipo, al igual que con las clases de tipos de un solo parámetro.

El código Haskell que utiliza clases de tipos con múltiples parámetros no es portable según el estándar Haskell 98, que no es el más reciente. Las implementaciones más populares de Haskell, GHC y Hugs , sí admiten clases de tipos con múltiples pará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ónadam 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 motivos 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 tipo como por ejemplo:

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 Compiler implementa internamente las clases de tipos).

Sin embargo, existe una diferencia crucial: los parámetros implícitos son más flexibles ; se pueden pasar diferentes instancias Num Int. En cambio, las clases de tipos imponen la llamada propiedad de coherencia , que requiere que solo haya una única instancia para cada tipo. La propiedad de coherencia hace que las clases de tipos sean algo antimodulares, razón por la cual se desaconsejan encarecidamente las instancias huérfanas (instancias definidas en un módulo que no contiene ni la clase ni el tipo de interés). No obstante, la coherencia añade un nivel adicional de seguridad a un lenguaje, garantizando que dos partes disjuntas del mismo código compartan la misma instancia. ^{[ 11 ]}

Por ejemplo, un conjunto ordenado (de tipo Set a) requiere un orden total en los elementos (de tipo a) para funcionar. Esto se evidencia mediante una restricción Ord a, que define un operador de comparación en los elementos. Sin embargo, existen numerosas maneras de imponer un orden total. Dado que los algoritmos de conjuntos generalmente no toleran cambios en el orden una vez construido el conjunto, pasar una instancia incompatible de Ord aa funciones que operan sobre el conjunto puede generar resultados incorrectos (o fallos). Por lo tanto, garantizar 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 del lenguaje, en lugar de una entidad completamente independiente. ^{[ 12 ] [ 13 ]} Si bien estas instancias se proporcionan por defecto 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 pueden proporcionarse explícitamente para resolver ambigüedades. Como resultado, las clases de tipos de Scala no satisfacen la propiedad de coherencia y son, en efecto, 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 representación textual trait 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 implicit 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

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

En Standard ML , el mecanismo de "tipos de igualdad" se corresponde aproximadamente con la clase de tipo integrada de Haskell Eq, pero todos los operadores de igualdad son derivados automáticamente por el compilador. El control del programador sobre el proceso 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 los tipos de igualdad.

Los módulos y functores 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, en cierto modo, 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 en C++20 , se admite el uso de clases de tipos mediante " conceptos ". A modo de ilustración, el ejemplo de clase de tipos de Haskell mencionado anteriormente Eqse implementaría de la siguiente manera:

usando std :: convertible_to ;// equivalente a std::equality_comparable template < typename T > concept EqualityComparable = requires ( T a , T b ) { { a == b } -> convertible_to < bool > ; { a != b } -> convertible_to < bool > ; };// usando el concepto EqualityComparable: plantilla < EqualityComparable T > [[ nodiscard ]] constexpr bool isEqual ( const T & x , const T & y ) noexcept { return x == y ; }

En Go , una interfaz puede verse como una clase de tipo, y es aproximadamente equivalente a un concepto de C++. ^{[ 19 ]}

En Java y C# , las interfaces son similares a las clases de tipos, ya que definen una "interfaz" de métodos a implementar (véase Interfaces de Java ).

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

Rust admite rasgos , que son una forma limitada de clases de tipos con coherencia, y también pueden verse como similares a las interfaces . ^{[ 20 ]}

Mercury tiene clases de tipos, aunque no son exactamente iguales que en Haskell.

En Scala , las clases de tipos son un patrón de programación que se puede implementar con características del lenguaje ya existentes, como los parámetros implícitos, y no una característica del lenguaje en sí misma. Debido a su implementación en Scala, es posible especificar explícitamente qué instancia de clase de tipos usar para un tipo en un punto específico del código, en caso de ambigüedad. Sin embargo, esto no siempre es una ventaja, ya que las instancias de clases de tipos ambiguas pueden generar errores.

El asistente de pruebas Rocq también ha incorporado clases de tipos en sus versiones recientes. A diferencia de los lenguajes de programación convencionales, en Rocq, cualquier ley de una clase de tipos (como las leyes de las mónadas) que se especifique en la definición de la clase debe demostrarse matemáticamente para cada instancia de la clase antes de su uso.

• "5. Clases de tipos y sobrecarga" . Una introducción sencilla a Haskell . Junio ​​de 2000. Versión 98.
• Curso avanzado de programación funcional en la Universidad de Utrecht, 74 diapositivas de clase sobre clases de tipos avanzadas . 7 de junio de 2005.
• Implementación y comprensión de las clases de tipos . 13 de noviembre de 2014.