agda-stdlib
agda-stdlib copied to clipboard
agda
Support for abstract vector spaces.
This PR introduces Algebra.Linear.VectorSpace, an abstract vector space.
The purpose of this new type is to provide the familiar metaphor/interface of "vector/matrix" that people are used to using in their client code, without locking the back-end implementation into arrays (more generally, n-tuples). In this way, we hope to decouple the capture of design intent from design implementation, for architectures based on the concepts of linear algebra, such as machine learning networks.
It would be great if you could either merge or rebase this on top of current master. I'll then review it :+1:
I'm... uncomfortable with this definition of vector spaces. It's really not what literature means by "vector space", like, at all. If anything I'd call this a free inner-product module, but that's not really a thing, and besides a definition of that ought to take into account complex conjugates somehow.
I'm... uncomfortable with this definition of vector spaces. It's really not what literature means by "vector space", like, at all. If anything I'd call this a free inner-product module, but that's not really a thing, and besides a definition of that ought to take into account complex conjugates somehow.
Hi @Taneb ,
Thanks for voicing your concern here. :)
Is it just the separation of the basis set and inner product, which has evolved in the back and forth between Matthew and me, here, or is there something else that you feel is fundamentally wrong with my definition of vector space?
Thanks, -db
Anyone know why the Ubuntu build / test-stdlib (pull_reuest) test failed?
From Wikipedia (https://en.wikipedia.org/wiki/Vector_space), I think that Vector Space is defined over a Field and not from a Commutative Ring.
Anyone know why the Ubuntu build / test-stdlib (pull_reuest) test failed?
Not your fault (https://github.com/agda/agda-stdlib/issues/1804)
From Wikipedia (https://en.wikipedia.org/wiki/Vector_space), I think that Vector Space is defined over a Field and not from a Commutative Ring.
Thanks @Taneb and @guilhermehas for the heads up! I'd totally missed that. It's a good point. @capn-freako I think they're right that we should stick to the standard definition. May I ask where you go the current definition from?
Thanks @Taneb and @guilhermehas for the heads up! I'd totally missed that. It's a good point. @capn-freako I think they're right that we should stick to the standard definition. May I ask where you go the current definition from?
Admittedly, I "cheated" when I didn't find Field available among the other standard algebraic definitions.
Shall I take a whack at defining Field and, then, redefining VectorSpace to use it, instead of CommutativeRing?
I think we'll need division eventually, anyway, when working most generally w/ vector spaces, even abstractly.
You're likely to want to define R-module over a (commutative?) ring first. That's fully constructive. Vector Space over a Field is... hard.
You're likely to want to define R-module over a (commutative?) ring first. That's fully constructive. Vector Space over a Field is... hard.
Thanks, Jacques! Have you been down that particular road before?
I like this concise summary of Field (from the Wikipedia page):
Even more summarized: a field is a commutative ring where 0 ≠ 1 and all nonzero elements are invertible.
You're likely to want to define R-module over a (commutative?) ring first. That's fully constructive. Vector Space over a Field is... hard.
Oh, shoot! The new multiplicative inverse function must be partial, because 0# must be excluded from its domain.
Is that why you warned me thusly?
Hey guys, a question about something in Algebra.Structures:
In IsRingWithoutOne, the additive inverse is defined thusly:
+-isAbelianGroup : IsAbelianGroup + 0# -_
while in IsNearring it is defined:
+-inverse : Inverse 0# _⁻¹ +
What is the significance of this difference?
Oh, shoot! The new multiplicative inverse function must be partial, because 0# must be excluded from its domain. Is that why you warned me thusly?
Yes we haven't quite worked out how we want to handle the partiality. See https://github.com/agda/agda-stdlib/issues/1175 for discussion.
What is the significance of this difference?
It's an artefact of the order of inheritance. One inherits from IsQuasiring and the other from IsAbelianGroup. In general it's very difficult to come up with a consistent inheritance pattern and is an area of active research how to do it modularly (which we have definitely not achieved in the standard library!)
Have you been down that particular road before?
Not this exact one, but close enough to know that this way lies much pain.
Oh, shoot! The new multiplicative inverse function must be partial, because 0# must be excluded from its domain. Is that why you warned me thusly?
Yes!
Matthew also said:
In general it's very difficult to come up with a consistent inheritance pattern and is an area of active research how to do it modularly (which we have definitely not achieved in the standard library!)
In my mind, the most general solution requires explicit morphisms between definitions (not just embeddings induced by same-name-same-thing) and a proper notion of pullback/pushout. Agda actually has many of the needed features already, but "closing the gap" still requires quite a lot of work.
@capn-freako I'm going to close this PR as I think the current approach needs some rethinking and probably some addition scaffolding first. Feel free to open a new PR if you revisit it later on and think you've fixed the problems!
Oh, snap! I was just putting the finishing touches on a next push, which I think addresses the concerns and is much more in line w/ the literature. Any chance you could reopen this PR for one more round?
Okay, guys, I think that last push is much more in line with the literature and addresses your previous concerns. Please, take a look and let me know what you think.
Thanks! -db
Given @Taneb's feedback and the lack of reply I'm going to close this again for now.