coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] difference between typeclass substructures vs. superclasses

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] difference between typeclass substructures vs. superclasses
Date: Mon, 27 Jun 2016 15:19:00 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f182.google.com
Ironport-phdr: 9a23:aRu9eB/3hJdTo/9uRHKM819IXTAuvvDOBiVQ1KB91eIcTK2v8tzYMVDF4r011RmSDN2dsqsP0rCI+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwud7yzQ9eZ1p7pn8mJuLTrKz1SgzS8Zb4gZD6Xli728vcsvI15N6wqwQHIqHYbM85fxGdvOE7B102kvpT41NdZ/i9Ro/Ms8dJbGeW/JvxgDO8QMDNzGGcsrObvqBOLGQCI/z4XVngcuhtOGQnMqh/gCMTfqCz/48h63iCGPcTwBZQ5WCqv6bsjHB3vjiYEOjo0/UnYj8VxiORQpxf39E83+JLdfIzAbKk2RajaZ95PADMZBss=

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

[Coq-Club] difference between typeclass substructures vs. superclasses, Jonathan Leivent, 06/27/2016
- Re: [Coq-Club] difference between typeclass substructures vs. superclasses, Abhishek Anand, 06/27/2016
  - Re: [Coq-Club] difference between typeclass substructures vs. superclasses, Jonathan Leivent, 06/28/2016