The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Dear Abhishek,

Thanks for this. For bystanders, the corresponding library is here:
http://math-classes.github.io/

Bas

On Mon, Jun 19, 2017 at 4:35 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
 wrote:
> Typeclasses are merely about inferring some implicit arguments using proof
> search. The underlying modularity mechanism, which is the ability to define
> "existential types" using induction, was ALWAYS there in Coq: typeclasses
> merely cuts down on verbosity because more arguments can now be implicit
> because they can be automatically inferred.
> Relying on proof search often brings predictability concerns. So, guidance
> on taming proof search would be very useful: Chapter 13 of CPDT might be a
> good background for using typeclasses.
> Also, it is good to keep in mind that if typeclass-resolution fails to
> instantiate an implicit argument, some/all of those arguments can be
> provided manually. Often, just providing one such implicit argument gives
> enough clues to the inference engine to infer all of them. I think it is
> important to emphasize that typeclass arguments are just implicit arguments.
>
> Also, another design decision in typeclasses/records is whether to unbundle.
> The following paper makes a great case for unbundling:
> 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
>
> I think the above paper is missing one argument for unbundling:
> I've seen many libraries that begin by making an interface (say I) that
> bundles ALL the operations (and their correctness properties) they will EVER
> need and then ALL items in the library (say L) are parametrized by over I.
> A problem with this bundled approach is impossible to use ANY part of D if
> you are missing ANY operation (or proof of a logical property of the
> operation) in the interface I, even if parts of D don't actually need that
> operation: I've run into situations where it is impossible to cook up an
> operation that 90% of L doesn't use anyway.
> When using the unbundled approach, one can use Coq's Section mechanism to
> ensure that definitions/proofs only depend on items of the interface they
> actually use, and not on a big bundle.
>
>
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
>
> On Mon, Jun 19, 2017 at 8:45 AM, Pierre Courtieu 
> <pierre.courtieu AT gmail.com>
> wrote:
>>
>> Hi
>>
>> my biggest problem with typeclasses is the error messages of the
>> unification engine. It is really hard, even for confirmed users, to figure
>> out from the message why some statement can't be coerced to something
>> typable.
>>
>> Something should be said about typeclasses vs functors/modules but I never
>> came to a clear conclusion about it.
>>
>> P.
>>
>>
>>
>> 2017-06-19 14:00 GMT+02:00 Benjamin C. Pierce 
>> <bcpierce AT cis.upenn.edu>:
>>>
>>> In preparation for the upcoming DeepSpec summer school, I’m working on
>>> putting together an “even gentler tutorial” on typeclasses in Coq.  I’d be
>>> grateful for the community’s advice on what are the most important / most
>>> used typeclasses in the standard libraries (or in widely used contributed
>>> libraries).  I plan to use a couple of these as running examples and make 
>>> a
>>> list of the rest so that people know they are there.
>>>
>>> More generally, I’d love to hear opinions on pragmatic aspects of
>>> typeclasses and how to get newcomers up to speed… E.g.:
>>>
>>> What are the most puzzling gotchas that people new to coq’s typeclasses
>>> tend to get stuck on, and what are some good strategies for getting
>>> un-puzzled?
>>> What advice should be given to new typeclass users to avoid getting
>>> themselves in trouble?  What are the tradeoffs between typeclasses and 
>>> other
>>> modularity mechanisms in Coq.
>>>
>>> Thanks!
>>>
>>>     - Benjamin
>>>
>>>
>>
>