coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gabriel Scherer <gabriel.scherer AT gmail.com>
- To: drg AT illinois.edu
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] binary operations on types with additional structure
- Date: Sun, 19 Jan 2014 16:41:01 +0100
> 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.
I am not convinced that this is actually different from the usual
mathematical practice. Before you introduce the notion of (semi)ring,
you may still want to be able to say things such as p*(m+n), using
elements of the same carrier set as part of two distinct algebraic
structures. A type error of the form "oh no, (m+n) lives in (X,+), how
dare you multiply it!" may be aesthetically pleasing but quickly annoy
practicioners. (And the idea that each combination of operation should
be preceded by an algebraic structure combining them, and re-exporting
combinable operations, may be a possible way to engineer and algebraic
hierarchy, but you don't want to be forced on that choice.)
In practice people rather request more identification between types
(eg. when manipulating quotient sets or subspaces) than less.
You may, however, use type abstraction to be able to protect yourself
from this mistake in cases you want to be careful. That is, instead of
defining the structure to be protective of its element by default,
give you the tools to forbid operation-mixing when you want to. You
would do that by adding an existential type to the group structure,
something like, in pseudo-coq:
Definition Group (Carrier: Type):=
{X: Type, elem: Carrier -> X, back : X -> Carrier, op: X -> X -> X, ...}
Definition op {C} {G : Group C} (a b : C) = G.back (G.op (G.elem a) (G.elem
b))
At group construction time you would simply define X as the carrier
set. But when you abstract over two groups G1 and G2 over the same
carrier, you may manipulate elements of the considered-distinct types
G1.X and G2.X to avoid any mistake.
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.
- Re: [Coq-Club] binary operations on types with additional structure, (continued)
- Re: [Coq-Club] binary operations on types with additional structure, Bas Spitters, 01/19/2014
- Re: [Coq-Club] binary operations on types with additional structure, Daniel R. Grayson, 01/19/2014
- Re: [Coq-Club] binary operations on types with additional structure, Daniel Schepler, 01/19/2014
- Re: [Coq-Club] binary operations on types with additional structure, Daniel R. Grayson, 01/19/2014
- Re: [Coq-Club] binary operations on types with additional structure, Arnaud Spiwack, 01/20/2014
- Re: [Coq-Club] binary operations on types with additional structure, Jason Gross, 01/20/2014
- Re: [Coq-Club] binary operations on types with additional structure, Arnaud Spiwack, 01/20/2014
- Re: [Coq-Club] binary operations on types with additional structure, Daniel R. Grayson, 01/20/2014
- Message not available
- Re: [Coq-Club] binary operations on types with additional structure, Daniel R. Grayson, 01/20/2014
- Re: [Coq-Club] binary operations on types with additional structure, Arnaud Spiwack, 01/22/2014
- Re: [Coq-Club] binary operations on types with additional structure, Daniel R. Grayson, 01/19/2014
- Re: [Coq-Club] binary operations on types with additional structure, Daniel Schepler, 01/19/2014
- Re: [Coq-Club] binary operations on types with additional structure, Daniel R. Grayson, 01/19/2014
- Re: [Coq-Club] binary operations on types with additional structure, Bas Spitters, 01/19/2014
Archive powered by MHonArc 2.6.18.