Closed milibopp closed 8 years ago
This is excellent! I was wondering if there might be a way of abstracting over operators.
Thoughts @darinmorrison?
By the way, sorry for being missing in action this past week or so . I just started full time work again and I've been a little drained. Hopefully I'll be able to acclimatise again this week so that I can get back to it.
Need to think about this some more. One approach I've been using is to define Magma
separately from MagmaMultiplicative
and then have a wrapper struct MgM
which lifts any Magma
into a canonical MagmaMultiplicative
. The advantage to this approach is that type inference still works. It's a bit more verbose but not too bad: see here. I had an idea on how to make this nicer with a macro but hadn't gotten around to it.
First, thanks for putting this together @aepsil0n.
Moving to a different design for dealing with operators is something I'd like. I'm not quite sure about the proposal for a couple of reasons though.
For one, I don't see how this will work for non-numeric types which is still my primary interest. For example, due to the coherence restrictions, we can't implement Add
or Mul
for builtin non-numeric types even when it makes perfect sense to do so from the point of view of abstract algebra. For those types, the extra Closed
constraint would be a burden since in some cases there is no underlying operator already defined. We'd already have to use wrapper structs in that case.
Secondly, it feels a little awkward conceptually for Magma
to need an underlying trait since it is already supposed to be the abstraction of an operator. I think we can start with Magma
, defining most of the machinery around that, and specialize it to specific operators rather than going the other way around. This would correspond to defining a particular impl for Closed
and we should still be able to use multiple notions of a Magma
or other trait in a more elaborate structure.
This is how I've been doing it in the epsilonz/algebra.rs library:
pub trait Magma
{
fn op(&self, rhs:&Self) -> Self;
}
pub trait MagmaAdditive
: Magma
+ Add<Self, Self>
{}
impl<A> MagmaAdditive for A
where
A: Magma,
A: Add<A, A>
{}
pub trait MagmaMultiplicative
: Magma
+ Mul<Self, Self>
{}
impl<A> MagmaMultiplicative for A
where
A: Magma,
A: Mul<A, A>
{}
and then I have some free/canonical implementations:
impl<A> Magma for MgA<A>
where
A: Magma,
{
#[inline]
fn op(&self, rhs: &MgA<A>) -> MgA<A> {
let &MgA(ref lhs) = self;
let &MgA(ref rhs) = rhs;
MgA(lhs.op(rhs))
}
}
impl<A> Add<MgA<A>, MgA<A>> for MgA<A>
where
A: Magma,
{
#[inline]
fn add(&self, rhs: &MgA<A>) -> MgA<A> {
self.op(rhs)
}
}
impl<A> Magma for MgM<A>
where
A: Magma,
{
#[inline]
fn op(&self, rhs: &MgM<A>) -> MgM<A> {
let &MgM(ref lhs) = self;
let &MgM(ref rhs) = rhs;
MgM(lhs.op(rhs))
}
}
impl<A> Mul<MgM<A>, MgM<A>> for MgM<A>
where
A: Magma,
{
#[inline]
fn mul(&self, rhs: &MgM<A>) -> MgM<A> {
self.op(rhs)
}
}
Further traits are defined in terms of just Magma
:
pub trait Semigroup: Magma
{
#[inline]
fn app(&self, rhs:&Self) -> Self {
self.op(rhs)
}
}
pub trait Monoid: Semigroup
{
fn nil() -> Self;
}
Then you can use the specific operators like in the earlier link I posted to the FingerTree
example.
You are right in that I have introduced an unnecessary additional level of indirection. This was mainly due to separating the operator from the equality requirement, but I guess Eq
is actually independent of Magma
.
However, I do not think that your approach actually solves the problem I wanted to address with this issue, as I can not require a type to be two different kinds of magmas (or semigroups or whatever) without specializing to some concrete operators. And as I see it this is especially important for non-numeric types, where the operations in question are not +
or *
. To unify both our approaches, I would still like to keep the unit structs to identify an operator and essentially rename Closed
to Magma
:
trait Magma<Op> {
fn op(&self, rhs: &Self) -> Self;
}
I think about the type parameter Op
here more as an abstraction of the symbol, rather than an abstraction of the actual operation (which is what Magma<Op>
does and previously my Closed<Op>
did). Your canonical implementations would still work but you would have MagmaAdditive: Magma<Addition> + Add<Self, Self>
. But in addition this allows us to impose generic trait bounds like Magma<Op1> + Magma<Op2>
, which I think is extremely valuable to make these abstractions more composable.
To put this in the theoretical context (quoting Wikipedia):
A magma is a set M matched with an operation "⋅" that sends any two elements a,b ϵ M to another element a ⋅ b.
Here a type implementing Magma<Op>
then corresponds to M, and Op
corresponds to "⋅". Without genericity over the operator, the trait simply does not capture the possibility that there may be multiple operations defined on a set, which satisfy this property. (Is there a type theoretical formulation of this? I figure it might be more useful in the context of a type system.)
Now the downside is, of course, that we loose type inference. But if you think about it looking at an expression like a.op(&b)
, I would say, that it is not clear what this means, if a
, b
are, say, elements of some group. It may be the group operation or the operation implied by the existence of an inverse ("division"), as both make the group a magma. For fields the situation becomes more complex.
So in essence I think it is actually a good thing that you'd have to write Magma<Op1>::op(&a, &b)
for clarity. Of course it is a bit tedious in a context, where you really only have one operation. But I would argue that it's worth the benefits.
btw, to address the connection to concrete operators a bit more we should totally have all of the following concrete operator unit structs and possibly more
struct Addition;
struct Substraction;
struct Multiplication;
struct Division;
struct StringConcatenation;
struct FunctionComposition;
and connect them to the relevant functionality using a mechanism like your MagmaAdditive
. So if you really want to work with concrete operators but abstract types, you can impose trait bounds like these:
T: MagmaStringConcatenative,
F: Field<Addition, Multiplication, Substraction, Division> + MagmaAdditive + MagmaMultiplicative + MagmaSubtractive ...
The latter for example could probably be wrapped into a CanonicalField
trait.
You are right in that I have introduced an unnecessary additional level of indirection. This was mainly due to separating the operator from the equality requirement, but I guess Eq is actually independent of Magma.
Yes, I think this will need to be the case otherwise we can only implement magmas with decidable equality. Any algebraic structures having closures in them or infinite objects like streams will often not have decidable equality. In fact, not even the real numbers have a decidable equality.
In type theory, one usually builds on the notion of a setoid, which is something like a type theoretic equivalence relation. It's possible to prove that two things are equal (e.g., real numbers, functions) even when there is no general algorithm that can determine their equality. So every higher algebraic structure would have the laws specified up to some particular notion of equivalence given by the underlying setoid.
We don't have dependent types in Rust though so we can't encode setoid. But we also can't specify the laws as part of the implementation without dependent types either, so I think it makes sense in light of the limitations to not mandate Eq
. The idea is that there would be a separate trait expressing that laws are decidable in some case, which I think is what the spire folks are doing.
However, I do not think that your approach actually solves the problem I wanted to address with this issue, as I can not require a type to be two different kinds of magmas (or semigroups or whatever) without specializing to some concrete operators.
[…]
Here a type implementing Magma
then corresponds to M, and Op corresponds to "⋅". Without genericity over the operator, the trait simply does not capture the possibility that there may be multiple operations defined on a set, which satisfy this property. (Is there a type theoretical formulation of this? I figure it might be more useful in the context of a type system.)
Okay I think I understand your intention better now. In type theoretic formulations of algebra, there are two approaches to encoding these structures. One is how you suggest where you parameterize the structures over their operations and other parts. Another is the bundled/packed approach, where there is no parameterization and everything is kept abstract.
Usually the motivation for using the parametric approach is to facilitate sharing of the components of a structure (e.g., two structures have the same carrier but different operations). However, in my experience, parametric approaches tend to lead to an explosion of parameters as their hierarchy is developed, negatively impacting usability. Most successful developments of algebra in type theory and programming languages that I am aware of avoid it in favor of the bundled approach because of this.
I think this particular case of wanting to express that a thing is a magma in at least two different senses points to a problem with traits/type-classes that we would be able to avoid with something like ML modules. Given that instance/impl resolution is type directed and expected to be unique, using Op
to work around this (rather than to facilitate sharing) feels like the wrong approach to me.
I think the usual answer to this problem is to use wrapper structs:
type A;
struct MagmaOne(A);
impl Magma for MagmaOne { … }
struct MagmaTwo(A);
impl Magma for MagmaTwo { … }
The wrapper structs let us "name" the different Magma
instances. It becomes a bit more cumbersome but I don't see another way without losing type inference and I think that's something we really, really want to avoid giving up.
Now the downside is, of course, that we loose type inference. But if you think about it looking at an expression like a.op(&b), I would say, that it is not clear what this means, if a, b are, say, elements of some group. It may be the group operation or the operation implied by the existence of an inverse ("division"), as both make the group a magma. For fields the situation becomes more complex.
It shouldn't be ambiguous what the operations mean because when there are multiple possibilities in higher structures they will have different names. If we want to forget the richer structure (e.g., treat a Group
as a Magma
) and there are again multiple possibilities, I think this is another case where we would want to use wrapper structs to drive implementation resolution (e.g., for H: HigherStructure
one would have ThisMagma<H>
and ThatMagma<H>
).
Ok, now it makes a lot more sense to me, why you objected to my initial idea. Thanks for taking the time to explain this. I have to admit, that the wrapper struct approach feels more ergonomic. However, I still think it is a little awkward to use, when a type (not a trait) has a certain abstract algebraic structure in two or more different senses, because then you can implement the corresponding trait only once, even though one view may not be more natural then the other. But I guess that's a more acceptable trade-off than the long list of type parameters I suggested.
We should probably wrap the essence of this discussion up as documentation at some point and file an issue to provide all these wrapper structs.
However, I still think it is a little awkward to use, when a type (not a trait) has a certain abstract algebraic structure in two or more different senses, because then you can implement the corresponding trait only once, even though one view may not be more natural then the other
Yeah, I definitely agree with you there. As I alluded to, this is one of the big flaws with traits/type-classes (also see this rfc thread). The coherence/global-uniqueness requirement forces you to make an arbitrary choice. If you need to work with alternate implementations, you have to do the manual bookkeeping with wrapper structs.
We should probably wrap the essence of this discussion up as documentation at some point and file an issue to provide all these wrapper structs.
Good idea.
There's another catch with wrapper structs. The MgA
/MgM
structs in your example contain an object directly, so they cannot be thought of as a view. I'm thinking of code like the following:
/// Some magma operation
fn f<M: Magma>(a: &M) -> M;
/// Some group operation
fn g<G: Group>(a: &G) -> G;
/// Another group that reuses magma code in the divisive sense
fn h<G: Group + Copy>(a: &G, b: &G) -> G {
let AlternativeMagma(transformed) = f(&AlternativeMagma(*a));
transformed.group_op(&g(b))
}
The problem here is that G
needs to be Copy
in the last example, as one can't move out of a reference. I think the fundamental problem is, that a view should not own the underlying data, but only keep a reference to them. But then again you cannot implement the Magma trait on it, because the op
method would have to return a reference to a new object, which makes no sense lifetime-wise. Is there any way to work around this?
Ah, yeah. There's definitely some complexity here that I haven't thought too carefully about yet. Mostly I was waiting to see what happened with the reform with numeric stuff in std
. This is also why the algebra library I was working on is currently broken :)
I think we will have to end up using associated types somehow but I'm not sure what it should look like yet and what exactly we would be able to get away with. Might be good to make a separate issue about this one actually.
This is a really good discussion! Thanks for putting so much time into your posts.
My concern is that I really find the wrapper-type style harder to grok from an API point of view, compared with @aepsil0n's type parameter style, although I also accept that 'type parameter explosions' could be an issue. It might help me to see something like a Vector3<T>
implemented using the wrapper style.
/cc. @aturon
I'm putting together an example using Vector3<T>
for both my proposal here and #19.
I guess what I'm saying is we do have to think ergonomics. We have to juggle the usability and grokability for both our clients (library authors) and our clients' clients (the users of those libraries).
True, essentially we want people to be able to write code in terms of e.g. an abstract field and have it work for their field-like data structures and so on. And it shouldn't be too messy compared to the less abstract approach. Point is I need to see the application of something myself, as I can't quite picture it yet in more complex situations than the magma/group case discussed here.
Here it is: https://gist.github.com/aepsil0n/5ab39051f0b09620f824
A couple of observations about the differences between wrapper.rs
and parametric.rs
:
wrapper.rs
is 50 loc longer, which is mostly due to the additional wrapper structsField<Add, Mul>: AddGroup<Add> + Group<Mul>
, the default is to use multiplication. So Group::<Mul>::group_op(&a, &b)
and a.group_op(&b)
are equivalent for a
, b
in some field F: Field<Add, Mul>
. (Not sure whether that is a sensible default though.)In essence, we have to decide between type inference and support for alternate views.
So, given the current impl resolution mechanism in Rust, the parametric approach is more powerful. Nonetheless, @darinmorrison convinced me that the non-parametric approach is "the right thing" to do. But I'm afraid it can't be done correctly at the moment. So once again I tend to favour the parametric version, even though it is a bit hacky.
I guess what I'm saying is we do have to think ergonomics. We have to juggle the usability and grokability for both our clients (library authors) and our clients' clients (the users of those libraries).
I agree. I think my main concern here is that with the parameterized approach we're more or less subverting the trait
mechanism to work in a certain fashion that it's not really geared toward. The partial loss of type inference is an indication of this. My experience with Haskell type classes leads me to believe this may end up being a bigger usability burden down the line (maybe in surprising ways) than the bookkeeping for wrappers but it's hard to be sure at this stage.
Regarding ergonomics using wrappers, I think what feels weird about it is that folks are more used to structs and to build data or objects but the intention here is really to transform the semantics of something by "hinting" the traits mechanism. In that sense, the wrappers ac a bit more like a function than something that builds data in the traditional sense. If we provide methods to do the wrapping/unwrapping it may feel more natural to the user, and then there's always macros.
But in any case, I'm certainly not opposed to exploring the parameterized version further. For the wrapper version, I don't have a good answer yet for the memory stuff pointed out by @aepsil0n so that's probably reason enough to try out more stuff with it.
Here it is: https://gist.github.com/aepsil0n/5ab39051f0b09620f824
This is great, thanks for putting this together!
I need to study it a bit closer when I have a moment but I think I agree with your observations. I think (more like hope) there may still be a another representation that behaves better wrt type inference and avoids the problem with non-copy types the wrapper approach has but I'm not sure yet.
Just a quick link: there is an interesting discussion on reddit mostly concerned with operator overloading. This is tangentially relevant, particularly how people perceive the ergonomics of certain APIs.
Thanks! By-ref vs by-val is a tricky problem.
Just a quick remark: operator overloading semantics have changed a bit, so we should look into if and how this affects this issue. btw, has anybody thought about this (and maybe found a better solution than the parametric approach)?
Sorry to necro this discussion once again… I'm not seriously working on this any more, but this article: "Scrap your typeclasses" strongly reminded me of our issue here. Perhaps traits are not quite the right approach here altogether? Of course, Rust operators are backed by traits, which might make this trickier than it seems, but still I wonder, whether one could take a radically different approach here.
There is a lot of code duplication for all the structural traits because all of them exist twice for addition and multiplication. The problem is also that one can not implement a magma, quasigroup, etc for any other operator than
+
or*
. I would feel uncomfortable misusing these for, say, a wedge product. There are furthermore other built-in operators, for which it makes sense to implement these categories.First I thought it might not be possible to do this to the type system, but then I tried and came up with a solution that allows us to actually be generic over the kind of operator. I haven't thought this through to the very end, but it looks like it works so far.
Closed operators
First of all, let's find an abstraction over closed operators.
This trait provides a similar signature as the stdlib operators and it is generic over some type
Op
. Now what isOp
? The simplest way to connect this trait to the language operators (or any other trait that qualifies) is to introduce a zero-sized struct for each and implement a concrete instance of this trait.This can be done analogously for all relevant operators and works nicely thanks to multidispatch. It can also be extended to arbitrary functions that can be used as an operator, e.g. a cross-product or a wedge product for differentials, etc.
The type parameter of the
Closed
trait can not be inferred, which makes for a bit of an ugly signature using this generically:Note that one may define operators more generically in terms of right-hand side and result but I wanted to keep this example simple.
Algebraic abstractions
Now this abstraction provides some benefits. For once we only need one generic definition for a Magma now instead of two and it automatically extends to all closed operators.
Another nice feature is that we can do stuff with more operators at the same time. Enter the quasigroup, which has two separate notions of division.
Currently, we can not write the following code due to rust-lang/rust#18693, which is why the above workaround using the helper trait is necessary. However, it was indicated that the restrictions here should be lifted in the future.