The Coq mailing list

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

Regarding the comparison between type classes and structures.

LEAN seems to have some nice support for Type Classes/Structures; see
https://leanprover.github.io/tutorial/

Chapter Structures.

They have a type class implementation, but provide some mechanisms for
extending and renaming structures. It seems light weight, but the
repackaging that is done behind the scenes looks really helpful and
natural.

It seems like it would be useful for Coq too, as it allows a nice
combination of the conveniences of both the unbundled approach (as in
math-classes) and package classes (as in ssreflect).

On Tue, Jun 20, 2017 at 1:57 PM, Bas Spitters 
<b.a.w.spitters AT gmail.com>
 wrote:
> 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
>>>>
>>>>
>>>
>>