Lamentablemente, la "polaridad" es un concepto algo sobrecargado en la teoría de tipos. "Posición positiva" y "posición negativa" se refieren a una noción de polaridad diferente de lo que Bob está hablando con enfoque / polarización.
Lo que significa para tí
Cuando define un tipo inductivo, proporciona una serie de reglas que corresponden a operaciones para el tipo que está definiendo. Por ejemplo, podría decir que a Nates algo con
- un valor
zero : Nat
- Una función
suc : Nat -> Nat
Y luego espere que Natcontenga todos los valores que se pueden generar aplicando repetidamente suca otros Nate incluye zero. En línea con esta construcción inductiva, obtenemos un principio de recursividad a través de Nats que funciona en base al hecho de que cualquiera Nates generado por esos constructores.
rec : A -> (A -> A) -> Nat -> A
así que eso
rec Z S zero = zero
rec Z S (suc n) = S (rec Z S n)
Sin embargo, hay algunas restricciones sobre lo que podemos escribir como reglas. De lo contrario, podemos escribir una serie de reglas para las cuales el principio de recursión no puede justificarse. Considere el "tipo inductivo" Dcon un constructor
Aquí no hay un principio de recursión sano aquí. y por buenas razones! Si tuviéramos algún principio de recursividad, podríamos usarlo para codificar una versión de auto aplicación y, con ello, la no terminación. ¡Esto significa Dque no se puede llamar "inductivo" porque los tipos inductivos son construcciones finitas generadas a partir de la aplicación repetida de constructores!
Para tratar esto, restringimos cómo los tipos inductivos pueden ser recursivos en la teoría de tipos. Específicamente, evitamos que aparezcan en "lugares negativos". Esta es la noción de polaridad de la que estabas hablando. La polaridad de una posición se determina así,
- El argumento comienza en una posición positiva.
- Cada vez que vamos a la izquierda una flecha, la polaridad cambia
Entonces Xes positivo en los primeros dos y negativo en los segundos dos
X
Int -> X
X -> Int
(Unit -> X) -> Int
Esta idea se justifica con un recurso a la teoría de categorías donde un tipo inductivo con cuyas únicas recurrencias son positivas da lugar a un functor covariante. Los detalles de cómo funciona esto y por qué es interesante son un poco largos.
Significado de Bob Harper
En su blog, Harper hablaba de un significado diferente de polaridad. Esta polaridad es una referencia a cómo se les da significado a varias conectivas en lógica. En particular, podemos clasificar las conectivas de dos maneras
- Los conectivos positivos se pueden definir definiendo cómo presentarlos (sus reglas de introducción)
- Los conectivos negativos se pueden definir definiendo cómo usarlos (sus reglas de eliminación)
En términos de lenguaje de programación, esto captura muy bien la distinción entre tipos perezosos y estrictos. Un tipo estricto se define por sus valores. Una perezosa se define por cómo el patrón puede coincidir con ellas. Para manejar esto adecuadamente, definimos un lenguaje con 2 construcciones principales, formas de construir tipos positivos y "espinas" para descomponer los tipos negativos. Podemos usar esto para incorporar computación estricta y perezosa en un idioma.
Para entender esto mejor, lo remito al capítulo 38 del libro de Bob Harper .
