¿Por qué los tipos de datos inductivos prohíben tipos como `datos Bad a = C (Bad a -> a)` donde la recursividad del tipo ocurre delante de ->?

Question

manual agda en Tipos de datos inductivos y coincidencia de patrones estados:

Para garantizar la normalización, los sucesos inductivos deben aparecer en posiciones estrictamente positivas.Por ejemplo, no se permite el siguiente tipo de datos:

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

ya que hay una aparición 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 proporcionó es especial porque es una incrustación del sin escribir cálculo lambda.

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

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

Veamos cómo.Recuerde, 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 de cálculo lambda sin tipo a términos de tipo Agda Bad (aunque no en Agda):

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

Ahora puede utilizar su término lambda sin tipo y sin terminación favorito para producir un término de tipo sin terminación Bad.Por ejemplo, podríamos traducir (\x. x x) (\x. x x) a la expresión no terminante de tipo Bad abajo:

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

Aunque el tipo resultó 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 dicho tipo de datos nos permite habitar cualquier tipo se da en Turner, D.A.(28 de julio de 2004), Programación funcional total, secta.3.1, página 758 en Regla 2:El tipo de recursividad debe ser covariante."

---

Hagamos un ejemplo más elaborado usando Haskell.Comenzaremos con un tipo de datos recursivo "malo"

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

y construir el combinador Y de él sin ninguna otra forma de recursividad.Esto significa que tener dicho tipo de datos nos permite construir cualquier tipo de recursividad o habitar cualquier tipo mediante una recursividad 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 es que aplicamos x a sí mismo en x x.En lenguajes mecanografiados esto no es directamente posible, porque no existe ningún tipo válido. x posiblemente podría tener.Pero nuestra Bad El tipo de datos permite que este módulo agregue/elimine 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 interna a x sí mismo.Una vez que sabemos cómo hacer esto, es fácil 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í misma. La recursividad aparece solo en nuestro tipo de datos recursivos.

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

loop :: a
loop = yc id

o calcular digamos MCD:

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