Clase de tipo - Type class

Este artículo trata sobre los sistemas de tipos polimórficos en informática. Para la clase de matemática de orden-tipos de una cardinalidad dada, ver Glosario de la teoría de conjuntos § T .
No confundir con clase (programación informática) .

En informática , una clase de tipos 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 a un tipo cuyos miembros admiten 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 , y originalmente se concibieron como una forma de implementar operadores aritméticos y de igualdad sobrecargados de una manera basada en principios. En contraste con los "eqtypes" del ML estándar, 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.

Desde su creación, se han descubierto muchas otras aplicaciones de clases de tipos.

Visión general

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 Eqde tipos destinada a contener tipos que admitan igualdad se declararía de la siguiente manera: 

class Eq a where
  (==) :: 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 ), lo que significa que el tipo de es TypeEq

Eq :: Type -> Constraint

La declaración puede leerse como si un "tipo apertenece a la clase de tipo Eqsi hay funciones nombradas (==)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) || elem y xs

La función elemtiene el tipo a -> [a] -> Boolcon el contexto Eq a, lo que restringe los tipos que apueden extenderse a los aque pertenecen a la Eqclase de tipos. ( Nota : Haskell => se puede llamar una 'restricción de clase').

Un programador puede hacer que cualquier tipo sea tmiembro de una clase de tipo dada Cmediante el uso de una declaración de instancia que define las implementaciones de todos Clos métodos 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 crea conveniente. Una vez hecho esto, pueden usar la función elemen [t], es decir, listas de elementos de tipo t.

Tenga en cuenta que las clases de tipos son diferentes de las clases en los 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 elemcomo se especificó 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, Type pero puede tomar una de cualquier tipo. Estas clases de tipos con tipos superiores a veces se denominan clases de constructores (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: 

class Monad m where
  return :: 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í: 

Monad :: (Type -> Type) -> Constraint

Clases de tipos de múltiples parámetros

Las clases de tipos permiten múltiples parámetros de tipos, por lo que las clases de tipos pueden verse como relaciones entre tipos. Por ejemplo, en la biblioteca estándar de GHC , la clase IArrayexpresa 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 usa para implementar tipos de matriz sin caja , por ejemplo).

Al igual que métodos múltiples , clases de tipo de múltiples parámetros admiten llamadas de diferentes implementaciones de un método en función de los tipos de argumentos múltiples, y de hecho volver tipos. Las clases de tipos de múltiples parámetros no requieren buscar el método para llamar en cada llamada en tiempo de ejecución; más bien, el método a llamar primero se compila y almacena en el diccionario de la instancia de clase de tipo, al igual que con las clases de tipo de parámetro único.

El código Haskell que usa clases de tipos de múltiples parámetros no es portátil, ya que esta característica no es parte del estándar Haskell 98. Las implementaciones populares de Haskell, GHC y Hugs , admiten clases de tipos de múltiples parámetros.

Dependencias funcionales

En Haskell, las clases de tipos se han refinado para permitir al programador declarar dependencias funcionales entre los parámetros de tipos, un concepto inspirado en la teoría de bases de datos relacionales . 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 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, 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 mse determina de forma única. Esto ayuda al compilador en la inferencia de tipos , así como al programador en la programación dirigida a tipos .

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

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 tipo como: 

sum :: Num a => [a] -> a

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

sum_ :: 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 bajo el capó).

Sin embargo, hay una diferencia crucial: los parámetros implícitos son más flexibles ; puede pasar diferentes instancias de Num Int. Por el contrario, las clases de tipos refuerzan la denominada propiedad de coherencia , que requiere que solo haya una opción única de instancia para cualquier tipo dado. La propiedad de coherencia hace que las clases de tipos sean algo antimodulares, por lo que se desaconsejan encarecidamente 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 agrega 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.

Como 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 en los elementos. Sin embargo, puede haber numerosas formas de imponer un orden total. Dado que los algoritmos de conjuntos generalmente no toleran 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 conducir a resultados incorrectos (o bloqueos). Por lo tanto, hacer cumplir la coherencia Ord aen este escenario particular es crucial.

Las instancias (o "diccionarios") en las clases de tipos de Scala son solo valores ordinarios en el lenguaje, en lugar de un tipo de entidad completamente separada. Si bien estas instancias se proporcionan de forma predeterminada al encontrar instancias apropiadas en el alcance para ser utilizadas como los parámetros reales implícitos para los 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 tipo 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: 

// A type class to provide textual representation
trait Show[A] {
  def show(f: A): String
}

// A polymorphic function that works only when there is an implicit 
// instance of Show[A] available
def log[A](a: A)(implicit s: Show[A]) = println(s.show(a))

// An instance for String
implicit val stringShow = new Show[String] {
  def show(s: String) = s
}

// The parameter stringShow was inserted by the compiler.
scala> log("a string")
a string

Coq (versión 8.2 en adelante) también admite clases de tipos al inferir las instancias apropiadas. Las versiones recientes de Agda 2 también ofrecen una función similar, denominada "argumentos de instancia".

Otros enfoques para la sobrecarga del operador

En ML estándar , el mecanismo de "tipos de igualdad" corresponde aproximadamente a la clase de tipos 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é tipo de variables en un rango de tipos polimórficos sobre 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 . El subconjunto orientado a objetos de OCaml es otro enfoque que es algo comparable al de las clases de tipos.

Nociones relacionadas

Una noción análoga para datos sobrecargados (implementada en GHC ) es la de familia tipográfica .

En C ++, en particular, C ++ 20 tiene soporte para clases de tipos que utilizan los conceptos (C ++) . Como ilustración, el ejemplo de Haskell mencionado anteriormente de ecuación de clase de tipos se escribiría como 

template <typename T>
concept Equal =
      requires (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.

Mercury tiene clases de tipos, aunque no son exactamente iguales a las de Haskell.

En Scala , las clases de tipos son un lenguaje de programación que se puede implementar con características de lenguaje existentes, como parámetros implícitos, no una característica de 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 una ventaja, ya que las instancias de clase de tipo 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 ordinarios, en Coq, cualquier ley de una clase de tipo (como las leyes de las mónadas) que se establecen dentro de la definición de la clase de tipo, debe probarse matemáticamente de cada instancia de clase de tipo antes de usarlas.

Ver también

Referencias

enlaces externos