On of my favorite perks of statically typed languagues is making
invalid states unrepresentable. So instead of throwing exceptions at
runtime, try to use types in such a way that you cannot even get invalid
states to even compile.

In a sense this is the big difference between dynamic and statically
typed languagues and for me stronger just means can express even more
of these constraints.

Today I want to talk a bit about the integers modulo
n
$$\mathbf{Z}/n\mathbf{Z}$$.

I want to make the modulo n part into a type in such a way that it’s
impossible to add an number in \( \mathbf{Z}/n\mathbf{Z} \) to one in
\(\mathbf{Z}/m\mathbf{Z} \) if \(m \neq n \).

So let’s do it using type-level natural numbers:

representing natural numbers as types

I want to declare type-synnonyms as instances of the Nat type-class
you will see in just a second. For this we need an GHC exctension: FlexibleInstances.
In addition I needScopedTypeVariables` later on.

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Nat where

And we will need this later to make our data-type an instance of
Fractional:

import Data.Ratio (numerator, denominator)

Now we can start with the fun. Every number will have a different type
(based on the ideas of Peano of course) but to constrain our functions
and types we need common type-class (the instances of which will be just
our peano-integers).

As it’s convenient at this point I will include overloaded functions to
get me back the Int represented by the type and a default value
for a Nat – this makes sense beause our types will be singletons
anyway.
This (together with ScopedTypeVariables) will enable some nice tricks.

class  Nat n where
  value :: n -> Int
  def   :: n

Of course the types themselves will just be the Peano
axioms encoded
as simple singleton types:

data Z   = Zero
data S a = Succ a

with the obvious instances:

instance Nat Z where
  value Zero = 0
  def        = Zero

instance Nat n => Nat (S n) where
  value (Succ n) = 1 + value n
  def            = Succ def

representing the integers modulo n

To make the operations only possible on numbers of the same modulo we
parameterize the data-type by out an generic parameter (which of course
will be our Nats):

data ModN n = ModN Int

Of course for us the value of n as an integer will be important and
this is where the overloaded functions from Nat become important. For
example show can be defined like this:

instance Nat n => Show (ModN n) where
  show (ModN x) = 
     show x ++ " (mod " ++ show (value $ (def :: n)) ++ ")"

Here you can see how I used ScopedTypeVariables to get the value represented by the n in ModN n –
this is the trick I mentioned above. You will see it quite often here.

We are mostly interesed in the standard-representatives
\(0+n\mathbf{Z}..1+n\mathbf{Z}\) so we define a smart-constructor that
will constraint the wrapped value to this range:

modN :: forall n . Nat n => Int -> ModN n
modN x = ModN (x `mod` value (def :: n))

Using this it’s easy to make ModN n an instance of Num when we
constraint n to Nat:

instance Nat n => Num (ModN n) where
  (ModN a) + (ModN b) = modN (a+b)
  (ModN a) * (ModN b) = modN (a*b)
  abs        (ModN a) = modN $ abs a
  signum     (ModN a) = modN $ signum a
  fromInteger      a  = modN $ fromInteger a
  negate     (ModN a) = modN $ value (def :: n) - a

This is exactly how you would define these operation in math – just use
integer-operations and take the results (modulo n).
All nicely wrapped into types 😉

Now we can already calculate in a type-safe way. For
example 3 * (2 + 2) :: ModN Five will give
you 2 (mod 5) (note: I used the type-synonym Five defined bellow).

But (2 :: ModN Five) + (2 :: ModN Four) of course will not typecheck.

more fun: talking about fields

To show case this a bit more let’s look at the integers modulo n where
\(n\) is a prime number. In this case \(\mathbf{Z}/n\mathbf{Z}\) is a field
and so we can have a division: (/).

To constraint our peano-number-types even more I’ll introduce another type-class:

class Nat n => Prim n

I will not even try to find some dependent-type magic to let the
compiler figure out when a Nat is Prim (indeed a quick google did
not find anything – so I guess the problem is rather non-trivial ;).

Anway I’ll just cheat here:

instance Prim Two
instance Prim Three
instance Prim Five

Now it’s easy to make ModN p and instance of Fractional for Prim p
if we know how to get an inverse for a number \(m + n\mathbf{Z}\) (and by
using the helper functions imported above):

instance Prim p => Fractional (ModN p) where
  recip x        = inverse x
  fromRational r = recip (modN . fromInteger $ denominator r)
                   * (modN . fromInteger $ numerator r)

To get the inverse we just use the extended euclidean
algorithm:

inverse :: forall p . (Prim p) => ModN p -> ModN p
inverse (ModN a) = modN inv
  where inv = if a' < 0 then n' + a' else a'
        (_,a',_) = extEuklid a n'
        n' = value (def :: p)

which can be defined by

extEuklid :: Int -> Int -> (Int, Int, Int)
extEuklid a 0 = (a, 1, 0)
extEuklid a b =
  let (d', s', t') = extEuklid b (a `mod` b)
  in (d', t', s' - t' * (a `div` b))

(see the wiki
article on
the subject).

Now you can do fun stuff like

λ> (2 + 3) / 4 + 3 :: ModN Five
3 (mod 5)
λ> 3 / 4 :: ModN Five
2 (mod 5)
λ> 2 * 4 :: ModN Five
3 (mod 5)

But the compiler will prevent you from using division in the wrong ring:

λ> 2 / 3 :: ModN Four

<interactive>:162:3:
    No instance for (Prim (S Three)) arising from a use of `/'
    In the expression: 2 / 3 :: ModN Four
    In an equation for `it': it = 2 / 3 :: ModN Four

Finally I have to give you the missing helper-types used for the examples:

type One = S Z
type Two = S One
type Three = S Two
type Four = S Three
type Five = S Four
type Six = S Five