Sucesos negativos "guardados" en la definición de tipos inductivos, ¿siempre malos?

Sé cómo algunas ocurrencias negativas pueden ser definitivamente malas:

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

Sin embargo, no estoy seguro de si:

• todos los tipos inductivos con ocurrencias negativas pueden resultar incorrectos

• si es así, hay una forma mecánica conocida de hacerlo;

Por ejemplo, he estado luchando tratando de hacer que este tipo salga mal:

type Not a = a -> False

data Bad2 a = C2 (Bad2 (Not a) -> a)

Cualquier puntero a la literatura sobre este tema sería apreciado.

La razón de la prohibición de sucesos negativos se puede entender por analogía con el teorema de Knaster-Tarski. Este teorema dice que

si es una red completa yf : L → L es una función monótona en L , entonces el conjunto de puntos fijos de f también es una red completa. En particular, hay un punto mínimo fijo μ f y un mayor punto fijo ν f .$L$$f : L \to L$$L$$f$$\mu{f}$$\nu f$

$L$$p \leq q$$q$$p$

$\mathbb{C}$$e : P \to Q$$Q$$Q$

$\mathbb{N} = \mu \alpha.\;1 + \alpha$ $F : \mathbb{C} \to \mathbb{C}$$e : P \to Q$$F(e) : F(P) \to F(Q)$$F$$F(g \circ f) = F(g) \circ F(f)$

$\mu \alpha.\;F(\alpha)$$F$

En lenguajes de tipo dependiente, también tiene tipos indexados y parametrizados, por lo que su tarea real es más complicada. Bob Atkey (que ha blogueado sobre esto aquí y aquí ) me dice que un buen lugar para buscar la historia es:

• Inducción estructural y coinducción en un entorno fibracional , Claudio Hermida y Bart Jacobs 1997.
• Reglas de inducción fibracional para álgebras iniciales , Neil Ghani, Patricia Johann y Clement Fumex 2010.

Como Andrej señala, fundamentalmente si una ocurrencia negativa está bien o no depende de cuál sea su modelo de teoría de tipos. Básicamente, cuando tienes una definición recursiva, estás buscando un punto fijo, y hay muchos teoremas de punto fijo en matemáticas.

Uno de los cuales, personalmente, he utilizado mucho es el teorema del punto fijo de Banach, que dice que si tiene una función estrictamente contractiva en un espacio métrico, entonces tiene un punto fijo único. Esta idea fue introducida en la semántica por (IIRC) Maurice Nivat, y fue ampliamente estudiada por América y Rutten, y recientemente Birkedal y sus colaboradores la conectaron con una técnica operativa popular llamada "indexación por pasos".

• Resolviendo ecuaciones de dominio reflexivo en una categoría de espacios métricos completos , Pierre America y Jan JMM Rutten 1989.
• La solución teórica de categoría de las ecuaciones recursivas de espacio métrico , Lars Birkedal, Kristian Støvring y Jacob Thamsborg. 2010

Esto da lugar a teorías de tipos en las que se permiten ocurrencias negativas en tipos recursivos, pero solo cuando las ocurrencias negativas ocurren bajo un constructor de tipo especial de "protección". Esta idea fue presentada por Hiroshi Nakano, y la conexión con el teorema de Banach fue hecha tanto por mí como por Nick Benton, así como por Lars Birkedal y sus coautores.

• Una modalidad para la recursión , Hiroshi Nakano, 2000.
• Semántica ultramétrica de programas reactivos , Nick Benton y Neel Krishnaswami, 2011.
• Un modelo métrico de recursión protegida , Lars Birkedal, Jan Schwinghammer y Kristian Støvring, 2010.

A veces puedes resolver ecuaciones recursivas "por suerte".

$$A \cong (A \to \emptyset) \to A.$$

1. $A$$A \to \emptyset \cong \emptyset$

   $$A \cong \emptyset \to A \cong 1.$$ $1$

2. $A$$\emptyset \cong (\emptyset \to \emptyset) \to \emptyset \cong 1 \to \emptyset \cong \emptyset$

Conclusión: hay dos soluciones, el tipo vacío (que llamó False) y el tipo de unidad ().

$$A \cong (A \to 2) \to 2,$$

data Cow a = Moo ((a -> Bool) -> Bool)

$A \cong 2^{2^A}$$A$$2^{2^A}$

$$\mathbb{N} \cong 2^{2^\mathbb{N}}.$$ $2^\mathbb{N}$$2^{2^\mathbb{N}}$Integer(Integer -> Bool) -> Bool

Es difícil agregar algo a las explicaciones de Andrej o Neel, pero lo intentaré. Voy a tratar de abordar el punto de vista sintáctico, en lugar de tratar de descubrir la semántica subyacente, porque la explicación es más elemental y puedo dar una respuesta más directa a su pregunta.

$\lambda$

La referencia crucial es la siguiente:

Mendler, N. (1991). Tipos inductivos y restricciones de tipo en el cálculo lambda de segundo orden. No he encontrado una referencia en línea, me temo. Sin embargo, las declaraciones y pruebas se pueden encontrar en la tesis doctoral de Nax (¡una lectura muy recomendable!).

$\mathrm{Bad}$

$$\mathrm{Bad} = \mathrm{Bad}\rightarrow A$$

$A$

$$\lambda x:\mathrm{Bad}.x\ x: \mathrm{Bad}\rightarrow A$$

y entonces

$$(\lambda x:\mathrm{Bad}.x\ x)\ (\lambda x:\mathrm{Bad}.x\ x): A$$

$$\mathrm{Bad} = F(\mathrm{Bad})$$ $F(X)$$X$$F(X)$

Por supuesto, no está trabajando con tipos definidos equitativamente sino con constructores , es decir, tiene

data Bad = Pack (Bad -> A)

en lugar de estricta igualdad. Sin embargo, puedes definir

unpack :: Bad -> (Bad -> A)
unpack (Pack f) = f

lo cual es suficiente para que este resultado continúe siendo válido:

 (\x:Bad -> unpack x x) (Pack (\x:Bad -> unpack x x))

$A$

---

En su segundo ejemplo, las cosas son un poco más complicadas, ya que tiene algo en la línea de

$$\mathrm{Bad} = \mathrm{Bad}' \rightarrow A$$

$\mathrm{Bad}'$$\mathrm{Bad}$$\mathrm{Bad}\ a$$\mathrm{Bad}\ (\mathrm{Not}\ a)$

type Not a = a -> False

con

data Not a = Not a

Se resolvería fácilmente si Haskell permitiera tales definiciones de tipo:

type Acc = Not Acc

En este caso, podría construir un combinador de bucles exactamente de la misma manera que antes. Sospecho que puedes llevar una construcción similar (pero más compleja) usando

data Acc = D (Not Acc)

El problema aquí es que para construir un isomorfismo

Bad Acc <-> Bad (Not Acc)

tienes que lidiar con la varianza mixta.