This series of blog posts is a chronicle of my working my way through Gareth and Mary Jones’ Elementary Number Theory and translating the ideas into the Haskell programming language. This is the first installment of the series, which I’m calling “Learning Number Theory and Haskell.”
(As a quick side note, I know many readers already know Haskell. I hope this will get interesting for you soon, but my stated goal is to write for beginners… so you may want to skim the first few entries, or treat this as an opportunity to comment on whether I’ve chosen the best way to present ideas for new Haskellers.)
The Jones text begins with a description of the “division algorithm.” (If you’re following along in the text, which I hope you are, I’m combining theorem 1.1 with corollary 1.2 here.) This is seemingly an odd name for a theorem, but here it is. For all integers a and b, where b is not 0, there is a unique q and r such that a = qb + r and 0 <= r < |b|. The text calls these numbers the quotient and remainder. I call them an excuse to go hunting through the Haskell standard library a bit.
There are a few candidates in the standard library for the divison of numbers into a quotient and remainder. Haskell has quot and rem functions, which look promising. It also has div and mod functions, though. Let’s play around a bit and see which (if any) do what we want.
Since I said I’d start from the beginning, here’s the beginning. There are two commands to run GHC: ghc and ghci. We will start out in GHCi, which allows you to type lines of Haskell code and have them evaluated immediately. In some social circles, this is known as an REPL, which stands for “Read-Eval-Print Loop”. It makes poking around a lot easier, since you don’t need to save, recompile, or write a main function before seeing results. Later on, we can use the ghc command to compile programs or libraries that can be run on their own.
$ ghci -fglasgow-exts
(I added an option there that I haven’t mentioned yet. That option enables some language extensions that I don’t intend to use. I added it because it causes GHCi to use a slightly different form of type signatures that I think are actually easier to understand than the default.)
Finally, it’s time to ask GHCi for basic information about those functions. Specifically, we will ask for their types. One of the major keys to Haskell is that if you know the type of something, you are three fourths of the way to understanding it.
Prelude> :t quot
quot :: forall a. (Integral a) => a -> a -> a
Prelude> :t rem
rem :: forall a. (Integral a) => a -> a -> a
Prelude> :t div
div :: forall a. (Integral a) => a -> a -> a
Prelude> :t mod
mod :: forall a. (Integral a) => a -> a -> a
First of all, Prelude> is the basic GHCi prompt. Anything after that on a line is something I typed. We’re more interested in the responses, which are all about the same. Those are type signatures, and types are fundamental to Haskell. I think it might be helpful, though, to work our way up from simpler types toward the more complicated types above.
Prelude> :t not
not :: Bool -> Bool
The response to the :t command uses the :: syntax, which provides type annotations in Haskell. You should read :: as “has type”, so that statement is: not has type Bool -> Bool. That, of course, raises the question of what Bool -> Bool means as a type. First, Bool is the Boolean data type, with values of True or False. Second, -> describes a function mapping from one type to another. The not function, then, takes either True or False as an argument, and returns either True or False as a result. Simple enough.
Prelude> :t length
length :: forall a. [a] -> Int
There are two extra elements here. The first, which we won’t be using yet, is that [Bool] denotes a list whose elements are type Bool. The important thing is that in Haskell, you can’t just have a list. You must have a list of Bool or a list of Integer, or some other type. The length function, though, wants to operate on all possible types of lists. Therefore, it uses polymorphism. The keyword forall introduces a generic name for a type. It’s basically a logic quantifier, which in other contexts is often written as an upside-down A. The type here says that for all possible types a, the length function can calculate an Int from a list of a.
I like the -fglasgow-exts command line argument to ghci because it makes this explicit. Without that argument, the type above would have just been written as [a] -> Int. This is a valid abbreviation for the type given above; if some name in a type signature begins with a lower-case letter, it is assumed to be a type variable, even if there is no explicit forall clause. On the other hand, types beginning with upper-case letters are specific type names, like Int or Bool.
Prelude> :t negate
negate :: forall a. (Num a) => a -> a
The new concept introduced here is that of type classes. There are many different types that all represent numbers in Haskell. It would be painful if things like negate (or +, for that matter) could only work on one of those many types. (As a side note, I suppose it’s not universally agreed that this would be painful, because ML does it that way.) On the other hand, it makes no sense for negate to operate on all possible types, either! How do you keep a programmer from negating a banana warehouse? (Hmm, I feel like there should be a punchline here.) The solution is type classes. A type class, which starts with an upper-case letter much like a type, defines a group of many types (called instances) for which some set of operations is possible. You can read the => operator as an if/then statement, so the statement is: negate has a type so that for all types a, if a belongs to the type class Num, then negate can take an argument of type a and return a result of type a. Whew, that’s a mouthful! It says what we want, though. Now back to the beginning.
Prelude> :t quot
quot :: forall a. (Integral a) => a -> a -> a
Prelude> :t rem
rem :: forall a. (Integral a) => a -> a -> a
Prelude> :t div
div :: forall a. (Integral a) => a -> a -> a
Prelude> :t mod
mod :: forall a. (Integral a) => a -> a -> a
The only new thing here is that these functions take two parameters of type a, and return a result of type a. The Integral type class is exactly what you’d expect: it describes types whose values are mathematical integers. The two interesting types in this type class are Integer, which is an arbitrary precision type (in other words, it never overflows), and Int, which stores at least 30-bit signed values, depending on the implementation.
We now know the types, so let’s see how these functions behave. In other words, let’s play! (Any function of two parameters can be used as an infix operator by enclosing it in back-ticks, which are probably above the tilde on your keyboard. That’s what I’m doing below.)
Prelude> 6 `div` 4
1
Prelude> 6 `mod` 4
2
Prelude> 6 `quot` 4
1
Prelude> 6 `rem` 4
2
So far, so good. It looks like both pairs of functions behave like the Jones text’s quotient and remainder. However, a single test case does not make a correct function! We could try a few more test cases. Let’s try 100 of them instead! A nice systematic way to try lots of test cases is with a nifty library called QuickCheck. This library will verify stuff with bunches of random test cases. It tells us whether a property is false, or likely to be true. The wording there is very deliberate. It will definitely not tell us that the statement is true. That would require a general proof! QuickCheck will just try some random inputs to look for counter-examples.
I get tired of typing long commands, so I’ve added the following line to my GHCi configuration file, ~/.ghci:
:def qc \\c -> return $ ":m + Test.QuickCheck.Property \\nTest.QuickCheck.quickCheck (" ++ c ++ ") \\n:m - Test.QuickCheck.Property"
To use QuickCheck, we need functions that take parameters (values for a and b) and evaluate to either True (success) or False (failure). That’s convenient, because the Jones text gives us two of them. Specifically, the theorem asks for: a = qb + r, and 0 <= r < |b|. We can define these as anonymous functions using the lambda syntax in Haskell. Here’s a simple example of lambda syntax:
Prelude> (\\ x -> x * x) 4
16
The anonymous function begins with a backslash (\) and a list of parameters. The arrow (->) introduces the body of the function. This example defines an anonymous function to calculate the square of a number, and then applies it to 4 to get 16. We’ll do the same thing for our test cases. We are given that b is not zero, and QuickCheck defines a handy operator ==> to express that. Let’s try this with quot and rem.
Prelude> :qc \\a b -> (b /= 0) ==> (a `quot` b) * b + (a `rem` b) == a
+++ OK, passed 100 tests.
Prelude> :qc \\a b -> (b /= 0) ==> (0 <= a `rem` b) && (a `rem` b < abs b)
*** Failed! Falsifiable (after 9 tests and 5 shrinks):
-5
-3
Oops! The first test case succeeded, but the second test case failed. Specifically, it failed with values of a = -5 and b = -3. QuickCheck generates random test cases, so you will probably see a different test case fail. Hopefully your test did fail, though! Clearly, then, the quot and rem functions don’t satisfy the requirements of the division algorithm, because the result of rem is out of range for this input! Looking closer at the test case, we find that using quot and rem gives q and r of 1 and -2, while we wanted 2 and 1.
Let’s try div and mod.
Prelude> :qc \\a b -> (b /= 0) ==> (a `div` b) * b + (a `mod` b) == a
+++ OK, passed 100 tests.
Prelude> :qc \\a b -> (b /= 0) ==> (0 <= a `mod` b) && (a `mod` b < abs b)
*** Failed! Falsifiable (after 7 tests and 3 shrinks):
1
-2
So neither of the Haskell standard library functions agree with the spec that we got from the text. Both pairs of functions satisfy the first equality from the text, a = qb + r, all the time. If you’re wondering how they differ, the answer is that when the signs of a and b are different, rem gives the remainder the same sign as a, while mod gives the remainder the same sign as b. Thus, quot and rem fail our purposes precisely when a is negative and r is non-zero, while div and mod fail precisely when b is negative and r is non-zero.
We now know that we have two different incorrect functions. What about a correct one? We’ll have to write it; but fortunately it’s given in the Jones text. We’re in GHCi, and I’d prefer not to write a lot of code at a command prompt, so use GHCi’s :edit command.
Prelude> :edit NumTheory.hs
That should open up a text editor. (If you prefer a different editor, then set your EDITOR environment variable.) Now enter the following code, save the file, and exit the editor.
module NumTheory where
import Data.Ratio
jonesQuot, jonesRem :: Integral a => a -> a -> a
a `jonesQuot` b | b < 0 = ceiling (a % b)
| b > 0 = floor (a % b)
a `jonesRem` b = a - b * (a `jonesQuot` b)
Here’s what’s going on. The module statement defines this as a module with the name NumTheory. The import statement lets us use the Rational type, and the % operator to build it. I chose the Rational type to avoid the rounding error that would occur with floating point numbers. Next, there’s a type signature. Haskell could infer the type signature, but there are two advantages to specifying it ourselves. First, the signature inferred by Haskell is too general and is confusing. Second, the explicit type signature makes it abundantly clear how to use the function without having to ask GHCi for help. Next, jonesQuot has two cases corresponding to the main theorem and the corollary in the Jones text. (The vertical bar can be read as “such that” or “for” and is called a guard clause.) In one case, a floor is needed, while the other case requires a ceiling (this is in the book, if you’re reading it.) The % operator constructs a Rational from two Integral numbers.
Use the GHCi :l command to load the module, and you have precisely the functions we went searching for. We have QuickCheck to help us be more certain.
Prelude> :l NumTheory
[1 of 1] Compiling NumTheory ( NumTheory.hs, interpreted )
Ok, modules loaded: NumTheory.
*NumTheory> :qc \\a b -> (b /= 0) ==> (a `jonesQuot` b) * b + (a `jonesRem` b) == a
+++ OK, passed 100 tests.
*NumTheory> :qc \\a b -> (b /= 0) ==> (0 <= a `jonesRem` b) && (a `jonesRem` b < abs b)
+++ OK, passed 100 tests.
Ah, the feeling of success! Of course, QuickCheck didn’t prove anything except that failure probably happens less than one out of a hundred inputs. Proofs of the theorem and simple algebra to establish that the algorithm is correct are in the Jones text, and you’re encouraged to read them. Just remember that there is no (okay, only a little) competition between testing and proof. Knuth’s famous quote comes to mind: “Beware of bugs in the above code; I have only proved it correct, not tried it.” Proofs don’t always catch boneheaded coding mistakes.
It’s worth a brief mention that, in this case, the interaction between testing and proof is particularly appealing. The text proves that there is one and only one function for which those two QuickCheck tests would always succeed. In other words, we actually have a proof that our test cases test everything of importance! That’s pretty cool; we have proven the completeness of the test suite. (The passing tests still don’t prove the correctness of the code, though. Why not?)
