Ich kann naiv eine Hierarchie von algebraischen Strukturen in Coq mit Hilfe von Typklassen konstruieren. Ich habe Probleme, Ressourcen für Coqs Syntax und Semantik für Typklassen zu finden. Ich glaube jedoch, dass das Folgende eine korrekte Implementierung von Halbgruppen, Monoiden und kommutativen Monoiden ist:
%Vor% Wenn ich richtig verstehe, können zusätzliche Parameter (z. B. das Identitätselement eines Monodens) hinzugefügt werden, indem zuerst Monoid eine Instanz von Semigroup deklariert und dann auf id : A parametrisiert wird. In dem für AbelianMonoid konstruierten Datensatz tritt jedoch etwas Ungewöhnliches auf.
Dies geschah, als ich versuchte, eine Klasse für Halbgruppen zu erstellen. Ich dachte, dass die folgende Syntax korrekt war:
%Vor% Ich konnte jedoch nicht die richtigen Operatoren und Identitätselemente disambigutieren. Das Drucken der Aufzeichnungen ergab die oben beschriebenen Probleme. Also habe ich zwei Fragen: Erstens, wie deklariere ich korrekt die Klasse Monoid ; Zweitens, wie kann ich Funktionen in Superklassen disambiguieren?
Was ich wirklich gerne hätte, wären gute Ressourcen, die Coqs Typklassen ohne antiquierte Syntax klar erklären. Zum Beispiel dachte ich, dass Huttons Buch die Klassen in Haskell klar erklärte.
Referenzen:
Die kanonischen Referenzen für Typklassen in Coq - über das Handbuch - sind diese Arbeit und die These (in französischer Sprache) von Matthieu Sozeau . Es gibt weniger kanonische Verweise (mit unterschiedlichen Standpunkten) auf der Forschungsebene in einem aktuellen Papier und in mein These . Sie sollten auch einige Zeit auf dem #coq-Kanal von Freenode verbringen und die Mailingliste abonnieren .
Ihr Problem:
Das Syntaxproblem ist nicht mit Classes per se, sondern mit maximal eingefügt < a href="http://coq.inria.fr/refman/Reference-Manual004.html#toc20"> implizite Argumente . Die Monoid und AbelianMonoid Typen haben in Ihrer Definition (implizit) parametrische Argumente, die in dieser Reihenfolge der Domain-Typ, die Operation und die Identität sind - wie vom abhängigen Produkt indiziert Sie werden beim Drucken dieser Datensatztypen vollständig erweitert angezeigt. Sie werden automatisch ausgefüllt, wenn Sie das abhängige Produkt ohne seine Argumente in einer Position angeben, in der es benötigt wird.
Tatsächlich fügt die implizite Argumentauflösung automatisch die erforderlichen Parameterargumente ein, damit sie identisch sind (für beide Produkte, die von ihnen abhängen: P und M 's Typen), wenn sie auf ihren eigenen Geräten belassen werden. Sie müssen nur Einschränkungen zwischen diesen Bezeichnern angeben, indem Sie für die verschiedenen Bezeichner Variablen angeben, die gegebenenfalls eindeutig sind:
Das Ergebnis:
%Vor%Beachten Sie, dass die Identitäten für das abelsche Monoid und Monoid diesmal verschieden sind. Es ist eine gute Übung (auch wenn es wenig mathematischen Sinn macht), sich selbst zu üben, den Datensatztyp (auch Klasse genannt) zu schreiben, den man haben möchte, wenn man für die additiven und multiplikativen Strukturen dasselbe Identitätselement hätte.
Tags und Links scope coq functional-programming typeclass