The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> "BCP" == Benjamin C Pierce 
>>>>> <bcpierce AT cis.upenn.edu>
>>>>>  writes:

BCP> In preparation for the upcoming DeepSpec summer school, I’m working on
BCP> putting together an “even gentler tutorial” on typeclasses in Coq. I’d be
BCP> grateful for the community’s advice on what are the most important / most
BCP> used typeclasses in the standard libraries (or in widely used contributed
BCP> libraries).

I most use Equivalence (and it's related type classes) and Proper.

BCP> More generally, I’d love to hear opinions on pragmatic aspects of
BCP> typeclasses and how to get newcomers up to speed… E.g.: What are the most
BCP> puzzling gotchas that people new to coq’s typeclasses tend to get stuck
BCP> on, and what are some good strategies for getting un-puzzled? What advice
BCP> should be given to new typeclass users to avoid getting themselves in
BCP> trouble? What are the tradeoffs between typeclasses and other modularity
BCP> mechanisms in Coq. Thanks!

One thing that always gets me is that overlapping instances are easy to write
with no warning from Coq (unlike Haskell, which ensures that resolution always
pick a single instance). This requires me to often use:

    Typeclasses eauto := debug.

and switch to my *coq* buffer to see which lookup did not resolve to the
instance I was expecting. This is usually fixed by one of two things:

  1. Change the "priority" of the overlapping instance (something we cannot do
     in Haskell).

  2. Change the Instance to a Definition -- which I can still use it as an
     explicitly passed dictionary, but this removes it from resolution.


Another scenario that often bites me is when I define an instance for a type
class, and then intend to write a function using the type class and forget to
provide it as an argument. In Haskell this would be an error, but in Coq it
just resolves to whatever the last globally defined instance was.

For example, say I write a function that uses a functor, but forget to mention
the functor:

    Definition foo (C D : Category) (x y : C) (f : x ~> y) : fobj x ~> fobj y 
:=
      fmap f.

In Haskell this gives an error stating that no Functor is available. In Coq,
it type checks using the highest priority C --> D functor instance in scope. I
typically discover that this has happened when I try to use [foo] and find the
Functor to be too specific, or by turning on Printing All and looking at the
definition of `foo`. However, there are times when `foo` is deep down in an
expression, and then it's not obvious *at all* why it's failing.

The other way to solve this is to manually ensure there are no Instance
definitions that might overlap, such as a generic Instance for C --> D, but
only instances from specific categories to specific categories (though again,
I might define several functors of that same type). It would be nice if I
could make this situation into an error.


Finally, there is the dreaded "diamond problem", when referring to type
classes as record members rather than type indices:

    Class Foo := {
      method : Type -> Type
    }.

    Class Bar := {
      bar_is_foo :> Foo
    }.

    Class Baz := {
      baz_is_foo :> Foo
    }.

    Class Oops := {
      oops_is_bar :> Bar
      oops_is_baz :> Baz
    }.

Oops refers to two Foos, and I need explicit evidence to know when they are
the same Foo. I work around this using indices:

    Class Foo := {
      method : Type -> Type
    }.

    Class Bar (F : Foo) := {
    }.

    Class Baz (F : Foo) := {
    }.

    Class Oops (F : Foo) := {
      oops_is_bar :> Bar F
      oops_is_baz :> Baz F
    }.

Only those classes which might be multiply-inherited need to be lifted like
this. It forces me to use Sections to avoid repetition, but allows Coq to see
that base classes sharing is plainly evident.

The main gotcha here for the newcomer is that it is not obvious at all when
the diamond problem is what you're facing, since when it hits the parameters
are hidden indices, and you end up with goals like:

    A, B : Type
    F : Foo
    O : Oops
    H : @method (@bar_is_foo (@oops_is_bar O)) A = @method F B
    --------------------
    @method F A = @method F B

You can't apply here without simplying in H. However, what you see at first
is:

    A, B : Type
    F : Foo
    O : Oops
    H : method A = method B
    --------------------
    method A = method B

As a newcomer, knowing to turn on Printing All is just not obvious here, but
it quickly becomes something you learn to do whenever what looks obvious is
not.


Other than these things, I use type classes heavily in my own libraries, and
very much enjoy the facility they provide. I have a category-theory library
that is nearly all type classes, and I ran into every one of the problems
described above, before learning how to "work with Coq" to make things happy.

-- 
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2