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

recursive-datastructures algebraic-data-types

Question

Manual de Agda sobre tipos de datos inductivos y estados de coincidencia de patrones :

Para garantizar la normalización, las incidencias inductivas deben aparecer en posiciones estrictamente positivas. Por ejemplo, el siguiente tipo de datos no está permitido:

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

ya que hay una ocurrencia negativa de Malo en el argumento al 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 cálculo lambda sin tipo .

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

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

Vamos a ver 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 de cálculo lambda no tipificados 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 tipificado favorito sin terminación para producir un término sin terminación de tipo Bad . Por ejemplo, podríamos traducir (/x. xx) (/x. xx) a la expresión sin terminación de tipo Bad continuación:

unbad (bad (/x -> unbad x x)) (bad (/x -> unbad x x))

Aunque el tipo resultó ser una forma particularmente conveniente para este argumento, puede generalizarse con un poco de trabajo para cualquier tipo de datos con ocurrencias negativas de recursión.

Answer 2

Un ejemplo de cómo un tipo de datos de este tipo nos permite habitar en cualquier tipo se encuentra en Turner, DA (2004-07-28), Total Functional Programming , secc. 3.1, página 758 en la Regla 2: La recursión de tipos 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 construya el combinador Y a partir de él sin ninguna otra forma de recursión. Esto significa que tener ese tipo de datos nos permite construir cualquier tipo de recursión, o habitar cualquier tipo por una recursión infinita.

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

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

La clave para ello es que aplicamos x a sí mismo en xx . En los idiomas escritos, esto no es directamente posible, ya que posiblemente no haya un tipo válido que pueda tener x . Pero nuestro tipo de datos Bad permite que este módulo agregue / elimine el constructor:

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

Tomando x :: Bad a , podemos desempaquetar su constructor y aplicar la función dentro de x sí. Una vez que sabemos cómo hacerlo, es fácil construir el combinador de 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 para sí misma. La recursión aparece solo en nuestro tipo de datos recursivos.

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

loop :: a
loop = yc id

o compute 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