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