Eu sei como algumas ocorrências negativas podem definitivamente ser ruins:
data False
data Bad a = C (Bad a -> a)
selfApp :: Bad a -> a
selfApp (x@(C x')) = x' x
yc :: (a -> a) -> a
yc f = selfApp $ C (\x -> f (selfApp x))
false :: False
false = yc id
No entanto, não tenho certeza se:
todos os tipos indutivos com ocorrências negativas podem ficar errados;
nesse caso, existe uma maneira mecânica conhecida de fazê-lo;
Por exemplo, eu tenho lutado tentando fazer esse tipo dar errado:
type Not a = a -> False
data Bad2 a = C2 (Bad2 (Not a) -> a)
Qualquer indicação para a literatura sobre este assunto seria apreciada.
lo.logic
type-theory
soundness
Ptival
fonte
fonte
Respostas:
A razão para a proibição de ocorrências negativas pode ser entendida por analogia com o teorema de Knaster-Tarski. Este teorema diz que
Na teoria tradicional dos modelos, as redes podem ser vistas como proposições, e a relação de ordem pode ser entendida como implicação (isto é, que a verdade de é implicada pela verdade de ).p ≤ q q peu p ≤ q q p
Quando passamos da teoria do modelo para a teoria da prova, as treliças generalizam para categorias. Tipos pode ser visto como os objectos de uma categoria , e um mapa representa uma prova de que pode ser derivada a partir de . e : P → Q Q QC e:P→Q Q Q
Quando tentamos interpretar tipos definidos por equações recursivas, ee, , a coisa mais óbvia a fazer é procurar uma generalização do teorema de Knaster-Tarski. Portanto, em vez de uma função monótona em uma rede, sabemos que queremos um functor , que envia objetos para objetos, mas generaliza a condição de monotonicidade para que todo mapa obtém um mapa (com as condições de coerência que envia identidades para identidades e preserva composições de modo que ).F : C → C e : P → Q F ( e ) : F ( P ) → F ( Q ) F F ( g ∘ f ) = F ( g ) ∘ F ( f )N=μα.1+α F:C→C e:P→Q F(e):F(P)→F(Q) F F(g∘f)=F(g)∘F(f)
Portanto, se você deseja um tipo de dados indutivo , também precisará fornecer uma ação funcional nos termos do operador de tipo para garantir que o ponto fixo desejado exista. A condição estrita de positividade em Agda e Coq é uma condição sintática que implica essa restrição semântica . Em termos gerais, diz que, se você criar um operador de tipo a partir de somas e produtos, poderá sempre preparar a ação funcional, e assim qualquer tipo formado dessa maneira deve ter um ponto fixo.Fμα.F(α) F
Em idiomas de tipo dependente, você também tem tipos indexados e com parâmetros, portanto sua tarefa real é mais complicada. Bob Atkey (que escreveu um blog sobre isso aqui e aqui ) me diz que um bom lugar para procurar a história é:
Como observa Andrej, fundamentalmente, se uma ocorrência negativa é boa ou não, depende de qual é o seu modelo de teoria dos tipos. Basicamente, quando você tem uma definição recursiva, está procurando um ponto fixo, e há muitos teoremas de ponto fixo em matemática.
Um dos quais eu pessoalmente fiz muito uso é o teorema do ponto fixo de Banach, que diz que se você tem uma função estritamente contrativa em um espaço métrico, então ele tem um ponto fixo exclusivo. Essa idéia foi introduzida na semântica por (IIRC) Maurice Nivat, e foi extensivamente estudada pela America e Rutten, e foi recentemente conectada por Birkedal e seus colaboradores a uma técnica operacional popular chamada "indexação por etapas".
Isso gera teorias de tipos em que ocorrências negativas em tipos recursivos são permitidas, mas somente quando as ocorrências negativas ocorrem sob um construtor de tipo especial de "proteção". Essa idéia foi introduzida por Hiroshi Nakano, e a conexão com o teorema de Banach foi feita por mim e por Nick Benton, além de Lars Birkedal e seus co-autores.
fonte
Às vezes, você pode resolver equações recursivas "por sorte".
Suponho que você queira fazer isso em conjuntos (em oposição a algum tipo de teoria de domínio). Se desdobrarmos sua definição e escrevermos a equação diretamente sem anotações de Haskell, obteremos Vamos considerar dois casos:
Se é habitado, ou seja, contém algo, então , portanto, a equação se reduz a E, de fato, o conjunto singleton resolve a equação.A A→∅≅∅
Se estiver vazio, obteremos .A ∅≅(∅→∅)→∅≅1→∅≅∅
Conclusão: existem duas soluções, o tipo vazio (que você chamou
False
) e o tipo de unidade()
.Aqui está outro exemplo interessante: ou em Haskell
Em termos de conjuntos, isso é . Pelo teorema de Cantor, não há solução, pois possui menos elementos que . No entanto, se observarmos essa equação em espaços topológicos, haverá uma solução, a saber Isso ocorre porque é o espaço Cantor, é o espaço de seus subconjuntos clopen, dos quais existem muitos (e você deve pensar para ver isso eles formam um espaço discreto). Da mesma forma, você pode exibir uma bijeção entre e em Haskell.A≅22A A 22A
Integer
(Integer -> Bool) -> Bool
fonte
É difícil acrescentar algo às explicações de Andrej ou Neel, mas vou tentar. Vou tentar abordar o ponto de vista sintático, em vez de tentar descobrir a semântica subjacente, porque a explicação é mais elementar e darei uma resposta mais direta à sua pergunta.
Eu estou indo para o trabalho no simplesmente tipado -calculus ao invés do sistema mais complexo subjacente Haskell. Eu acredito em particular que a presença de variáveis de tipo pode estar confundindo você até certo ponto.λ
A referência crucial é a seguinte:
Mendler, N. (1991). Tipos indutivos e restrições de tipo no cálculo lambda de segunda ordem. Não encontrei uma referência online, receio. As declarações e provas podem, no entanto, ser encontradas na tese de doutorado de Nax (uma leitura altamente recomendada!).
Mendler explica que a positividade é uma condição necessária e suficiente para o término na presença de definições de caso não recursivas (e definições recursivas estruturalmente decrescentes). Ele afirma usando uma formulação equacional . Dou um exemplo simples, que é uma simplificação do seu tipo .Bad
Onde é qualquer tipo. Temos entãoA
e entao
Mendler mostra que isso pode ser realizado para qualquer tipo que é um tipo com pelo menos uma ocorrência negativa de (também pode haver ocorrências positivas) . Ele fornece um termo explícito que não termina com um (páginas 39-40 de sua tese).
É claro que você está trabalhando não com tipos definidos equacionalmente, mas com construtores , ou seja, você tem
ao invés de estrita igualdade. No entanto, você pode definir
o que é suficiente para que esse resultado continue mantendo:
Este termo ainda é bem digitado do tipo .A
No seu segundo exemplo, as coisas são um pouco mais complicadas, pois você tem algumas coisas ao longo das linhas de
onde está relacionado , mas não igual, ao (no seu caso, eles são iguais a e respectivamente). Admito que não consegui construir um isomorfismo direto entre os dois. O mesmo problema está presente se você substituirB um d B um d um B um d ( N O t um)Bad′ Bad Bad a Bad (Not a)
com
Seria facilmente resolvido se Haskell permitisse essas definições de tipo:
Nesse caso, você pode criar um combinador de loop exatamente da mesma maneira que antes. Eu suspeito que você pode realizar uma construção semelhante (mas mais complexa) usando
O problema aqui é que, para construir um isomorfismo
você tem que lidar com variância mista.
fonte