Hacker News new | past | comments | ask | show | jobs | submit login
Rust implementations of abstract algebraic structures (gitlab.com)
139 points by alex_hirner 42 days ago | hide | past | web | favorite | 9 comments



In my opinion, the best way to learn about abstract algebraic structures is to sit down with a book and write some proofs. That’s the purpose of these structures, to provide a minimal language for describing the behavior of mathematical objects for the purpose of exposition or proof. For example, prove that given any element g of a finite group G that there exists a positive integer k such that g^k is the identity element.

“Implementing” (with big scare quotes) algebraic structures by essentially implementing what appear to be “interfaces” (or traits or type classes or ...) might give you a brief “aha!” about what an abstract algebraic structure is on the surface, but won’t give much insight or practical use beyond that. Critically, one of the many hugely lacking aspects in this approach to implementing these structures in a language like Rust (or Haskell or ...) is that one needs to prove that these interfaces satisfy the axiomatic laws of the structure.

I maintain a library that allows one to compute with groups of permutations. The entire library—thousands of lines of fiddly code—is dedicated to one and only one algebraic structure (the group) on one and only one kind of object (the permutation). Countless papers have been written about just this combination, and should give you some appreciation for the depth of this subject. Slapping on a “identity” and “mul” implementation to a “Permutation” object doesn’t do justice.


> “Implementing” (with big scare quotes) algebraic structures by essentially implementing what appear to be “interfaces” (or traits or type classes or ...) might give you a brief “aha!” about what an abstract algebraic structure is on the surface, but won’t give much insight or practical use beyond that.

I find something relatively simple like a monoid already tremendously useful for practical software engineering tasks like some aggregation.

> Critically, one of the many hugely lacking aspects in this approach to implementing these structures in a language like Rust (or Haskell or ...) is that one needs to prove that these interfaces satisfy the axiomatic laws of the structure.

Typically these libraries (alga for rust, spire for scala) come with laws that allow at least checking if the properties hold using property based testing. I find this very useful. See for example https://github.com/typelevel/spire/tree/master/laws/src/main...


I think one needs to be careful with this sort of argument. Do you completely understand an algebraic structure by writing a bare-bones implementation of it? Absolutely not. Do you completely understand an algebraic structure by proving a few exercises in a book, or all of the exercises in a book? Also absolutely not.

All either of these does is change the balance an infinitesimal amount between what you do know about the structure and the vast, staggering amount of things you don't know about the structure. Getting paralysed by that vast, staggering amount out there doesn't help anyone. Instead, take tiny nibbles and build confidence—and if your implementation in a programming language of an algebraic structure helps you to do the proofs, or even just helps you realise when the structure might be appropriate in a programming task, then real progress has been made, no matter how much you still don't know.


As you say, the big problem is you can’t express rules. I don’t think that rules out using code to understand these things, but you’re better off starting with something like LEAN.


It’s one of the issues. The other is that you quickly will want to work with these algebraic structures as objects themselves. When the algebraic structure is encoded as a protocol, you won’t be able to manipulate them as first-class values. For instance, you’ll want this if you want to do things like factorizing groups, constructing products (like the semi direct product), computing graded algebras, computing homomorphisms, constructing Groebner bases, etc.


Yeah, you need dependent typing to do that in a programming language. But as cool as dependently typed languages are, developing serious software in them remains a bit of a research problem. Idris is closest, but it also less convenient for actual proofs.


> In my opinion, the best way to learn about abstract algebraic structures is to sit down with a book (...)

For starters, what book would you recommend? Cheers!


I quite like Pinter’s “A Book of Abstract Algebra”. He writes very cleanly, is aimed at beginners, but doesn’t cut corners.

If you’re already pretty serious about math (i.e., you already write proofs; maybe you took an analysis class), then I recommend Artin’s Algebra.

If you really want tons of practice and a Stewart’s Calculus-like book, then Dummit and Foote.


Looks very nice and straightforward. Otherwise, seems similar to alga: https://docs.rs/alga/0.9.2/alga/




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: