In this post I will speak about how one can implement ( or the integers modulo n) using fake dependent types in Haskell. What I want to do is to represent the modulus that characterizes the ring we are working over at the type level. To do this I use the type-level library which contains an implementation of tons of type level numbers and operations on them. The type of can be represented using a phantom type which denote the modulus:

newtype Zn n = Zn Integer deriving (Eq,Ord)

It is easy to implement a Show instance:

instance Pos n => Show (Zn n) where show (Zn n) = show n

Here Pos denote positive natural numbers. The Num instance is a bit more interesting:

instance Pos n => Num (Zn n) where Zn x + Zn y = Zn $ (x+y) `mod` toNum (undefined :: n) Zn x * Zn y = Zn $ (x*y) `mod` toNum (undefined :: n) negate (Zn x) = Zn $ negate x `mod` toNum (undefined :: n) fromInteger x = Zn $ fromInteger $ x `mod` toNum (undefined :: n)

I have left abs and signum out since I don’t know what they mean in this setting (does anyone have an idea?). Anyway, toNum is a function that only depend on its type. What I mean is that toNum for D3 (digit 3) always return 3 regardless of input, so all computations are done modulo the number encoded in the type. fromInteger is quite interesting also, it is the canonical homomorphism or natural map which takes an element and send it to its congruence class modulo n.

In fact this fit very well in the algebraic hierarchy that I discussed in my previous post.

instance Pos n => Ring (Zn n) where (<+>) = (+) (<*>) = (*) zero = Zn 0 one = Zn 1 neg = negate instance Pos n => CommutativeRing (Zn n) where

We can now check that we haven’t done anything stupid so far.

type Z6 = Zn D6 test = quickCheck (propCommutativeRing :: Z6 -> Z6 -> Z6 -> Property) *Algebra.Zn> test +++ OK, passed 100 tests. *Algebra.Zn> 2 + 2 * 4 :: Z6 4

So is a commutative ring and the basic operations seem to be working fine. But what about making it an instance of integral domain? This should not be possible since 2*3=0 in and thus it has zero divisors. In fact is an integral domain only if n is prime, but how do we test this on the type level? There is no type level primality test in the library, so I decided to hack one up myself. The only problem was that I don’t really know functional dependencies that well, but I looked at the code in the library and read some tutorials and this is what I came up with:

class (Pos x, Pos sqrt) => Sqrt x sqrt | x -> sqrt instance (Pos x, Pos sqrt, Sqrt' x D1 GT sqrt) => Sqrt x sqrt class Sqrt' x y r sqrt | x y r -> sqrt instance Sub y D2 y' => Sqrt' x y LT y' instance Pred y y' => Sqrt' x y EQ y' instance (ExpBase y D2 square, Succ y y', Trich x square r, Sqrt' x y' r sqrt) => Sqrt' x y GT sqrt sqrt :: Sqrt x sqrt => x -> sqrt sqrt = undefined class (Pos x, Data.TypeLevel.Bool b) => Prime x b | x -> b instance (Sqrt x y, Trich y D1 r, Prime' x y r b) => Prime x b class Data.TypeLevel.Bool b => Prime' x y r b | x y r -> b instance Prime' x D1 EQ True instance (Pred y z, Trich z D1 r1, Mod x y rest, IsZero rest b1, Not b1 b', Prime' x z r1 b2, And b' b2 b3) => Prime' x y GT b3 prime :: Prime x b => x -> b prime = undefined

It looks like a lot of mumbo jumbo and maybe it is, but it seems to work. The main problem though is that it is horribly slow and that it believes that 1 is a prime number… If anyone know fundeps (or type families) and sees how this can be improved, please let me know. Anyway, now I can implement the integral domain instance for .

instance (Prime n True, Pos n) => IntegralDomain (Zn n) where

So if n is a prime number then is an integral domain. Using this we can try to make ghc believe that an integral domain:

*Algebra.Zn> quickCheck (propIntegralDomain :: Z6 -> Z6 -> Z6 -> Property) Top level: Couldn't match expected type `True' against inferred type `False' ...

Woho, ghc can correct us automagically! What about giving a field instance? To do it we need to be able to compute the inverse of any nonzero element. Here Fermat’s little theorem comes in handy, it says that for any prime p and natural number x coprime to p (which in our case is any element of ) we have that . So by computing we find an element y such that xy = 1 in .

instance (Prime n True, Pos n) => Field (Zn n) where inv (Zn x) | x == 1 = Zn 1 | p `mod` x == 0 = error "Can't invert zero!" | otherwise = Zn $ x <^> (p-2) `mod` p where p = toNum (undefined :: n)

Now we can try this out on a prime number, for instance 17.

type Z17 = Zn D17 *Algebra.Zn> inv 13 :: Z17 4 *Algebra.Zn> 13 * 4 :: Z17 1 *Algebra.Zn> quickCheck (propField :: Z17 -> Z17 -> Z17 -> Property) +++ OK, passed 100 tests.

Everything seem to be working fine, but sadly it is not useful for something “real” since the typechecking is so slow for primality testing. But I think it is quite cool that you can do these things in Haskell, but of course it would be even nicer to do it in a language with real dependent types.

Very interesting posts! Looking forward to more.