Significado de "posição positiva" e "posição negativa" na teoria dos tipos?

O que "em posição positiva" e "em posição negativa" significa no contexto da teoria dos tipos?

A única coisa que entendi no post de Bob Harper sobre o tema é que há uma conexão entre polaridade nesse sentido na teoria dos tipos e polaridade na lógica, mas não sei qual é essa conexão.

Infelizmente, "polaridade" é um conceito um pouco sobrecarregado na teoria dos tipos. "Posição positiva" e "posição negativa" referem-se a uma noção diferente de polaridade do que o que Bob está falando com foco / polarização.

Seu significado

Ao definir um tipo indutivo, você fornece uma série de regras que correspondem às operações para o tipo que você está definindo. Por exemplo, você pode dizer que a Naté algo com

• um valor zero : Nat
• uma função suc : Nat -> Nat

E então espere que Natcontenha todos os valores que podem ser gerados da aplicação repetida suca outros se Natinclui zero. De acordo com essa construção indutiva, obtemos um princípio de recursão entre Nats, que funciona com base no fato de que qualquer um Naté gerado por esses construtores.

rec : A -> (A -> A) -> Nat -> A

de modo a

rec Z S zero = zero
rec Z S (suc n) = S (rec Z S n)

No entanto, existem algumas restrições sobre o que podemos escrever como regras. Caso contrário, podemos escrever uma série de regras para as quais o princípio da recursão não pode ser justificado. Considere o "tipo indutivo" Dcom um construtor

• d : (D -> D) -> D

Aqui não há um princípio de recursão são aqui. e por boas razões! Se tivéssemos algum princípio de recursão, poderíamos usá-lo para codificar uma versão de auto-aplicação e, com isso, não-terminação. Isso significa Dque não pode ser chamado de "indutivo" porque tipos indutivos são construções finitas geradas a partir da aplicação repetida de construtores!

Para lidar com isso, restringimos como os tipos indutivos podem ser recursivos na teoria dos tipos. Especificamente, impedimos que eles apareçam em "lugares negativos". É sobre essa noção de polaridade que você estava falando. A polaridade de uma posição é determinada assim,

1. O argumento começa em uma posição positiva
2. Toda vez que vamos à esquerda uma flecha, a polaridade muda

Então, Xé positivo nos dois primeiros e negativo nos dois segundos

X
Int -> X
X -> Int
(Unit -> X) -> Int

Essa idéia é justificada com o recurso à teoria das categorias, em que um tipo indutivo cujas únicas recorrências são positivas dá origem a um functor covariante. Os detalhes de como isso funciona e por que é interessante um pouco longo.

O significado de Bob Harper

Em seu blog, Harper estava falando sobre um significado diferente de polaridade. Essa polaridade é referência a como vários conectivos na lógica recebem significado. Em particular, podemos classificar conectivos de duas maneiras

• Os conectivos positivos podem ser definidos definindo como apresentá-los (suas regras de introdução)
• Os conectivos negativos podem ser definidos definindo como usá-los (suas regras de eliminação)

Em termos de linguagem de programação, isso captura bem a distinção entre tipos preguiçoso e estrito. Um tipo estrito é definido por seus valores. Um preguiçoso é definido por como o padrão pode corresponder a eles. Para lidar com isso corretamente, definimos uma linguagem com duas construções principais, maneiras de criar tipos positivos e "espinhos" para decompor tipos negativos. Podemos usar isso para incorporar computação rigorosa e lenta em um idioma.

Para entender melhor isso, refiro-lhe ao capítulo 38 do livro de Bob Harper .