Os literais em linguagens funcionais podem ser pensados ​​como funções do tipo vazio?

Há um tempo atrás, penso no Stack Overflow, vi alguém dizer que os literais de Haskell podem ser pensados ​​como funções que não operam em nada. Isso faz sentido para mim, mas eu lembro de outra pessoa que discorda veementemente dele.

Se bem entendi, todos os valores em tipos primitivos, ou pelo menos aqueles em Bool, são construtores de tipo e construtores de tipo são um tipo especial de função para o tipo. Desde valores gostar 2.87, Trueou 'f'não tem quaisquer parâmetros passados para eles parece que ele não teria efeito a semântica da língua se você pensa deles, assim como elementos de seu tipo ou funções de um tipo contendo nada em seu tipo que sempre retorna seu valor. Há algo de errado em pensar em literais dessa maneira?

Vamos começar em um idioma total como o Agda. Então, como afirma Gallais, isso só faz sentido se, por "tipo vazio", você quer dizer o tipo de unidade, ou seja, a tupla 0-ária, que tem exatamente um valor. O tipo vazio pode ser pensado como um tipo de soma de maiúsculas e minúsculas e não possui nenhum valor. No Agda, você pode facilmente provar que isso Unit -> Aé isomórfico A. Nesse sentido, você pode considerá-los iguais, embora ainda não sejam literalmente iguais. Não posso, por exemplo, fazer uma análise de caso Unit -> Boolnem aplicar True : Boola nada como uma função.

A história para Haskell é bem diferente. () -> Ae Asão tipos semanticamente não isomórficos. Em particular, () -> ()tem quatro valores, enquanto ()tem apenas 2. Os quatro observacionalmente distintos valores são undefined, \_ -> undefined, \x -> x, \_ -> (). Portanto, ()não é realmente um tipo de unidade, no sentido de que existe exatamente uma função (). (Na Agda, por outro lado, podemos provar que se x : Unite y : Unit, então, são iguais [definicionalmente, se definirmos Unitcom a recordsintaxe em oposição à datasintaxe]. Isso significa que Unittem apenas um valor. Além disso, podemos provar que Unite A -> Unitsão isomórficos para qualquer um A.)

De fato, um tipo "vazio", como Voiddefinido, data Voidestá mais próximo de ser um tipo de unidade nesse sentido. Voidtem apenas um valor, mas Void -> Voidainda tem dois. De fato, todo tipo de função A -> Btem pelo menos dois valores observacionalmente distintos, a saber, undefinede \_ -> undefined. Portanto, Haskell não possui uma unidade verdadeira ou um tipo de vazio.

Muito disso se deve ao fato de Haskell ser uma linguagem não estrita e é exasperada pela existência de seq(e seus equivalentes). Por exemplo, a distinção entre undefinede \_ -> undefinedsó pode ser vista com seq. Se eliminássemos seqe seus equivalentes de Haskell, Voidserviríamos como um tipo de unidade, embora, ironicamente, ainda não fosse um tipo vazio.

Geralmente, quando as pessoas falam sobre essas coisas em Haskell, elas estão fingindo tacitamente que Haskell é uma linguagem mais bem comportada do que é. Ou seja, eles assumem que os fundos não existem para seus propósitos, ou seja, você está trabalhando em um idioma total como o Agda. Para os propósitos de projetar seu código, isso geralmente é adequado; não é comum nos preocuparmos ou esperarmos fundos. Essas distinções podem se tornar importantes se estivermos fazendo algo como programação circular ou se as garantias de segurança de nosso programa dependem dessas propriedades, por exemplo, uma função nunca pode ser chamada se tiver um tipo vazio como domínio.