search

brendanzab / algebra

Abstract algebra for Rust (still very much a WIP!)
Apache License 2.0
60 stars 9 forks source link

Migrate to Cargo. #4

Closed omasanori closed 10 years ago

omasanori commented 10 years ago

I'm unsure whether this project is still alive or not, but I did it just for fun.

brendanzab commented 10 years ago

Heh cheers! Yes it is pretty dead. I can transfer it to you if you like?

omasanori commented 10 years ago

Well, for now, I have no future plan to improve the library and even I haven't understood the core concept of it deeply yet. I'm interested in a solid mathematical construction on top of the Rust standard library, though.

brendanzab commented 10 years ago

Yeah take a look and see what you think. I too am interested in a more formal foundation for mathematics, but I have basically abandoned this approach because it doesn't actually reflect the semantics of Rust's core types: ie. floats are not reals, ints are not modulo arithmetics etc... A proper formalization would stay true to the actual semantics of the machine types. I'm not sure if this is possible in Rust's type system though. @cartazio knows more about this topic than me though.

cartazio commented 10 years ago

point of order: you can totally give many of operations for floats/ints/uints the algebraic semantics, just not quite the ones you'd expect

a starting reference point might be to do the following:

have two (three?) classes of operations (which will otherwise look the same) a) the instances which are legal/valid for a given type, and obey the laws on the whole domain b) the sound but unsafe siblings, which throw an error / die on inputs that break the algebraic invariants c) unsound but assassin instances, whereby they makeup some behavior on the corner cases. and on your head when it happens.

on the floating point front, the right "reference point" for thinking about how to build a truthful api would be to considered what an API for computable reals looks like, and then consider what an api for "approximate computable reals" looks like. (though theres the question of models that fold nan in as a legal value, or doing Maybe Real as the sort of result type.) . One important take away is that computable functions on (approximate) computable reals aren't allowed to test for equality! They can only ask "how close are two numbers, up to some specified tolerance epsilon". That is, you can't do dist(a,b), you can only do dist(a,b,epsilon).

now whats this mean when you compare things? instead having >,==,< as the choices, you get >, near(epsilon), and <

the point is theres a perfectly natural explicit precision abstraction that has algebraic laws that hold for for floats, its just that the the equations are not using == but rather near(epsilon)

exact computable real computation is a rabbit hole if you're not careful, but my point is that at subject to being explicitly approximate about the laws, you get the "right" algebraic laws for floats.

cartazio commented 10 years ago

unsigned ints do form a ring thing, unlike signed ints though!

omasanori commented 10 years ago

Hmm...

a) the instances which are legal/valid for a given type, and obey the laws on the whole domain b) the sound but unsafe siblings, which throw an error / die on inputs that break the algebraic invariants c) unsound but assassin instances, whereby they makeup some behavior on the corner cases. and on your head when it happens.

So, for example, is (uint, +) in "b" category? Or, in "a" category using something like addition with wrapping op?

cartazio commented 10 years ago

hrmm, i'll have to think about that. I think UInt === a, its Int thats trickier. like negate minInt < 0 for standard signed ints.

relatedly, you can treat floating point as being lawful if you allow some notion of "approximate algebraic laws", like (a_b)_c * (1± epsilon)= (1±epsilon) * a * (b*c) etc