¿Por qué los tipos de datos inductivos prohíben tipos como `datos Malo a = C (Malo a -> a)` donde el tipo de recursión ocurre frente a ->?

Question

manual de Agda en Inductive Data Types and Pattern Matching estados:

Para garantizar la normalización, las ocurrencias inductivos debe aparecer en posiciones estrictamente positivos. Por ejemplo, no se permite el siguiente tipo de datos:

data Bad : Set where 
    bad : (Bad → Bad) → Bad 

ya que hay una incidencia negativa de Bad en el argumento del constructor.

¿Por qué es necesario este requisito para los tipos de datos inductivos?

Answer 1

El tipo de datos que diste es especial, ya que es una incrustación del cálculo lambda sin tipo.

data Bad : Set where 
    bad : (Bad → Bad) → Bad 

unbad : Bad → (Bad → Bad) 
unbad (bad f) = f 

Veamos cómo. Recordemos, el cálculo lambda sin tipo tiene estos términos:

e := x | \x. e | e e' 

Podemos definir una traducción [[e]] de términos cálculo lambda sin tipo a términos agda de tipo Bad (aunque no en Agda):

[[x]]  = x 
[[\x. e]] = bad (\x -> [[e]]) 
[[e e']] = unbad [[e]] [[e']] 

Ahora puede usar su término lambda no-terminado preferido para producir un término no-terminante del tipo Bad. Por ejemplo, podríamos traducir (\x. x x) (\x. x x) a la expresión no terminar de tipo Bad a continuación:

unbad (bad (\x -> unbad x x)) (bad (\x -> unbad x x)) 

Aunque el tipo pasó a ser una forma particularmente conveniente para este argumento, se puede generalizar con un poco de trabajo a cualquier tipo de datos con ocurrencias negativas de recursividad.

Answer 2

Un ejemplo de cómo este tipo de datos nos permite habitar en cualquier tipo se da en Turner, D.A. (2004-07-28), Total Functional Programming, secc. 3.1, página 758 en Regla 2: Tipo de recursión debe ser covariante "

---

Hagamos un ejemplo más elaborado usando Haskell Vamos a empezar con una. "Malo" tipo de datos recursiva

data Bad a = C (Bad a -> a) 

.

y construir el Y combinator de ella sin cualquier otra forma de recursión. Esto significa que tiene un tipo de tales datos nos permite construir cualquier tipo de recursión, o habitar cualquier tipo por una recursión infinita.

El combinador Y en el cálculo lambda sin tipo se define como

Y = λf.(λx.f (x x)) (λx.f (x x)) 

La clave para esto es que aplicamos x a sí mismo en x x. En los idiomas tipados, esto no es directamente posible, porque no existe un tipo válido x que pueda tener. Pero nuestra Bad tipo de datos permite que este módulo añadir/eliminar el constructor:

selfApp :: Bad a -> a 
selfApp (x@(C x')) = x' x 

Tomando x :: Bad a, podemos desenvolver su constructor y aplicar la función dentro de x sí. Una vez que sabemos cómo hacer esto, es fácil de construir el combinador Y:

yc :: (a -> a) -> a 
yc f = let fxx = C (\x -> f (selfApp x)) -- this is the λx.f (x x) part of Y 
     in selfApp fxx 

Tenga en cuenta que ni selfApp ni yc son recursivos, no hay una llamada recursiva de una función a sí mismo. La recursividad aparece solo en nuestro tipo de datos recursivos.

Podemos comprobar que el combinador fabricado realmente hace lo que debería. Podemos hacer un bucle infinito:

loop :: a 
loop = yc id 

o calcular digamos GCD:

gcd' :: Int -> Int -> Int 
gcd' = yc gcd0 
    where 
    gcd0 :: (Int -> Int -> Int) -> (Int -> Int -> Int) 
    gcd0 rec a b | c == 0  = b 
        | otherwise = rec b c 
     where c = a `mod` b