The Coq mailing list

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

Sorry, I was in a hurry.

Such a problem usually comes up with Rings which are semigroups (and monoids) in two ways.

What one solves using canonical structures or type classes is the diamond inheritance problem.

In your approach it seems that you want disallow "1*2" as 1 and 2 are really in (Z,+), not to be confused with 1 and 2 which are in (Z,*) ?

As Gabriel says, one usually tries to solve the opposite problem.

Best,

Bas

On Sun, Jan 19, 2014 at 4:18 PM, Daniel R. Grayson <drg AT illinois.edu> wrote:

Correct me if I'm wrong, but I'm under the impression that type classes can

be useful for letting coq guess what group an object is in, but it doesn't solve

the ambiguity that I point out: that there will be confusion if a type

is the type of elements of two groups.

On Sun, Jan 19, 2014 at 9:16 AM, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

Dear Dan,

We collected some references on this at the Institute:
http://uf-ias-2012.wikispaces.com/Type+classes

Best,

Bas

On Fri, Jan 17, 2014 at 8:06 PM, <drg AT illinois.edu> wrote:

One way to implement the notion of group G (for example) would be as a record,
the first element of which is the type X of the elements of the group.  The
multiplication operation could be defined with something like

   Definition op {G:Group} (g:pr1 G) (h:pr1 G) := ... .

where pr1 is projection on the first component.  If pr1 is defined as a
coercion,
then it can be written more suggestively as

   Definition op {G:Group} (g:G) (h:G) := ... .

If G' is another group sharing X with G, but not the other data, and g : G and
g' : G', then " op g g' " will be well-typed, which is mathematically
surprising
and might lead the user astray.

Assuming this issue has already been encountered in the past, I wonder what

the best solution is.  I'm tempted to say that an element g of G should be

defined
to be a pair (G,x) with x:X, and the coercion would then be the one that sends
G

to the type of such pairs.  This would be mathematically pleasing, as elements
of groups would know to which group they belong, just as elements of a type
"know" to which type they belong.

The actual situation where this arose was with two objects of a category and
the type of isomorphisms between them.