Une description mathématique (catégorique) des classes de type

14

Un langage fonctionnel peut être considéré comme une catégorie où ses objets sont des types et des fonctions de morphismes entre eux.

Comment les classes de types s'intègrent-elles dans ce modèle?

Je suppose que nous ne devons considérer que les implémentations qui satisfont à la contrainte de la plupart des classes de types, mais qui ne sont pas exprimées dans Haskell. Par exemple, nous ne devons considérer que les implémentations Functorpour lesquelles fmap id ≡ idet fmap f . fmap g ≡ fmap (f . g).

Ou existe-t-il d'autres fondements théoriques pour les classes de types (par exemple basés sur des calculs lambda typés)?

Petr Pudlák
la source
1
Vous voudrez peut-être être plus explicite sur ce que vous voulez pour un modèle. Si vous voulez quelque chose qui puisse décrire rigoureusement l'hypothèse du monde ouvert, le comportement de la résolution d'instance, l'interaction de diverses extensions GHC, etc., c'est plutôt plus compliqué qu'une version idéalisée. De même, notez que les fonds sont souvent ignorés lorsque vous discutez de Hask.
CA McCann
4
Les classes de types peuvent être considérées comme des signatures (au sens de l'algèbre universelle). La collection de toutes les entités partageant la même signature (éléments de la même classe de type) est une variété .
Dave Clarke
1
@DaveClarke: Il n'est pas immédiatement évident pour moi de décrire les classes de types sur les types supérieurs de cette façon, mais je ne connais pas très bien l'algèbre universelle et je peux mal comprendre la correspondance que vous avez en tête ...
CA McCann
1
@camccann: Je ne sais pas jusqu'où va la correspondance. Cela semblait certainement un bon point de départ.
Dave Clarke
2
@camccann: Modifiez simplement la catégorie de base sur laquelle vous définissez votre algèbre: les classes de type de base comme num sont des signatures sur la catégorie des types haskell (ou des objets de la catégorie Hsk), les classes de type sur les constructeurs de type sont des algèbres sur la catégorie des foncteurs de Hask à Hask. Notez que l'algèbre universelle est complètement subsumée par la notion d'algèbre dans la théorie des catégories. Aussi: Dave: vous devriez transformer votre commentaire en réponse.
cody

Réponses:

18

Comment les classes de types s'intègrent-elles dans ce modèle?

La réponse courte est: ils ne le font pas.

Chaque fois que vous introduisez des contraintes, des classes de types ou d'autres mécanismes de polymorphisme ad hoc dans un langage, le principal problème de conception auquel vous êtes confronté est cohérence .

Fondamentalement, vous devez vous assurer que la résolution de la classe de types est déterministe, afin qu'un programme bien typé ait une seule interprétation. Par exemple, si vous pouviez donner plusieurs instances pour le même type dans la même étendue, vous pourriez potentiellement écrire des programmes ambigus comme ceci:

class Blah a where
   blah : a -> String 

instance Blah T where
   blah _ = "Hello"

instance Blah T where
   blah _ = "Goodbye"

v :: T = ...

main :: IO ()
main = print (blah v)  -- does this print "Hello" or "Goodbye"?

Selon le choix de l'instance effectuée par le compilateur, blah vpeut être égal à"Hello" ou "Goodbye". Par conséquent, la signification d'un programme ne serait pas complètement déterminée par la syntaxe du programme, mais pourrait plutôt être influencée par des choix arbitraires faits par le compilateur.

La solution de Haskell à ce problème consiste à exiger que chaque type ait au plus une instance pour chaque classe de types. Pour ce faire, il autorise les déclarations d'instance uniquement au niveau supérieur et rend en outre toutes les déclarations visibles globalement. De cette façon, le compilateur peut toujours signaler une erreur si une déclaration d'instance ambiguë est faite.

Cependant, rendre les déclarations globalement visibles rompt la compositionnalité de la sémantique. Ce que vous pouvez faire pour récupérer, c'est de donner une sémantique d'élaboration pour le langage de programmation - c'est-à-dire que vous pouvez montrer comment traduire des programmes Haskell en un langage mieux composé et plus compositionnel.

En fait, cela vous donne également un moyen de compiler des classes de types - cela est généralement appelé la "traduction des preuves" ou la "transformation par dictionnaire" dans les cercles Haskell, et c'est l'une des premières étapes de la plupart des compilateurs Haskell.

Les classes de types sont également un bon exemple de la façon dont la conception du langage de programmation diffère de la théorie des types purs. Les classes de caractères sont une fonctionnalité de langage vraiment géniale, mais elles sont assez mal comportées d'un point de vue théorique. (C'est pourquoi Agda n'a pas du tout de classes, et pourquoi Coq les fait partie de son infrastructure d'inférence heuristique.)

Neel Krishnaswami
la source
quel est le finaliste candidat qui ne possède la sémantique dénotationnelle iyswim?
Ohad Kammar
1
Je n'en ai aucune idée, hélas.
Neel Krishnaswami
Est-ce que cela mérite une question supplémentaire?
Ohad Kammar
@NeelKrishnaswami: Avez-vous une idée de la façon dont les modules ML s'inscrivent dans cela? Et qu'en est-il des modules Agda (dont quelqu'un m'a dit qu'ils sont "de première classe")?
Lii
1
@Lii: les modules ML et les enregistrements Agda se comportent beaucoup mieux, mais c'est trop compliqué à expliquer dans un commentaire - posez une question à leur sujet, et moi (ou quelqu'un d'autre) vous expliquerai.
Neel Krishnaswami