En el campo de la teoría de tipos en informática , un tipo cociente es un tipo de datos que respeta una relación de igualdad definida por el usuario . Un tipo cociente define una relación de equivalencia entre elementos del tipo; por ejemplo, podríamos decir que dos valores del tipo son equivalentes si tienen el mismo nombre; formalmente si . En las teorías de tipos que permiten tipos de cocientes, se establece un requisito adicional de que todas las operaciones deben respetar la equivalencia entre elementos. Por ejemplo, si es una función sobre valores de tipo , debe darse el caso de que para dos s y , si entonces .Person
p1 == p2
p1.name == p2.name
f
Person
Person
p1
p2
p1 == p2
f(p1) == f(p2)
Los tipos de cociente son parte de una clase general de tipos conocidos como tipos de datos algebraicos . A principios de la década de 1980, se definieron e implementaron tipos de cocientes como parte del asistente de prueba Nuprl , en un trabajo dirigido por Robert L. Constable y otros. [1] [2] Los tipos de cociente se han estudiado en el contexto de la teoría de tipos de Martin-Löf , [3] la teoría de tipos dependientes , [4] la lógica de orden superior , [5] y la teoría de tipos de homotopía . [6]
Para definir un tipo de cociente, normalmente se proporciona un tipo de datos junto con una relación de equivalencia en ese tipo, por ejemplo, Person // ==
donde ==
hay una relación de igualdad definida por el usuario. Los elementos del tipo cociente son clases de equivalencia de elementos del tipo original. [3]
Los tipos de cocientes se pueden utilizar para definir la aritmética modular . Por ejemplo, si Integer
es un tipo de datos de números enteros, se puede definir diciendo que si la diferencia es par. Luego formamos el tipo de números enteros módulo 2: [1]
Integer //
Se puede demostrar que las operaciones con números enteros +
están -
bien definidas en el nuevo tipo de cociente.
En las teorías de tipos que carecen de tipos de cocientes, a menudo se utilizan setoides (conjuntos explícitamente equipados con una relación de equivalencia) en lugar de tipos de cocientes. Sin embargo, a diferencia de los setoides, muchas teorías de tipos pueden requerir una prueba formal de que cualquier función definida en tipos de cocientes está bien definida . [7]
Los tipos de cociente son parte de una clase general de tipos conocidos como tipos de datos algebraicos . Así como los tipos de producto y los tipos de suma son análogos al producto cartesiano y la unión disjunta de estructuras algebraicas abstractas, los tipos de cociente reflejan el concepto de cocientes de teoría de conjuntos , conjuntos cuyos elementos se dividen en clases de equivalencia mediante una relación de equivalencia dada en el conjunto. Las estructuras algebraicas cuyo conjunto subyacente es un cociente también se denominan cocientes. Ejemplos de tales estructuras de cocientes incluyen conjuntos de cocientes , grupos , anillos , categorías y, en topología, espacios de cocientes . [3]