Dúvidas sobre o comportamento do Unit Type em um sistema de tipos

Question

Tenho uma dúvida sobre o Tipo de Unidade no contexto da Teoria dos Tipos e sua utilização em diferentes cenários de caso.

Para começar, um Tipo de unidade pode ser visto como um tipo de produto nulo, ou seja, Unidade, com um único termo de valor que é a tupla vazia, ().Além disso, existe um exclusivo mapear de qualquer tipo para a Unidade.

Ora, acontece que o uso do Tipo Unidade vai além dessa definição trivial, sendo de fato utilizado na definição de Tipos de Dados Algébricos, que são Somas de Tipos de Produtos.Especificamente, é possível representar o conceito de um Tipo Enumerado usando uma soma de tipos de unidades, por ex.no StandardML podemos ter:

datatype suit = HEARTS | CLUBS | DIAMONDS | SPADES

onde CORAÇÕES, PAUS, DIAMANTES e ESPADAS são tipos de produtos nulos e, portanto, todos isomórficos à unidade.

Minha dúvida é a seguinte:se existe apenas um elemento de Unit, como o sistema de tipos pode distinguir entre as quatro instâncias distintas usadas no Sum Type acima (cinco instâncias se considerarmos também a tupla vazia...)?Entendo que todos podem ser considerados iguais entre si até o isomorfismo, mas são extensionalmente diferentes e de fato, mesmo considerando apenas o suit devemos combinar padrões com eles...

Answer 1

A resposta curta é que os tipos isomórficos não são iguais, apesar de se comportarem de forma idêntica, e assim o sistema de tipos pode distingui-los.Em um sistema de tipos nominais, como o que você descreve, os tipos são essencialmente identificados por seus nomes, mesmo que sejam estruturalmente equivalentes.Este é o caso dos cinco tipos de unidades que você descreve:eles são estruturalmente equivalentes, mas nominalmente desiguais e, portanto, são tratados como distintos.

Observe que o aspecto de correspondência de padrões é ortogonal:você pode pensar nos cinco tipos de unidades como existindo isoladamente.Na maioria das teorias de tipos, você pode calcular a soma de quaisquer dois tipos, mesmo dois que sejam (nominalmente) iguais, por exemplo. Unit + Unit.Você ainda precisará fazer a correspondência de padrões e terá dois casos:a esquerda Unit e o certo Unit.O aspecto nominal não é importante, embora muitas linguagens de programação usem os nomes para distinguir entre os diferentes casos como este, em vez dos índices das somas (em particular, em linguagens onde você só pode tomar somas de tipos nominais distintos, como ML padrão).