Sciweavers

Share
TPHOL
2008
IEEE

First-Class Type Classes

9 years 4 months ago
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 specith abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, 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.
Matthieu Sozeau, Nicolas Oury
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TPHOL
Authors Matthieu Sozeau, Nicolas Oury
Comments (0)
books