Tipo de cociente

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.${\displaystyle \equiv }$sobre elementos del tipo — por ejemplo, podríamos decir que dos valores del tipo Pointson equivalentes si tienen las mismas coordenadas x e y respectivas; formalmente p1 == p2si p1.x == p2.x && p1.y == p2.y. En las teorías de tipos que permiten tipos cociente, se exige además que todas las operaciones respeten la equivalencia entre elementos. Por ejemplo, si fes una función sobre valores de tipo Point, debe cumplirse que para dos Pointy p1, p2si p1 == p2entonces f(p1) == f(p2).

Los tipos cociente forman parte de una clase general de tipos conocidos como tipos de datos algebraicos . A principios de la década de 1980, los tipos cociente se definieron e implementaron como parte del asistente de pruebas Nuprl , en un trabajo liderado por Robert L. Constable y otros. ^{[ 1 ] [ 2 ]} Los tipos 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 homotópicos . ^{[ 6 ]}

Para definir un tipo cociente, normalmente se proporciona un tipo de datos junto con una relación de equivalencia sobre ese tipo, por ejemplo, Point // ==, donde ==es 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 cociente se pueden usar para definir aritmética modular . Por ejemplo, si Integeres un tipo de datos de enteros,${\displaystyle \equiv _{2}}$se puede definir diciendo que${\displaystyle x\equiv _{2}y}$si la diferencia${\displaystyle xy}$es par. Entonces formamos el tipo de enteros módulo 2: ^{[ 1 ]}

Integer //${\displaystyle \equiv _{2}}$

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 cociente, a menudo se utilizan setoides (conjuntos equipados explícitamente con una relación de equivalencia) en lugar de tipos cociente. 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 cociente está bien definida . ^{[ 7 ]}

Los tipos cociente forman parte de una clase general de tipos conocidos como tipos de datos algebraicos . Así como los tipos producto y los tipos suma son análogos al producto cartesiano y la unión disjunta de estructuras algebraicas abstractas, los tipos cociente reflejan el concepto de cocientes conjuntistas , 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 cociente incluyen conjuntos cociente , grupos , anillos , categorías y, en topología, espacios cociente . ^{[ 3 ]}

• Tipo de datos algebraicos
• Tipo de producto
• Setoid
• Tipo de suma