First-Class Type Classes

Abstract : Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these con- structs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and integrates well inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.
Type de document :
Article dans une revue
Lecture notes in computer science, springer, 2008, 〈10.1007/978-3-540-71067-7_23〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00628864
Contributeur : Matthieu Sozeau <>
Soumis le : mardi 4 octobre 2011 - 13:51:45
Dernière modification le : mardi 24 avril 2018 - 13:38:49

Lien texte intégral

Identifiants

Collections

Citation

Matthieu Sozeau, Oury Nicolas. First-Class Type Classes. Lecture notes in computer science, springer, 2008, 〈10.1007/978-3-540-71067-7_23〉. 〈inria-00628864〉

Partager

Métriques

Consultations de la notice

102