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

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)?

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.)