Email Gateway (Aug 18 2022 at 13:01): Email Gateway (Aug 18 2022 at 13:01):From: Andrei Popescu <uuomul@yahoo.com>
Hello,
As far as I see, type classes do not allow multiple type
variables. Concretely, say I
want to reason about vector spaces (K,V,+,*,...) without having either of K and V fixed. Is there any elegant way around this?
Thank you in advance for any hint,
Andrei Popescu
Email Gateway (Aug 18 2022 at 13:01):From: Amine Chaieb <ac638@cam.ac.uk>
Dear Andrei,
It might not be the most elegant way. In the recent snapshot development
there is theory in HOL/Library/Finite_Cartesian_Product.thy which
introduces a new type constructor "'a ^ 'n" which represents 'a * ... 'a
and this as many times as 'n has inhabitants. This is true only if 'n
has finitely many inhabitants.
Of course this is more restrictive that an abstract view, but better
than nothing. You can also look at an other new theory in
HOL/Library/Euclidean_Space.thy, where it is shown that e.g is 'a is a
group, then so is 'a^'n etc. for several interesting algebraic classes.
So you get implicitly that it is a vector space (there is scalar
multiplication) but this is not a class.
On the other hand, if you want to have thing really general and nice,
you could use locales.
Best wishes,
Amine.
Andrei Popescu wrote:
Email Gateway (Aug 18 2022 at 13:02):From: Tim McKenzie <tjm1983@gmail.com>
On Friday 20 February 2009 12:23:17 Andrei Popescu wrote:
Have you looked at using locales? I'm just learning about them myself at the
moment, and all the examples I've seen in the documentation use only one type
variable, but I don't immediately see why locales wouldn't work with more than
one type variable.
Tim
<><
signature.asc
Last updated: May 03 2024 at 08:18 UTC