Eine mathematische (kategoriale) Beschreibung von Typklassen

Eine funktionale Sprache kann als eine Kategorie angesehen werden, in der ihre Objekte Typen sind und Morphismen zwischen ihnen funktionieren.

Wie passen Typklassen in dieses Modell?

Ich gehe davon aus, dass wir nur die Implementierungen berücksichtigen sollten, die die Bedingungen der meisten Typklassen erfüllen, aber nicht in Haskell ausgedrückt werden. Zum Beispiel sollten wir nur diejenigen Implementierungen betrachten, Functorfür die fmap id ≡ idund fmap f . fmap g ≡ fmap (f . g).

Oder gibt es andere theoretische Grundlagen für Typklassen (zum Beispiel basierend auf typisierten Lambda-Kalkülen)?

Wie passen Typklassen in dieses Modell?

Die kurze Antwort lautet: Sie tun es nicht.

Wann immer Sie Zwänge, Typklassen oder andere Mechanismen für den Ad-hoc-Polymorphismus in eine Sprache einführen, ist das Hauptproblem des Designs die Kohärenz .

Grundsätzlich müssen Sie sicherstellen, dass die Typklassenauflösung deterministisch ist, damit ein gut typisiertes Programm eine einzige Interpretation hat. Wenn Sie beispielsweise mehrere Instanzen für denselben Typ im selben Bereich angeben, können Sie möglicherweise mehrdeutige Programme wie das folgende schreiben:

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

Je nachdem, welche Instanz der Compiler auswählt, blah vkann entweder "Hello"oder gleich sein "Goodbye". Daher würde die Bedeutung eines Programms nicht vollständig durch die Syntax des Programms bestimmt, sondern könnte durch willkürliche Entscheidungen des Compilers beeinflusst werden.

Haskells Lösung für dieses Problem besteht darin, dass jeder Typ für jede Typklasse höchstens eine Instanz hat. Um dies zu gewährleisten, erlaubt es Instanzdeklarationen nur auf oberster Ebene und macht darüber hinaus alle Deklarationen global sichtbar. Auf diese Weise kann der Compiler bei einer mehrdeutigen Instanzdeklaration immer einen Fehler melden.

Das globale Sichtbarmachen von Deklarationen bricht jedoch die Kompositionalität der Semantik. Zur Wiederherstellung können Sie eine Ausarbeitungssemantik für die Programmiersprache angeben. Das heißt, Sie können zeigen, wie Sie Haskell-Programme in eine besser funktionierende, kompositorischere Sprache übersetzen.

Dies gibt Ihnen tatsächlich auch die Möglichkeit, Typenklassen zu kompilieren - in Haskell-Kreisen wird dies normalerweise als "Übersetzung von Beweisen" oder "Dictionary-Passing-Transformation" bezeichnet und ist eine der frühen Phasen der meisten Haskell-Compiler.

Typenklassen sind auch ein gutes Beispiel dafür, wie sich das Design von Programmiersprachen von der reinen Typentheorie unterscheidet. Typenklassen sind ein wirklich großartiges Sprachfeature, aber sie verhalten sich unter beweistheoretischen Gesichtspunkten ziemlich schlecht. (Aus diesem Grund hat Agda überhaupt keine Typenklassen und Coq macht sie zu einem Teil seiner heuristischen Inferenzinfrastruktur.)