The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Section 3 of the following article discusses some practical differences:

Spitters, Bas, and Eelis Van Der Weegen. “Type Classes for Mathematics in Type Theory.” MSCS 21, no. Special Issue 04 (2011): 795–825. doi:10.1017/S0960129511000119.

http://arxiv.org/pdf/1102.1323v1.pdf

If I understand the article correctly, it recommends the former (bundled) approach for proof-irrelevant items such as your `Irrelevant`.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Mon, Jun 27, 2016 at 3:19 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

What are the differences between typeclass substructures and superclasses?

For instance, suppose I have:


Class Irrelevant T := { all_the_same : forall a b : T, a = b }.

Class Singular T := { irr :> Irrelevant T; unique : T }.

Class Singular2 T `{irr : Irrelevant T} := { unique2 : T }.


What is the difference between Singular and Singular2? Is there a semantic difference?  Are there situations in which one is preferable to the other?

-- Jonathan