Quelle est la base théorique des types existentiels ?

Question

El Haskell Wiki explique bien comment utiliser les types existentiels, mais je ne comprends pas bien la théorie qui les sous-tend.

Considérons cet exemple de type existentiel :

data S = forall a. Show a => S a      -- (1)

pour définir un emballage de type pour les choses que nous pouvons convertir en un String . Le wiki mentionne que ce que nous vraiment que vous voulez définir est un type comme

data S = S (exists a. Show a => a)    -- (2)

c'est-à-dire un véritable type "existentiel" - en gros, je pense que cela revient à dire "le constructeur de données S prend tout type pour lequel un Show instance existe et l'enveloppe". En fait, vous pourriez probablement écrire un GADT comme suit :

data S where                          -- (3)
    S :: Show a => a -> S

Je n'ai pas essayé de le compiler, mais il me semble qu'il devrait fonctionner. Pour moi, le GADT est évidemment équivalent au code (2) que nous aimerions écrire.

Cependant, il n'est absolument pas évident pour moi de comprendre pourquoi (1) est équivalent à (2). Pourquoi le fait de déplacer le constructeur de données à l'extérieur transforme-t-il l'élément forall dans un exists ?

Les choses les plus proches auxquelles je peux penser sont Les lois de Morgan en logique, où l'interversion de l'ordre d'une négation et d'un quantificateur transforme les quantificateurs existentiels en quantificateurs universels, et vice-versa :

¬(∀x. px) ⇔ ∃x. ¬(px)

mais les constructeurs de données semblent être une bête totalement différente de l'opérateur de négation.

Quelle est la théorie qui se cache derrière la capacité de définir des types existentiels en utilisant forall au lieu de l'inexistant exists ?

Answer 1

Tout d'abord, jetez un coup d'œil à la "correspondance de Curry Howard" qui stipule que les types d'un programme informatique correspondent aux formules de la logique intuitionniste. La logique intuitionniste est tout comme la logique "régulière" que vous avez apprise à l'école, mais sans la loi du milieu exclu ou la double élimination par négation :

• Ce n'est pas un axiome : P ⇔ ¬¬P (mais P ⇒ ¬¬P est bien)

• Ce n'est pas un axiome : P ∨ ¬P

Les lois de la logique

Vous êtes sur la bonne voie avec les lois de DeMorgan, mais nous allons d'abord les utiliser pour en dériver de nouvelles. La version pertinente des lois de DeMorgan est la suivante :

• ∀x. P(x) = ¬∃x. ¬P(x)
• ∃x. P(x) = ¬∀x. ¬P(x)

Nous pouvons dériver (∀x. P ⇒ Q(x)) = P ⇒ (∀x. Q(x)) :

1. (∀x. P ⇒ Q(x))
2. (∀x. ¬P ∨ Q(x))
3. ¬P ∨ (∀x. Q(x))
4. P ⇒ (∀x. Q)

Et (∀x. Q(x) ⇒ P) = (∃x. Q(x)) ⇒ P (celle-ci est utilisée ci-dessous) :

1. (∀x. Q(x) ⇒ P)
2. (∀x. ¬Q(x) ∨ P)
3. (¬¬∀x. ¬Q(x)) ∨ P
4. (¬∃x. Q(x)) ∨ P
5. (∃x. Q(x)) ⇒ P

Notez que ces lois sont également valables en logique intuitionniste. Les deux lois que nous avons dérivées sont citées dans l'article ci-dessous.

Types simples

Les types les plus simples sont faciles à utiliser. Par exemple :

data T = Con Int | Nil

Les constructeurs et les accesseurs ont les signatures de type suivantes :

Con :: Int -> T
Nil :: T

unCon :: T -> Int
unCon (Con x) = x

Constructeurs de type

Abordons maintenant les constructeurs de types. Prenons la définition de données suivante :

data T a = Con a | Nil

Cela crée deux constructeurs,

Con :: a -> T a
Nil :: T a

Bien sûr, en Haskell, les variables de type sont implicitement quantifiées de manière universelle, donc elles le sont vraiment :

Con :: ∀a. a -> T a
Nil :: ∀a. T a

Et l'accesseur est tout aussi simple :

unCon :: ∀a. T a -> a
unCon (Con x) = x

Types quantifiés

Ajoutons le quantificateur existentiel, ∃, à notre type original (le premier, sans le constructeur de type). Plutôt que de l'introduire dans la définition du type, qui ne ressemble pas à de la logique, introduisons-le dans les définitions du constructeur / accesseur, qui ressemblent à de la logique. Nous corrigerons la définition des données plus tard pour qu'elle corresponde.

Au lieu de Int nous allons maintenant utiliser ∃x. t . Ici, t est une sorte d'expression de type.

Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)

En se basant sur les règles de la logique (la deuxième règle ci-dessus), nous pouvons réécrire le type de Con à :

Con :: ∀x. t -> T

Lorsque nous avons déplacé le quantificateur existentiel vers l'extérieur (forme prenex), il s'est transformé en un quantificateur universel.

Les éléments suivants sont donc théoriquement équivalents :

data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil

Sauf qu'il n'y a pas de syntaxe pour exists en Haskell.

En logique non intuitionniste, il est permis de dériver ce qui suit à partir du type de unCon :

unCon :: ∃ T -> t -- invalid!

La raison pour laquelle cela n'est pas valable est qu'une telle transformation n'est pas autorisée en logique intuitionniste. Il est donc impossible d'écrire le type pour unCon sans un exists et il est impossible de mettre la signature de type sous forme de prenex. Il est difficile de faire un vérificateur de type dont la fin est garantie dans de telles conditions, c'est pourquoi Haskell ne supporte pas les quantificateurs existentiels arbitraires.

Sources

"First-class Polymorphism with Type Inference", Mark P. Jones, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages ( web )

Answer 2

Plotkin et Mitchell ont établi une sémantique pour les types existentiels, dans leur célèbre article, qui a fait le lien entre les types abstraits dans les langages de programmation et les types existentiels en logique,

Mitchell, John C. ; Plotkin, Gordon D. ; Les types abstraits ont un caractère existentiel Type ACM Transactions on Programming Languages and Systems, Vol. 10, n° 3, juillet 1988, pp. 470-502

À un niveau élevé,

Les déclarations de types de données abstraites apparaissent dans les langages de programmation typés comme Ada, Alphard, CLU et ML. Cette forme de déclaration de déclaration lie une liste d'identifiants à un type avec des opérations associées, une valeur" composite que nous appelons une algèbre de données. Nous utilisons un lambda calculus SOL du second ordre pour montrer comment on peut donner des types aux algèbres de données, passées comme paramètres, et retournées comme résultats d'appels de fonctions. Dans processus, nous discutons de la sémantique des déclarations de type de données déclarations de types de données abstraites et nous examinons un lien entre les langages de de programmation typés et la logique constructive.

Answer 3

C'est indiqué dans l'article du wiki haskell dont vous avez donné le lien. Je vais emprunter quelques lignes de code et commentaires de cet article et tenter de l'expliquer.

data T = forall a. MkT a

Ici, vous avez un type T avec un constructeur de type MkT :: forall a. a -> T n'est-ce pas ? MkT est (en gros) une fonction, donc pour chaque type possible a la fonction MkT avoir le type a -> T . Nous sommes donc d'accord pour dire qu'en utilisant ce constructeur, nous pouvons construire des valeurs telles que [MkT 1, MkT 'c', MkT "hello"] tous de type T .

foo (MkT x) = ... -- what is the type of x?

Mais que se passe-t-il lorsque vous essayez d'extraire (par exemple via un filtrage) la valeur contenue dans un fichier de type T ? Son annotation de type indique seulement T sans aucune référence au type de la valeur qu'il contient réellement. Nous pouvons seulement nous mettre d'accord sur le fait que, quelle que soit la valeur, elle aura un (et un seul) type ; comment pouvons-nous énoncer cela en Haskell ?

x :: exists a. a

Cela signifie simplement qu'il existe un type a à laquelle x appartient. A ce stade, il devrait être clair que, en supprimant le forall a de MkT et en spécifiant explicitement le type de la valeur enveloppée (à savoir exists a. a ), nous sommes en mesure d'obtenir le même résultat.

data T = MkT (exists a. a)

Le résultat est le même si vous ajoutez des conditions sur les classes de type implémentées comme dans vos exemples.