Control.Algebra contrib library? addition of VectorSpace (and related) unlawful versions and theorems/lemmas

[Release-Candidate]

I'd like to add some verified interfaces (VectorSpace and related) and also unverified versions of the existing ones (Group, Ring, Field, ...) as unverified versions would also be usable with types like Double, GMP's fractional type, MPFR floats, ... without needing constructing e.g. reals from cauchy sequences (like for example. Coq does).

If I correctly understand, everything Control.Algebra (in contrib) is going to be put into a library. As this would break its usage anyway, I'd like to also rename some of the existing verified interfaces to get consistent naming of verified and unverified versions. As of now the verified versions of Semigroup and Monoid are called SemigroupV and MonoidV (for obvious reasons), but the verified Group, Ring, Field, ... don't have a suffix V. I'd like to add the V to the existing interfaces and add unverified versions of these.

My questions is how to proceed? Should I add everything to contrib now (with unverified versions suffixed an U) or wait until it is extracted to a library (by @nickdrozd?)?

Edit: sorry, this shouldn't be labeled 'Feature Request'.

[stefan-hoeck]

For your info, there is an external library not maintained by the Idris core team which tries to provide such verified "interfaces". Maybe this could be useful for you as well? Here's the link.

[Release-Candidate]

For your info, there is an external library not maintained by the Idris core team which tries to provide such verified "interfaces". Maybe this could be useful for you as well? Here's the link.

Thank you. Of course I could also add the verified versions to your library (too).
But I don't think that the unverified interfaces to algebraic structures belong to idris2-algebra.

What I'm interested in is a 'place' where I could add unverified interfaces like Group, Ring,Field, VectorSpace, ... to.

So I rephrase my questions:

• where should I put these unlawful interfaces? To Control.Algebra - either in contrib or a to-be-made library, in another existing library (I haven't found one) or should I make a separate library?

I'd rather contribute to some sort of 'central' library (or contrib) than create my own, to avoid unnecessary fragmentation. And I thought, that Control.Algebra would be the place where these belong.

[gallais]

The plan is for contrib to be slowly taken apart and disposed of.
So I don't think I will accept PRs adding content to it.

[Release-Candidate]

Thanks for your answer.
So I wait until there is an Algebra/Math/Whatever library in the idris-community repo.
Is there anything I could do to help @Sventimir (@nickdrozd or whoever) with the transition out of contrib?

Edit: sorry, I confused nickdrozd with Sventimir

[nickdrozd]

I don't have any plans to maintain any libraries. So if nobody else picks the algebra stuff and it gets removed from the main repo, it will get scattered to the wind. Which would be a shame, both because the code is pretty cool on its own and also because it's a great stress test for the compiler. For example, AFAIK #1630 is still an issue.

Incidentally, I am opposed to "unverified" interfaces. Currently the hierarchy mixes verified (real) and unverified (fake) interfaces, leading to unsolvable but completely avoidable problems like #72. I am not aware of any compelling technical reasons why it should be like this. (On the other hand, there are a variety of uncompelling social reasons.) It would be much simpler to make all the algebra interfaces verified and then just assert the laws to hold in cases where they can't be proved. See this post for more discussion.

[Release-Candidate]

I don't have any plans to maintain any libraries.

Sorry, I confused you with @Sventimir see this post

Although reading that again now, calling a package math and only including algebraic structures and theorems/lemmas/... is not what I did have in mind. I thought about a package including proofs but also generic algorithms and types that use the algebraic structures as constraints.

So if nobody else picks the algebra stuff and it gets removed from the main repo, it will get scattered to the wind. Which would be a shame, both because the code is pretty cool on its own and also because it's a great stress test for the compiler.

Exactly my thoughts. I'm willing to help or even maintain the package, if nobody else does.

Incidentally, I am opposed to "unverified" interfaces. Currently the hierarchy mixes verified (real) and unverified (fake) interfaces, leading to unsolvable but completely avoidable problems like #72. I am not aware of any compelling technical reasons why it should be like this. (On the other hand, there are a variety of uncompelling social reasons.) It would be much simpler to make all the algebra interfaces verified and then just assert the laws to hold in cases where they can't be proved. See this post for more discussion.

That's fine by me too. I've just thought that unverified interfaces are the 'expected' way to do it for algebraic structures that are meant to be used by 'the public' and to not just 'turn them off' when they can't be proved (which you can't do for almost all uses of Field).

[Release-Candidate]

Reading the linked threads I'm now beginning to realize what this is all about.

But ignoring the (IMHO unnecessary diamond hierarchy) for now:

Taking a closer look at contrib/Control/Algebra.idr there are some additional severe errors:

• Ring has Group as constraint, but that should be AbelianGroup: so + isn't commutative.
• Same for RingWithUnity as that 'inherits' the flaw.
• Field is defined as a RingWithUnity with inverse in (ty{0}, *) which should be a CommutativeRingWithUnity (which doesn't exist), and so Field isn't commutative for both + and *.

This renders everything Ring* and Field unusable for lawful usage which is quite ironic.

[nickdrozd]

@Release-Candidate Yes, the current system has some flaws! A while back I worked out the details of fixing it; see yet another post. It would be great to get all that working, but unfortunately the "unverified" interfaces are an insurmountable obstacle. Oh well!

But even if that issue were resolved, it turns out that it's very hard to work with fields anyway. This is because constant reference is made to the "nonzero elements", and that really complicates all the types. Maybe there is an ergonomic way to handle that, but I couldn't figure it out.

As far as the ring definition, I think under certain circumstances it's possible to prove the commutativity of addition assuming the existence of a multiplicative identity. Or maybe I have the details wrong here, but in any case it's often possible to define the hierarchy of structures in alternative ways. Part of the fun is minimizing the the axioms required to prove something and figuring out what exactly follows from what.

[stefan-hoeck]

I once again invite you to have a look at idris2-algebra (if you haven't already done so). Personally, I think we should not write laws about interfaces but about sets (types) and their operations (functions). For instance, to proof the Monoid laws, we need a type plus a binary function p that is associative and has a neutral element n. Whether Monoid is implemented for this triple, is irrelevant. So we have:

record LMonoid (a: Type) (p : a -> a -> a) (n : a) where
  constructor MkMonoid
  0 associative : Associative p
  0 leftNeutral : LeftNeutral n p
  0 rightNeutral : RightNeutral n p

This solves the diamond issue and decouples proofs from interfaces. Of course we could still proof the correctness of an interface implementation. For instance:

listMonoid : LMonoid (List a) (++) []
listMonoid = ...

We can also show that LMonoid a p n implies LSemigroup a p:

(.semi) : LMonoid a p n -> LSemigroup a p
m.semi = MkLSemigroup m.associative

This style is used throughout idris2-algebra, and I find it to be pretty convenient.

[Sventimir]

@Release-Candidate, I am not actively working on Idris at the moment and also I cannot dedicate any amount of time consistently to maintaining an external library. So if you want to, please go ahead and extract algebraic interfaces from contrib.

[Release-Candidate]

Sorry, this is going to be long. I hope it is (at least somewhat) comprehensible.

• First: let’s leave the proofs and laws aside for a while and talk about the the part that is actually of use for the ‚everyday‘ programmer (although somebody who uses Idris (2) maybe isn’t ;):

Interfaces for rings, fields and vector spaces. For practical and consistency reasons these have to be interfaces and be compatible with the existing interfaces - Num, Integral, Fractional, …

What are they for? Well, a ring is the structure of e.g. integer types, a Ring is an abstraction for all integer-like types - like the existing Integral, but it also includes the existing Fractional. Which means Ring is a specialization of Num.
Exactly the integers form a commutative ordering ring with 1 (unity), but let’s just define this as a ring, because we as mathematicians are lazy[^1].

So why Ring and not just use Num? Because Num does not include Neg and Abs and Ord, 0 and 1. And some other, to be defined ones like functions max and min.

Then Field, which for example the rational and real numbers ‚are‘. This is Idris’ Fractional with additional constraints, like Ring.

Real - real numbers like Double, which has the constraint Field with trigonometric functions, power and exponential functions and related (like square root and log), …

And finally a vector space over a Field (or Real or …) which includes vectors (of elements of a field), lists (of elements of a field), tuples (of elements of a field), but also ‚same shaped‘ trees (with values of a field) and the field itself (which is sometimes useful). Of course including functions like an inner product, …

These abstractions are mainly useful to integrate ‚external‘ types like the ones from GMP, MPFR for JS’ Decimal JS, in generic algorithms.
Generic algorithms include things like interpolation (which needs a vector space).

To be usable, these interfaces have to be implemented in a sufficiently ‚central‘ place to avoid fragmentation and every math library using its own, incompatible, interfaces.

• Big nitpick: why does Num not have the constraint Eq? Defining + and * is quite useless without being able to actually compare numbers. Actually Ord would be appropriate, as a commutative + is certainly enough to prove that for all a, b, a < b <=> exists c > 0, a = b + c is an ordering. As any type implementing Num is going to have a 0.

• A smaller nitpick: why is Abs an extra interface and not part of Neg?

• Now to the laws:

First of all, the big problem is proving that some type actually fulfills the laws of some algebraic structure. For an inductive type like the unary numbers, Nat this is quite simple. Same as proving some lemmas which follow from the laws of a algebraic structure.
For all primitive types T that is impossible, as the only have a finite number of elements, and there are always elements a and b for which the sum (or product) of a and b is not an element of this type (there exist a, b in T, so that a + b is not in T - what is INT_MAX + INT_MAX?).
So trying to prove that (Int64, +, *) is a ring does not fail because you are bad at proving, but because that’s impossible because Int64 only has a finite amount of elements.

@nickdrozd

@Release-Candidate Yes, the current system has some flaws!

The biggest one is the missing link to the interfaces Num, Integral and Fractional. The diamond pattern could be easily resolved.
Actually using a hierarchy for lawful algebraic structures is a problem anyway, algebraic structures should better be viewed as composition of certain laws under a name. And we are functional programmers that favor composition over inheritance anyway, don’t we :D

But even if that issue were resolved, it turns out that it's very hard to work with fields anyway. This is because constant reference is made to the "nonzero elements", and that really complicates all the types. Maybe there is an ergonomic way to handle that, but I couldn't figure it out.

I don’t know what you mean (proofing in Idris is generally not very ergonomic).
It should mainly help avoiding problem during certain proof steps.
Say 1/0 actually exists. So 0*(1/0) = 1 per definition of the inverse.
Lets just try something:

For all x: x = x*1 = x*0*(1/0) = (x*0)*(1/0) = 0*(1/0) = 1

Cool, now every x is 1 :)
And somewhere in your proofs you need 1/x to not be 1/0 to avoid such contradictions.

As far as the ring definition, I think under certain circumstances it's possible to prove the commutativity of addition assuming the existence of a multiplicative identity.

Your definition of Ring is an error, it should be interface AbelianGroup ty => Ring ty but is interface Group ty => Ring ty. What this defines is a Near Ring (German: ‚Fast Ring‘ - ‚almost a ring‘ :).
Also the definition of the interface Field does additionally forget about the law of the commutativity of the multiplication.

What you are thinking about is the proof that some ‚type‘ is commutative, for that you need to use the laws defined for your ‚type‘.

@stefan-hoeck

I once again invite you to have a look at idris2-algebra (if you haven't already done so). Personally, I think we should not write laws about interfaces but about sets (types) and their operations (functions).

Yes, it would be very beneficial to actually explicitly state the binary operation to use, as to be able to ‚say‘ that a field over A has two abelian groups, (A, +) and (A, *).
The most important thing for proofs and laws is their composability and reusability. So that you can reuse existing proofs without the need to rewrite just because of different interface.

[^1] Definitions are often used in a way that are the least ‚work‘, so if you need e.g. natural numbers including/excluding zero, instead of always having to say ‚natural numbers including/excluding zero‘ you just define the natural numbers to be natural numbers including/excluding zero.
And the same for rings, if you always (well, for the following 1/2 hour) need a ring that is commutative and has a 1, you define a ring to be that instead of always having to talk about a ‚commutative ring with 1‘.

[stefan-hoeck]

Actually Ord would be appropriate, as a commutative + is certainly enough to prove that for all a, b, a < b <=> exists c > 0, a = b + c is an ordering. As any type implementing Num is going to have a 0.

You do realize that the complex numbers form a field without a total order? In addition, you can implement Num (lawfully) for functions of type a -> Integer without ever being able to implement Eq for those. It makes perfect sense for Num to come without an Eq or Ord constraint.

* A smaller nitpick: why is `Abs` an extra interface and not part of `Neg`?

We can have negate (-3 + 2i) but what is abs (-3 + 2i)?

Edit: Actually, abs (-3 + 2i) is well-defined. Sorry about that.

[stefan-hoeck]

So trying to prove that (Int64, +, *) is a ring does not fail because you are bad at proving, but because that’s impossible because Int64 only has a finite amount of elements.

But (Int64, +, *) is a lawful ring, as are all the other integral types such as (Bits8, +,*) or (Int16, +, *) (otherwise please show us, which one of the ring laws does not hold). The reason why this can't be proven in Idris is because it is a primitive type. However, the laws can be assumed to hold by means of using believe_me.

Edit: Please note that the fixed precision integral types are implemented in such a way that in case of an over- or underflow, they automatically wrap around (using Euclidian division / modulo, as discussed in #1480). For example, for Bits8, 255 + 1 returns `0'. That's the ring of integers modulo 256.

[Release-Candidate]

Sorry for the late response, I had been occupied by other stuff for a while.

@Sventimir

@Release-Candidate, I am not actively working on Idris at the moment and also I cannot dedicate any amount of time consistently to maintaining an external library. So if you want to, please go ahead and extract algebraic interfaces from contrib.

Thanks, will do.

@stefan-hoeck

Actually Ord would be appropriate, as a commutative + is certainly enough to prove that for all a, b, a < b <=> exists c > 0, a = b + c is an ordering. As any type implementing Num is going to have a 0.

You do realize that the complex numbers form a field without a total order?

No, I totally ignored them, thanks for your correction.

In addition, you can implement Num (lawfully) for functions of type a -> Integer without ever being able to implement Eq for those. It makes perfect sense for Num to come without an Eq or Ord constraint.

Ignoring Ord because of my error with the complex numbers, so this is now just about Eq.
Of course you can, It just seems like a strange decision to me.

So trying to prove that (Int64, +, *) is a ring does not fail because you are bad at proving, but because that’s impossible because Int64 only has a finite amount of elements.

But (Int64, +, *) is a lawful ring, as are all the other integral types such as (Bits8, +,*) or (Int16, +, *)

But if you define the ring as being the ring modulo n, it is impossible to define a (total) ordering that is compatible with the addition of the ring (which means for example that for all elements a, b of the ring, there exists a c > 0, so that a < b <=> a + c = b holds), because the ‚wrapping around‘ breaks that. And exactly such an ordering, the ‚usual‘ one, is defined for all of the Int?s.
So either the ring must be defined as ‚the‘ integers and the Int?s as finite subsets of them which do not have closed + and * or the definition of the Int? and their Ord constraint leads to a contradiction when trying to prove the laws.
As you can’t practically prove the ring laws anyway (as you’ve said), I’d rather have easy provable and consistent total orderings for the Int?s.

[stefan-hoeck]

But if you define the ring as being the ring modulo n, it is impossible to define a (total) ordering that is compatible with the addition of the ring.

True, the rings modulo n do not have a total order. But still they are commutative rings, so we should be able to treat them as such. And there is a total order for the fixed precision integers which is useful to have on its own right, for instance when implementing well-founded recursion. Just because this does not make Bits8 an ordered ring, does not mean that (Bits8,+,*) is not a lawful commutative ring, or that (<=) is not a lawful total order.

About proving the ring laws: You can't prove them in Idris itself, but you can definitely proof them based on the representation of these integers as fixed precision sequences of bits and how the arithmetic operations are implemented. Thus, they do hold, so we might just as well tell Idris that they hold and use this knowledge to our advantage.