effectfully / tiny-lang

BSD 3-Clause "New" or "Revised" License
6 stars 2 forks source link

Get fields to advertise their characteristic #36

Open kwxm opened 5 years ago

kwxm commented 5 years ago

We should probably add a method to the Field typeclass to return the characteristic of a field. Among other things, this would let us add a test to make sure that the characteristic is actually prime (or zero). With Data.Field.Galois you can define a supposed field of characteristic 1000 by writing Prime 1000 for example, and you don't get any complaints (not surprisingly: you'd presumably need compile-time primality checking at the type level for that). Things will go wrong when you try to do calculations in this "field" though. If you're cutting and pasting numbers with dozens of digits then there's a danger that you might miss a digit or two, so we should add a test for this. Note that Data.Field.Galois already includes a char function which returns the characteristic.

We'd also need primality testing functions for large numbers, but implementations of these already exist: see for example http://hackage.haskell.org/package/arithmoi-0.9.0.0/docs/Math-NumberTheory-Primes-Testing.html

See https://wiki.haskell.org/Prime_numbers for lots of information about primality testing.

kwxm commented 5 years ago

Note that the property tests for the field axioms aren't good enough to check this. If you take a large prime p and look at Z_(p^2) then it will automatically satisfy the ring axioms and the only possible problem is with invertibility of non-zero elements. However, in this ring everything is invertible except multiples of p, and if p is enormous then you're very unlikely to randomly select a multiple of p. Similar things are true in any ring Z_m where all of the prime factors of m are large.