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.`

ScopedTypeVariables` later on.

In addition I need

{-# 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 `Nat`

s):

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