Occurrences négatives «gardées» dans la définition des types inductifs, toujours mauvaises?

Je sais comment certaines occurrences négatives peuvent définitivement être mauvaises:

data False

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

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

yc :: (a -> a) -> a
yc f = selfApp $ C (\x -> f (selfApp x))

false :: False
false = yc id

Cependant, je ne sais pas si:

• tous les types inductifs avec des événements négatifs peuvent tourner mal;

• dans l'affirmative, il existe un moyen mécanique connu de le faire;

Par exemple, je me suis battu en essayant de faire mal ce type:

type Not a = a -> False

data Bad2 a = C2 (Bad2 (Not a) -> a)

Tout pointeur vers la littérature sur ce sujet serait apprécié.

La raison de l'interdiction des occurrences négatives peut être comprise par analogie avec le théorème de Knaster-Tarski. Ce théorème dit que

si est un réseau complet et f : L → L est une fonction monotone sur L , alors l'ensemble des points fixes de f est également un réseau complet. En particulier, il existe un point fixe le plus petit μ f et un point fixe le plus grand ν f .$L$$f : L \to L$$L$$f$$\mu{f}$$\nu f$

Dans la théorie des modèles traditionnels, les réseaux peuvent être considérés comme des propositions, et la relation d'ordre p ≤ q peut être comprise comme une implication (c'est-à-dire que la vérité de q est impliquée par la vérité de p ).$L$$p \leq q$$q$$p$

Lorsque nous passons de la théorie des modèles à la théorie des preuves, les réseaux se généralisent en catégories. Les types peuvent être considérés comme les objets d'une catégorie , et une carte e : P → Q représente une preuve que Q peut être dérivée de Q .$\mathbb{C}$$e : P \to Q$$Q$$Q$

Lorsque nous essayons d'interpréter des types définis par des équations récursives, ee, , la chose évidente à faire est de chercher une généralisation du théorème de Knaster-Tarski. Ainsi, au lieu d'une fonction monotone sur un réseau, nous savons que nous voulons unfoncteur F : C → C , qui envoie des objets aux objets, mais généralise la condition de monotonie afin que chaque carte e : P → Q obtienne une carte F ( e ) : F ( P ) → F ( Q ) (avec les conditions de cohérence que F envoie des identités aux identités et préserve les compositions pour que$\mathbb{N} = \mu \alpha.\;1 + \alpha$ $F : \mathbb{C} \to \mathbb{C}$$e : P \to Q$$F(e) : F(P) \to F(Q)$$F$ ).$F(g \circ f) = F(g) \circ F(f)$

Donc, si vous voulez un type de données inductif , vous devez également fournir une action fonctorielle aux termes de l'opérateur de type F afin de vous assurer que le point fixe souhaité existe. La condition de positivité stricte dans Agda et Coq est uneconditionsyntaxiquequi implique cettecontraintesémantique. En gros, il dit que si vous construisez un opérateur de type à partir de sommes et de produits, vous pouvez toujours faire cuire l'action fonctorielle, et donc tout type formé de cette manière devrait avoir un point fixe.$\mu \alpha.\;F(\alpha)$$F$

Dans les langages de type dépendant, vous avez également des types indexés et paramétrés, donc votre tâche réelle est plus compliquée. Bob Atkey (qui a blogué à ce sujet ici et ici ) me dit qu'un bon endroit pour chercher l'histoire est:

• Induction structurelle et coinduction dans un contexte de fibrillation , Claudio Hermida et Bart Jacobs 1997.
• Règles d'induction fibreuse pour les algèbres initiales , Neil Ghani, Patricia Johann et Clement Fumex 2010.

Comme le note Andrej, fondamentalement, si une occurrence négative est correcte ou non, cela dépend de votre modèle de théorie des types. Fondamentalement, lorsque vous avez une définition récursive, vous recherchez un point fixe, et il y a beaucoup de théorèmes à point fixe en mathématiques.

Personnellement, j'ai beaucoup utilisé le théorème du point fixe de Banach, qui dit que si vous avez une fonction strictement contractuelle sur un espace métrique, alors il a un point fixe unique. Cette idée a été introduite dans la sémantique par (IIRC) Maurice Nivat, et a été largement étudiée par America et Rutten, et a été récemment reliée par Birkedal et ses collaborateurs à une technique opérationnelle populaire appelée "indexation par étapes".

• Résolution des équations de domaine réflexives dans une catégorie d'espaces métriques complets , Pierre America et Jan JMM Rutten 1989.
• La solution de catégorie théorique des équations récursives de l'espace métrique , Lars Birkedal, Kristian Støvring et Jacob Thamsborg. 2010.

Cela donne lieu à des théories de types où les occurrences négatives dans les types récursifs sont autorisées, mais uniquement lorsque les occurrences négatives se produisent sous un constructeur de type "garde" spécial. Cette idée a été introduite par Hiroshi Nakano, et le lien avec le théorème de Banach a été établi à la fois par moi-même et Nick Benton, ainsi que Lars Birkedal et ses coauteurs.

• A Modality for Recursion , Hiroshi Nakano, 2000.
• Sémantique ultramétrique des programmes réactifs , Nick Benton et Neel Krishnaswami, 2011.
• Un modèle métrique de récursivité surveillée , Lars Birkedal, Jan Schwinghammer et Kristian Støvring, 2010.

Parfois, vous pouvez résoudre des équations récursives "par chance".

$$A \cong (A \to \emptyset) \to A.$$

1. $A$$A \to \emptyset \cong \emptyset$

   $$A \cong \emptyset \to A \cong 1.$$ $1$

2. $A$$\emptyset \cong (\emptyset \to \emptyset) \to \emptyset \cong 1 \to \emptyset \cong \emptyset$

Conclusion: il existe deux solutions, le type vide (que vous avez appelé False) et le type d'unité ().

$$A \cong (A \to 2) \to 2,$$

data Cow a = Moo ((a -> Bool) -> Bool)

$A \cong 2^{2^A}$$A$$2^{2^A}$

$$\mathbb{N} \cong 2^{2^\mathbb{N}}.$$ $2^\mathbb{N}$$2^{2^\mathbb{N}}$Integer(Integer -> Bool) -> Bool

Il est difficile d'ajouter quoi que ce soit aux explications d'Andrej ou de Neel, mais je vais essayer. Je vais essayer d'aborder le point de vue syntaxique, plutôt que de découvrir la sémantique sous-jacente, parce que l'explication est plus élémentaire et que je donnerai une réponse plus simple à votre question.

$\lambda$

La référence cruciale est la suivante:

Mendler, N. (1991). Types inductifs et contraintes de type dans le calcul lambda du second ordre. Je n'ai pas trouvé de référence en ligne, je le crains. Les déclarations et les preuves peuvent cependant être trouvées dans la thèse de doctorat de Nax (une lecture fortement recommandée!).

$\mathrm{Bad}$

$$\mathrm{Bad} = \mathrm{Bad}\rightarrow A$$

$A$

$$\lambda x:\mathrm{Bad}.x\ x: \mathrm{Bad}\rightarrow A$$

et donc

$$(\lambda x:\mathrm{Bad}.x\ x)\ (\lambda x:\mathrm{Bad}.x\ x): A$$

$$\mathrm{Bad} = F(\mathrm{Bad})$$ $F(X)$$X$$F(X)$

Bien sûr, vous ne travaillez pas avec des types définis équativement mais avec des constructeurs , c'est-à-dire que vous avez

data Bad = Pack (Bad -> A)

plutôt qu'une stricte égalité. Cependant, vous pouvez définir

unpack :: Bad -> (Bad -> A)
unpack (Pack f) = f

ce qui est suffisant pour que ce résultat continue de tenir:

 (\x:Bad -> unpack x x) (Pack (\x:Bad -> unpack x x))

$A$

---

Dans votre deuxième exemple, les choses sont un peu plus délicates, car vous avez quelque chose comme

$$\mathrm{Bad} = \mathrm{Bad}' \rightarrow A$$

$\mathrm{Bad}'$$\mathrm{Bad}$$\mathrm{Bad}\ a$$\mathrm{Bad}\ (\mathrm{Not}\ a)$

type Not a = a -> False

avec

data Not a = Not a

Il serait facilement résolu si Haskell permettait de telles définitions de type:

type Acc = Not Acc

Dans ce cas, vous pouvez créer un combinateur en boucle exactement de la même manière qu'auparavant. Je suppose que vous pouvez réaliser une construction similaire (mais plus complexe) en utilisant

data Acc = D (Not Acc)

Le problème ici est que pour construire un isomorphisme

Bad Acc <-> Bad (Not Acc)

vous devez faire face à une variance mixte.