Curry-Howard, void e verificação de tipos em Haskell

Question

Estou tentando entender um exemplo de prova de teorema via verificação de tipo em Haskell dado aqui . O exemplo é o seguinte.

Usando o isomorfismo de Curry-Howard, construa um habitante do tipo e prove que $N= (A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow ((\neg B\& A)\vee ((A\rightarrow B)\&(B\rightarrow A)))$ detém.

O autor fornece o seguinte código.

data Void
nnot :: Void -> a
nnot = undefined
proposition :: (Either a (b -> a), (c, c -> b)) -> Either (Void -> b, a) (b -> a)
proposition (Left x, (y, f)) = Left (nnot, x)
proposition (Right g, (y,f)) = Left (nnot, (g (f y)))

A implicação $(A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow (\neg B \& A)$não segura. Mas o termo construído é afirmado como prova disso, e o verificador de tipo fica satisfeito com ele. Por quê?

Acho que a transcrição das fórmulas iniciais para o tipo de propositionestá incorreta, pois a negação de bé representada com o Void -> bque está o absurdo (e é definido como nnot). Ou seja, do ponto de vista lógico, o par (Void -> b, a)corresponde ao termo$\bot \& A$. Mas isso não dá uma resposta por que o verificador de tipo verifica o código acima. Portanto, aprecio muito qualquer sugestão sobre as duas perguntas a seguir.

1. Por que o compilador Haskell aprova o tipo de proposition?
2. Se for esse o caso quando Curry-Howard não estiver em vigor, como posso realmente usar o verificador de tipos para provar fórmulas com negação via Curry-Howard?

Não sei se esta pergunta é mais apropriada em cs ou stackoverflow, então, por favor, desculpe se não estiver no tópico.

EDITAR: Dada a seguinte proposição corrigida:

proposition :: (Either a (b -> a), (c, c -> b)) -> Either (b -> Void, a) (b -> a)

Eu escrevi a seguinte "prova" para isso, e o verificador de tipo ficou satisfeito. Não sei se posso acreditar que a proposição pode ser considerada como tendo sido provada após a verificação de tipo.

proposition (Left x, (y, f)) = Right ((\z1 z2 -> z1) x)
proposition (Right g, (y,f)) = Right ((\z1 z2 -> z1) (g (f y))) 

E ainda não tenho ideia se é possível provar alguma negação pelo procedimento de verificação de tipo.

Edit2: Achei que tinha entendido o assunto, mas tentei o seguinte:

prop1 :: ((Either a b), c) -> b
prop1 (Right x, y) = x

Este código está OK para Haskell (por exemplo, lá ). Mas parece ser mal tipificado do ponto de vista da lógica: o tipo correspondente é$(A\vee B)\& C\rightarrow B$. É óbvio que o caso dado em prop1(Right x, y) = xtem o tipo certo (heh), mas não defini o caso para prop1(Left x, y), portanto, a proposição não está provada para este caso. Portanto, também posso ter problemas com a disjunção.

Answer 1

Eu encontraria um tutorial diferente porque o autor daquele está fundamentalmente confuso. Eles erroneamente afirmam que$\neg a$ e $\bot\to a$ são equivalentes ($a\to\bot$ estaria correto), e também alegue erroneamente que você não pode escrever uma função do tipo $\texttt{Void}\to a$.

$\texttt{Void}\to a$é vacuamente verdadeiro. Em princípio, uma função desse tipo não deve exigir nenhuma definição porque o número de casos para os quais você precisa defini-la é zero. GHC não aceita isso, mas (com -XEmptyCase) aceita

f :: Void -> a
f x = case x of {}

que é uma definição perfeitamente válida e lógica.

Por que o compilador Haskell aprova o tipo de proposição?

A proposição conforme escrita no código Haskell é realmente verdadeira. A prova é inválida, pois usa$\texttt{undefined}$.

Se você substituiu o lado direito por $(b\to\texttt{Void},a)$ então seria falso, mas você ainda poderia "provar" usando $\texttt{undefined}$; na verdade você poderia apenas escrever$\texttt{proposition} = \texttt{undefined}$e o verificador de tipo aceitaria isso. Também aceitaria$\texttt{proposition} = \texttt{proposition}$. Se você quiser usar Haskell como um sandbox Curry-Howard, você deve tomar cuidado para que seu código não lance uma exceção ou falhe ao terminar, porque o compilador não detectará esses erros.

---

Resposta à edição: sua prova está correta, mas pode ser simplificada. No primeiro caso, não há necessidade de criar uma função e aplicá-la imediatamente a um de seus argumentos. Em vez de (\z1 z2 -> z1) xvocê pode escrever \z2 -> x, ou \_ -> xdesde que o argumento / premissa não seja usado. No segundo caso, você não precisa provar, b -> apois já o fez g :: b -> a. A prova simplificada é

proposition (Left x, _) = Right (\_ -> x)
proposition (Right g, _) = Right g

Além das armadilhas que Dan Doel mencionou em um comentário, casos perdidos são outra coisa a se observar. O GHC por padrão nem avisa sobre eles. Com -Werror=incomplete-patternsele se recusará a aceitar programas com casos perdidos.

Você pode provar negações. Você precisa retornar um valor do tipo$\texttt{Void}$, que você não pode criar sozinho, mas pode obter de outro lugar. Por exemplo, aqui está uma prova de$((P\Rightarrow Q) \mathbin{\&} \neg Q)\Rightarrow \neg P$:

f :: (a -> b, b -> Void) -> (a -> Void)
f (x, y) = \z -> y (x z)

Você pode se perguntar de onde o chamador obteve o valor do tipo $\texttt{Void}$, mas isso é problema de quem ligou, não seu. Derivar uma contradição em uma subprova não significa que a lógica é inconsistente, apenas significa que você mostrou que nunca chegará realmente a esse ponto no mundo real.