Hace algún tiempo en una de las extensiones de Haskell (no se puede encontrar el enlace), y recently in Ur Encontré que los nombres (por ejemplo, de los campos de registro) forman una especie. ¿Alguien puede explicar por qué la abstracción de tipos no es suficiente para ellos?¿Por qué los nombres forman un tipo y no solo un tipo?
La respuesta es simple: porque pueden aparecer en tipos. En consecuencia, tienen que vivir en el nivel de tipo (de lo contrario necesitaría tipos dependientes). Y debido a que viven en el nivel de tipo, se clasifican por tipo.
Los sistemas de registro definen reglas para valores, tipos y (tal vez) tipos. Las reglas que se usan dependen del tipo de sistema que se diseña y de lo que el diseñador desea lograr.
E.g. en Haskell, sellos discográficos son:
Record -> Int)*)Otros sistemas de registro puede use el tipo o el tipo de sistema para diferentes propósitos.
Al colocar las etiquetas en un tipo separado, el verificador de tipos puede tratarlas especialmente, con reglas especiales para, p. Ej. lentes automáticos, o pruebas que tienen que ver con la construcción de registros (tal vez la totalidad) no son ciertas para funciones de propósito general.
Un ejemplo del uso del sistema tipo en Haskell es el uso de "tipos no clasificados". Estos son los tipos que tienen:
para mantener tipos sin caja de mezcla en con regulares tipos, se les da un tipo diferente , que permite al compilador rastrear su separación.
Por lo tanto, no hay nada de mágico en los nombres de las etiquetas discográficas, lo que significa que debe usar un tipo diferente para representarlos, y en un lenguaje dependiente como Ur o En verdad, esa puede ser una distinción útil.
Gracias, el ejemplo sobre los tipos sin caja es esclarecedor – Fixpoint
Esta respuesta ha puesto todo en su lugar en mi cabeza. ¡Gracias! – Fixpoint