Pourquoi les types de données inductifs interdire des types comme données d'un Mauvais = C (Bad a -> a)` où le type se produit devant ->?

Question

Agda manuel sur Inductive Types de Données et le filtrage membres:

Pour assurer la normalisation, de l'inductif occurrences doivent apparaître dans strictement positive positions.Par exemple, suivant le type de données n'est pas autorisé:

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

car il y a un négatif apparition de Mauvaises dans l'argument du constructeur.

Pourquoi est-ce une condition nécessaire pour inductive types de données?

Answer 1

Le type de données que vous avez donné est particulier en ce qu'il est une incorporation de l' non typé lambda calcul.

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

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

Nous allons voir comment.Rappel, le type lambda calcul a ces termes:

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

On peut définir une traduction [[e]] de type lambda calcul des termes d'Agda termes de type de Bad (mais pas dans Agda):

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

Vous pouvez maintenant utiliser votre favori de la non-terminaison de type lambda terme pour produire un non-terminaison terme de type Bad.Par exemple, nous pourrions traduire (\x. x x) (\x. x x) à la non-terminaison expression de type Bad ci-dessous:

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

Bien que le type qui est arrivé à être particulièrement pratique pour cet argument, il peut être généralisée avec un peu de travail pour tout type de données négatives sur les occurrences de la récursivité.

Answer 2

Un exemple de comment un tel type de données nous permet d'habiter dans n'importe quel type est donné dans Turner, D. A.(2004-07-28), Total De La Programmation Fonctionnelle, sect.3.1, page 758 en Règle 2:Type de récursivité doit être covariantes."

---

Nous allons prendre un exemple plus élaboré à l'aide de Haskell.Nous allons commencer avec un "mauvais" type de données récursive

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

et la construction de la Y combinator de il sans autre forme de récursivité.Cela signifie que le fait d'avoir un type de données nous permet de construire tout type de récursivité, ou occupent tout type par une récursion infinie.

Le Y combinator dans le type lambda calcul est défini comme

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

La clé, c'est que nous appliquons x à lui-même dans x x.Dans les langages à typage ce n'est pas possible directement, car il n'y a pas de type valide x pourrait éventuellement avoir.Mais notre Bad type de données permet cette modulo ajout/retrait du constructeur:

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

La prise de x :: Bad a, nous pouvons déballer son constructeur et d'appliquer la fonction à l'intérieur de x lui-même.Une fois que nous savons comment le faire, il est facile de construire le Y combinator:

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

Notez que ni selfApp ni yc sont récursives, il n'y a pas d'appel récursif de la fonction elle-même. La récursivité n'apparaît que dans notre récursive du type de données.

Nous pouvons vérifier que le construit combinator, en effet, que ce qu'il devrait.Nous pouvons faire une boucle infinie:

loop :: a
loop = yc id

ou calculer disons PGCD:

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