having fun with type-level naturals

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.

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