Por que os tipos de dados indutivos proíbem tipos como `data Bad a = C (Bad a -> a)` onde a recursão de tipo ocorre na frente de ->?

Question

Manual Agda em Tipos de dados indutivos e correspondência de padrões afirma:

Para garantir a normalização, as ocorrências indutivas devem aparecer em posições estritamente positivas.Por exemplo, o seguinte tipo de dados não é permitido:

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

já que há uma ocorrência negativa de Bad no argumento do construtor.

Por que este requisito é necessário para tipos de dados indutivos?

Answer 1

O tipo de dados que você forneceu é especial porque é uma incorporação do não digitado cálculo lambda.

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

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

Vamos ver como.Lembre-se, o cálculo lambda não digitado tem estes termos:

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

Podemos definir uma tradução [[e]] de termos de cálculo lambda não digitados para termos de tipo Agda Bad (embora não em Agda):

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

Agora você pode usar seu termo lambda sem terminação favorito para produzir um termo sem terminação do tipo Bad.Por exemplo, poderíamos traduzir (\x. x x) (\x. x x) para a expressão não terminada do tipo Bad abaixo:

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

Embora o tipo seja uma forma particularmente conveniente para esse argumento, ele pode ser generalizado com um pouco de trabalho para qualquer tipo de dados com ocorrências negativas de recursão.

Answer 2

Um exemplo de como tal tipo de dados nos permite habitar qualquer tipo é dado em Turner, D.A.(28/07/2004), Programação Funcional Total, seita.3.1, página 758 em Regra 2:A recursão de tipo deve ser covariante."

---

Vamos fazer um exemplo mais elaborado usando Haskell.Começaremos com um tipo de dados recursivo “ruim”

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

e construir o Combinador Y dele sem qualquer outra forma de recursão.Isto significa que ter tal tipo de dados nos permite construir qualquer tipo de recursão, ou habitar qualquer tipo por uma recursão infinita.

O combinador Y no cálculo lambda não tipado é definido como

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

A chave para isso é que aplicamos x para si mesmo em x x.Em linguagens digitadas isso não é diretamente possível, porque não existe um tipo válido x poderia ter.Mas o nosso Bad tipo de dados permite este módulo adicionar/remover o construtor:

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

Tirando x :: Bad a, podemos desembrulhar seu construtor e aplicar a função interna a x em si.Depois de sabermos como fazer isso, é fácil construir o 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

Observe que nenhum selfApp nem yc são recursivos, não há chamada recursiva de uma função para si mesma. A recursão aparece apenas em nosso tipo de dados recursivo.

Podemos verificar se o combinador construído realmente faz o que deveria.Podemos fazer um loop infinito:

loop :: a
loop = yc id

ou 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