Stream: Coq users

Topic: Records and Typeclasses


view this post on Zulip Rich Hilliard (Aug 22 2021 at 17:22):

I can refer to the fields of record instances in two ways:

Record Point := mkPoint { px : nat; py : nat }.
Definition r : Point := mkPoint 6 7.
Compute r.(px) + r.(py).
Compute (px r) + (py r).

But these fail with typeclasses:

Class PointD := mkPointD { dx : nat; dy : nat }.
Definition rd : PointD := mkPointD 6 7.
Fail Compute rd.(dx) + rd.(dy).
Fail Compute (dx rd) + (dy rd).
=> Illegal application (Non-functional construction):
The expression "dx" of type "nat" cannot be applied to the term "rd" : "PointD"

Is there a way to refer to typeclass methods or is there a basic difference here, and if so, how can I learn more about the differences? (I've looked at the Reference Manual and M. Sozeau's original papers on typeclasses.)

view this post on Zulip Théo Winterhalter (Aug 22 2021 at 17:26):

What if you used @dx instead?

view this post on Zulip Théo Winterhalter (Aug 22 2021 at 17:27):

I think what happens is that when dx is defined, its PointD argument is automatically made implicit and since rd.(dx) is another way of writing dx rd the error happens (it does tell you that dx is of type nat).

view this post on Zulip Rich Hilliard (Aug 22 2021 at 17:37):

Thank you! I missed the change to an implicit argument.

view this post on Zulip Théo Winterhalter (Aug 22 2021 at 17:39):

You're welcome. You can use About dx or so to check this kind of thing.


Last updated: Mar 28 2024 at 20:01 UTC