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 )
*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?)

1. Eelis / Jun 2 2007 6:04 pm

I find the “there is no (okay, only a little) competition between testing and proof” sentiment rather unfounded. While it may apply when one’s program and proof are completely separate as they are in your case with the non-Haskell proof in the book separate from your Haskell program, it simply does not apply when the two are unified in a system such as Coq ( http://coq.inria.fr/ ) which lets you write functional programs along with formal machine-checked proofs of properties of those programs.

For this reason, systems such as Coq are far more suitable for building what you called “a software library that, in a sense, embodies the theory of a mathematical field” in your previous post, as they raise the status of programs from that of mere implementations that try to capture some property, to that of proper mathematical objects (defined on top of rigid logical foundations) that can be formally proven to possess the desired property. I encourage you to browse the Coq standard library; you may just find that it’s the kind of thing you were looking for :).

2. hs / Jan 27 2010 1:02 am

Why are you writing \\ instead of \? \ is the lambda symbol in haskell, \\ is just a char…

3. Sindikat Lolwut / Jun 24 2014 12:21 pm

As of June 2014, you can just type `import Test.QuickCheck` and use it like `quickCheck \$ \a b -> (b /= 0) ==> let q = a `quot` b; r = a `rem` b in q*b + r == a` in GHCi, instead of adding stuff in `~/.ghci`.