No isomorfismo de Curry-Howard, aplicado aos tipos de Hindley-Milner, que proposição corresponde a -> [a]?

(Usando a sintaxe Haskell, já que a pergunta é inspirada em Haskell, mas se aplica a sistemas polimórficos gerais de Hindley-Milner, como SML ou Elm).

Se eu tiver uma assinatura de tipo f :: a -> [a], qual é a proposição lógica codificada por essa assinatura de tipo?

Eu sei que tipo de construtores gosto ->, (,)correspondem a "operações" em sua lógica: ->corresponde ao "implica" símbolo$\rightarrow$.

Suponho que também []seja um construtor de tipos e tenho a sensação de que a resposta pode ter algo a ver com sua definição recursiva, que eu sei que poderia ser implementada como algo como:

data List a = Cons a (List a) | Nil

mas não tenho certeza do que isso significa no versículo lógico.

Uma maneira de interpretar tipos como lógica é como as condições de existência para valores do tipo de retorno. Então f :: a -> [a], o teorema de que, se existe um valor de tipo a, existe um valor de tipo [a]. A implementação da função é a prova da proposição.

Aqui está uma explicação mais detalhada:

Basicamente, os construtores de dados permitem criar coisas semelhantes a somas e produtos (OR e AND), mas podemos ter várias variantes e podemos "marcar" especialmente o tipo com um nome para distingui-lo (como o nome List).

Eles também nos permitem construí-los recursivamente: para uma proposição $a$, a proposição $[a]$ pode ser visto como uma solução para a equação $x(a) \iff \top \vee (a \wedge x(a) )$

As coisas ficam um pouco mais claras quando você escreve a definição de Lista usando o estilo GADT, pseudocódigo semelhante ao que você vê no Agda:

data List : Type -> Type where
    Nil : ∀ a . List a
    Cons : ∀ a . a -> List a -> List a

Isso nos dá duas coisas: os construtores (ou funções), que atuam como axiomas para as proposições de List, e axiomas para correspondê-los ou desconstruí-los.

Grosso modo, ele introduz os seguintes axiomas na lógica:

• Para qualquer proposição $a$, $[a]$ detém.
• E se $a$ detém e $[a]$ segura, então $[a]$ detém
• E se $[a]$ mantém, então $\top$ detém, ou $a \wedge [a]$ detém.

Estes são bastante inúteis quando interpretados como lógicos, pois sempre sabemos $\top$ desconstruir não nos fornece muita informação útil

Sem quantificadores ou extensões de tipo mais poderosas (GADTs, famílias de tipos, tipos dependentes etc.), você pode ver que não podemos realmente provar coisas interessantes, e é por isso que muitas vezes você não vê muito sobre a interpretação de tipos padrão Haskell como lógica .

Os tipos de lista são um pouco estranhos como proposição. Eles realmente não correspondem a nada diretamente familiar, mas é fácil ver o que são equivalentes. Como não existe, você sempre pode provar [a]para qualquer aum desses tipos de lista sempre é muito fácil de provar, em particular eles são trivialmente equivalentes a qualquer tautologia que já foi comprovada. Portanto, apresentá-los é um pouco desinteressante. Além disso, a regra de eliminação tem um problema. Ou seja, você precisa provar algo []para eliminar uma lista que não oferece novas suposições. Assim, geralmente posso transformar qualquer prova usando uma eliminação de lista em uma prova que não a utiliza. No entanto, talvez eu saiba algo sobre a lista que contradizia que ela estivesse vazia e, nesse caso, é muito mais interessante.

Então, na maioria das vezes, é meio chato, mas outras vezes é realmente um pouco interessante, graças à relevância da prova. No entanto, Haskell não tem relevância para provas, portanto, nas listas Haskell são apenas chatas.

Em certo sentido (estou enganando as coisas aqui), as listas em Haskell correspondem a algo que é equivalente ao operador booleano constantemente verdadeiro. Portanto, não nega um valor booleano, o id mantém o mesmo e a coisa que a lista se comporta como sempre é verdadeira, independentemente do que você conectar a ela.