Dudas sobre el comportamiento del Unit Type en un sistema de tipos

Question

Tengo una duda sobre el tipo de unidad en el contexto de la teoría de tipos y su uso en diferentes escenarios de casos.

Para empezar, un Tipo de unidad puede verse como un tipo de producto nulo, es decir, unidad, con un único término de valor que es la tupla vacía, ().Además, existe una único mapa de cualquier tipo a la Unidad.

Ahora bien, sucede que el uso del Tipo de Unidad va más allá de una definición tan trivial, y de hecho se utiliza en la definición de Tipos de Datos Algebraicos, que son Sumas de Tipos de Productos.En concreto, es posible representar el concepto de Tipo enumerado utilizando una suma de tipos de unidades, p.en StandardML podríamos tener:

datatype suit = HEARTS | CLUBS | DIAMONDS | SPADES

donde CORAZONES, Tréboles, DIAMANTES y ESPADAS son Tipos de Producto nulos y, por lo tanto, todos isomórficos a la Unidad.

Mi duda es la siguiente:Si existe solo un elemento de Unidad, ¿cómo puede el sistema de tipos distinguir entre las cuatro instancias distintas utilizadas en el Tipo de suma anterior (cinco instancias si también consideramos la tupla vacía...)?Entiendo que se pueden considerar todos iguales hasta el isomorfismo, pero son extensionalmente diferentes y de hecho, incluso considerando sólo los suit se supone que debemos hacer coincidir el patrón en ellos...

Answer 1

La respuesta corta es que los tipos isomórficos no son iguales, a pesar de comportarse de manera idéntica, por lo que el sistema de tipos puede distinguirlos.En un sistema de tipos nominales, como el que usted describe, los tipos se identifican esencialmente por sus nombres, incluso si son estructuralmente equivalentes.Este es el caso de los cinco tipos de unidades que usted describe:son estructuralmente equivalentes, pero nominalmente desiguales, por lo que se los trata como distintos.

Tenga en cuenta que el aspecto de coincidencia de patrones es ortogonal:se puede pensar que los cinco tipos de unidades existen de forma aislada.En la mayoría de las teorías de tipos, se puede tomar la suma de dos tipos cualesquiera, incluso dos que sean (nominalmente) iguales, p. Unit + Unit.Aún se le pedirá que coincida con el patrón y habrá dos casos:la izquierda Unit y el derecho Unit.El aspecto nominal no es importante, aunque muchos lenguajes de programación usarán los nombres para distinguir entre los diferentes casos como este, en lugar de los índices de los sumandos (en particular, en lenguajes donde solo se permite tomar sumas de distintos tipos nominales, como Estándar ML).