Positiva estrita

Desta referência: Estrita positividade

A estrita condição de positividade exclui declarações como

data Bad : Set where
 bad : (Bad → Bad) → Bad
         A      B       C
 -- A is in a negative position, B and C are OK

Por que A é negativo? Também porque B é permitido? Eu entendo por que C é permitido.

$A \Rightarrow B$$A$$B$

Agora, para tipos de dados indutivos.

$T$$T$$T$

Na álgebra, é habitual que uma operação use um número finito de argumentos e, na maioria dos casos, use zero (constante), um (unário) ou dois (binário). É conveniente generalizar isso para construtores de tipos de dados. Suponha que cseja um construtor para um tipo de dados T:

• se cé uma constante, podemos pensar nisso como uma função unit -> T, ou equivalente (empty -> T) -> T,
• se cé unário, podemos pensar nisso como uma função T -> T, ou equivalente (unit -> T) -> T,
• se cé binário, podemos pensar nisso como uma função T -> T -> T, ou equivalente T * T -> T, ou equivalente (bool -> T) -> T,
• se quiséssemos um construtor cque receba sete argumentos, poderíamos vê-lo como uma função em (seven -> T) -> Tque sevenhá algum tipo definido anteriormente com sete elementos.
• também podemos ter um construtor cque receba muitos argumentos, infinitamente, que seriam uma função (nat -> T) -> T.

Esses exemplos mostram que a forma geral de um construtor deve ser

c : (A -> T) -> T

onde chamamos Aa arity de ce pensamos ccomo um construtor que recebe Aargumentos -muitos do tipo Tpara produzir um elemento de T.

Aqui está algo muito importante: as aridades devem ser definidas antes de definirmos T, ou então não podemos dizer o que os construtores devem estar fazendo. Se alguém tentar ter um construtor

broken: (T -> T) -> T

então a pergunta "quantos argumentos são brokennecessários?" não tem boa resposta. Você pode tentar respondê-lo com "são necessários Tmuitos argumentos", mas isso não Tserve , porque ainda não está definido. Podemos tentar sair do cunundrum usando a teoria de ponto fixo sofisticada para encontrar um tipo Te uma função injetiva (T -> T) -> T, e teríamos sucesso, mas também quebraríamos o princípio da indução ao Tlongo do caminho. Portanto, é apenas uma má idéia tentar uma coisa dessas.

$\lambda$$v$$\lambda \cdot v$cB

c : B * (A -> T) -> T

Na verdade, muitos construtores pode ser reescrita dessa maneira, mas não todos, precisamos de mais um passo, ou seja, devemos permitir Aque dependem em B:

c : (∑ (x : B), A x -> T) -> T

Esta é a forma final de um construtor para um tipo indutivo. Também é precisamente o que são os tipos W. O formulário é tão geral que precisamos apenas de um único construtor c! De fato, se tivermos dois deles

d' : (∑ (x : B'), A' x -> T) -> T
d'' : (∑ (x : B''), A'' x -> T) -> T

então podemos combiná-los em um

d : (∑ (x : B), A x -> T) -> T

Onde

B := B' + B''
A(inl x) := A' x
A(inr x) := A'' x

By the way, se curry a forma geral, vemos que é equivalente a

c : ∏ (x : B), ((A x -> T) -> T)

que é mais próximo do que as pessoas realmente escrevem em assistentes de prova. Os assistentes de prova nos permitem escrever os construtores de maneira conveniente, mas esses são equivalentes à forma geral acima (exercício!).

A primeira ocorrência de Badé chamada 'negativa' porque representa um argumento de função, ou seja, está localizada à esquerda da seta da função (consulte Tipos recursivos gratuitamente por Philip Wadler). Eu acho que a origem do termo 'posição negativa' deriva da noção de contravariância ('contra' significa oposto).

Não é permitido que o tipo seja definido em posição negativa, porque é possível escrever programas não-terminativos usando-o, ou seja, uma forte normalização falha em sua presença (mais sobre isso abaixo). A propósito, esse é o motivo do nome da regra 'estrita positividade': não permitimos posições negativas.

Permitimos a segunda ocorrência de, Baduma vez que não causa terminação e queremos usar o tipo que está sendo definido ( Bad) em algum momento de um tipo de dados recursivo ( antes da última seta do construtor).

É importante entender que a seguinte definição não viola a regra estrita de positividade.

data Good : Set where
  good : Good → Good → Good

A regra se aplica somente aos argumentos do construtor (que são os dois Goodnesse caso) e não ao próprio construtor (consulte também " Programação Certificada com Tipos Dependentes ", de Adam Chlipala ).

Outro exemplo que viola uma estrita positividade:

data Strange : Set where
  strange : ((Bool → Strange) → (ℕ → Strange)) → Strange
                       ^^     ^
            this Strange is   ...this arrow
            to the left of... 

Você também pode verificar esta resposta sobre posições negativas.

Declarações não estritamente positivas são rejeitadas porque é possível escrever uma função não-terminadora usando-as. Para ver como é possível escrever uma definição de loop usando o tipo de dados Ruim acima, consulte BadInHaskell .

Aqui está um exemplo análogo no Ocaml, que mostra como implementar o comportamento recursivo sem (!) Usando a recursão diretamente:

type boxed_fun =
  | Box of (boxed_fun -> boxed_fun)

(* (!) in Ocaml the 'let' construct does not permit recursion;
   one have to use the 'let rec' construct to bring 
   the name of the function under definition into scope
*)
let nonTerminating (bf:boxed_fun) : boxed_fun =
  match bf with
    Box f -> f bf

let loop = nonTerminating (Box nonTerminating)

A nonTerminatingfunção "desempacota" uma função de seu argumento e a aplica ao argumento original. O que é importante aqui é que a maioria dos sistemas de tipos não permite a passagem de funções para si mesmos; portanto, um termo como f fnão será checado tipicamente, pois não há um tipo para fsatisfazer o checador tipográfico. Um dos motivos pelos quais os sistemas de tipos foram introduzidos é desativar a autoaplicação (veja aqui ).

O agrupamento de tipos de dados como o que introduzimos acima pode ser usado para contornar esse obstáculo no caminho para a inconsistência.

Quero acrescentar que cálculos não-térmicos introduzem inconsistências nos sistemas lógicos. No caso da Agda e da Coq, o Falsetipo de dados indutivo não possui construtores; portanto, você nunca pode criar um termo de prova do tipo False. Mas se cálculos não-terminantes fossem permitidos, seria possível, por exemplo, desta maneira (no Coq):

Fixpoint loop (n : nat) : False = loop n

Depois loop 0, verificava-se a doação loop 0 : False, portanto, sob a correspondência de Curry-Howard, isso significava que provávamos uma proposição falsa.

Resultado : a regra estrita de positividade para definições indutivas impede cálculos sem fim que são desastrosos para a lógica.