Estricta positividad

De esta referencia: positividad estricta

La condición de positividad estricta descarta declaraciones como

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

¿Por qué A es negativo? ¿También por qué B está permitido? Entiendo por qué C está permitido.

Primero una explicación terminológica: las posiciones negativas y positivas provienen de la lógica. Son alrededor de una asimetría en conectores lógicos: en al A se comporta de manera diferente de B . Algo similar sucede en la teoría de categorías, donde decimos contravariante y covariante en lugar de negativo y positivo, respectivamente. En física, hablan de cantidades que se comportan "covariablemente" y "contrariamente, también. Así que este es un fenómeno muy general. Un programador podría pensar en ellas como" entrada "y" salida ".$A \Rightarrow B$$A$$B$

Ahora en tipos de datos inductivos.

Piensa en un tipo de datos inductiva como una especie de estructura algebraica: constructores son las operaciones que tienen elementos de T como argumentos y producen nuevos elementos de T . Esto es muy similar al álgebra ordinaria: la suma toma dos números y produce un número.$T$$T$$T$

En álgebra, es costumbre que una operación tome un número finito de argumentos, y en la mayoría de los casos toma cero (constante), uno (unario) o dos (binarios) argumentos. Es conveniente generalizar esto para constructores de tipos de datos. Supongamos que ces un constructor para un tipo de datos T:

• si ces una constante, podemos pensar en ella como una función unit -> T, o de manera equivalente (empty -> T) -> T,
• si ces unario, podemos considerarlo como una función T -> T, o de manera equivalente (unit -> T) -> T,
• si ces binario, podemos considerarlo como una función T -> T -> T, o de manera equivalente T * T -> To equivalente (bool -> T) -> T,
• Si quisiéramos un constructor cque tomara siete argumentos, podríamos verlo como una función (seven -> T) -> Tdonde sevenhay algún tipo previamente definido con siete elementos.
• También podemos tener un constructor cque tome innumerables argumentos, que sería una función (nat -> T) -> T.

Estos ejemplos muestran que la forma general de un constructor debe ser

c : (A -> T) -> T

donde llamamos a Ala aridad de cy pensamos que ces un constructor que toma A-muchos argumentos de tipo Tpara producir un elemento de T.

Aquí hay algo muy importante: las aridades deben definirse antes de que las definamos T, o de lo contrario no podemos saber qué deben hacer los constructores. Si alguien intenta tener un constructor

broken: (T -> T) -> T

entonces la pregunta "¿cuántos argumentos brokenlleva?" No tiene una buena respuesta. Puede intentar responderlo con "se necesitan Tmuchos argumentos", pero eso no servirá, porque Taún no está definido. Podríamos tratar de salir del cunundrum usando una teoría elegante de punto fijo para encontrar un tipo Ty una función inyectiva (T -> T) -> T, y tendríamos éxito, pero también romperíamos el principio de inducción en Tel camino. Entonces, es una mala idea intentar tal cosa.

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

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

De hecho, muchos constructores se pueden reescribir de esta forma, pero no todos, necesitamos un paso más, es decir, debemos permitir Aque dependerá de B:

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

Esta es la forma final de un constructor para un tipo inductivo. También es precisamente lo que son los tipos W. ¡La forma es tan general que solo necesitamos un solo constructor c! De hecho, si tenemos dos de ellos

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

entonces podemos combinarlos en uno

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

dónde

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

Por cierto, si cambiamos la forma general, vemos que es equivalente a

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

que está más cerca de lo que la gente realmente escribe en asistentes de prueba. Los asistentes de prueba nos permiten escribir los constructores de manera conveniente, pero son equivalentes a la forma general anterior (¡ejercicio!).

La primera aparición de Badse llama 'negativa' porque representa un argumento de función, es decir, se encuentra a la izquierda de la flecha de función (vea Philip Wadler los tipos recursivos de forma gratuita ). Supongo que el origen del término 'posición negativa' proviene de la noción de contravarianza ('contra' significa opuesto).

No se permite que el tipo se defina en posición negativa porque uno puede escribir programas sin terminación usándolo, es decir, una fuerte normalización falla en su presencia (más sobre esto a continuación). Por cierto, esta es la razón del nombre de la regla 'positividad estricta': no ​​permitimos posiciones negativas.

Permitimos la segunda aparición de, Badya que no causa la no terminación y queremos usar el tipo que se define ( Bad) en algún momento en un tipo de datos recursivo ( antes de la última flecha de su constructor).

Es importante comprender que la siguiente definición no viola la estricta regla de positividad.

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

La regla se aplica solo a los argumentos del constructor (que son ambos Gooden este caso) y no a un constructor en sí mismo (véase también " Programación certificada con tipos dependientes " de Adam Chlipala ).

Otro ejemplo que viola la positividad estricta:

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

También es posible que desee verificar esta respuesta sobre las posiciones negativas.

Las declaraciones no estrictamente positivas se rechazan porque uno puede escribir una función sin terminación usándolas. Para ver cómo se puede escribir una definición de bucle usando el tipo de datos Bad desde arriba, vea BadInHaskell .

Aquí hay un ejemplo análogo en Ocaml, que muestra cómo implementar un comportamiento recursivo sin (!) Usando la recursión directamente:

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)

La nonTerminatingfunción "desempaqueta" una función de su argumento y la transfiere al argumento original. Lo importante aquí es que la mayoría de los sistemas de tipos no permiten pasar funciones a sí mismos, por lo que un término como f fno mecanografiará, ya que no hay ningún tipo para fsatisfacer el mecanografiado. Una de las razones por las que se introdujeron los sistemas de tipos es para deshabilitar la auto aplicación (ver aquí ).

Los tipos de datos de envoltura como el que presentamos anteriormente se pueden usar para sortear este obstáculo en el camino hacia la inconsistencia.

Quiero agregar que los cálculos sin terminación introducen inconsistencias en los sistemas lógicos. En el caso de Agda y Coq, el Falsetipo de datos inductivo no tiene ningún constructor, por lo que nunca se puede construir un término de prueba de tipo False. Pero si se permitieran los cálculos sin terminación, uno podría hacerlo, por ejemplo, de esta manera (en Coq):

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

Luego loop 0escribiría cheques loop 0 : False, por lo que, según la correspondencia de Curry-Howard, significaría que probamos una proposición falsa.

Resultado : la estricta regla de positividad para las definiciones inductivas evita los cálculos sin terminación que son desastrosos para la lógica.