I am working on a small library for the university that does integer calculations in a cyclic group; Things like:
(3 (% 11)) + (10 (% 11))
--> (2 (% 11))
'Integers (% n)' clearly form a monoid under addition with '0 (% n)' as identity element. However, addition only makes sense when the modulo of the two operands being added is the same: a (% n) + b (% n)
makes sense, while a (% n) + b (% m)
does not.
Is there any way to enforce this with Haskell's type system? The same of course holds true for the mempty
identity element: How can 0 (% n)
be constructed? Can n
be kept somehow in the type system?
Or do structures like these require the usage of dependent types?
As we can see, Monoid in Haskell is a typeclass that has three methods: mempty , mappend , and mconcat . mempty is a value that doesn't impact the result when used together with the binary operation. In other words, it's the identity element of the monoid. mappend (or <> ) is a function that puts two monoids together.
mappend is the concatenation operator which means the Neutral Element, mempty can only be the empty list, [] . It's important to realize that mconcat takes a List of elements from the set which here are Lists. Therefore, it takes a List of Lists, hence the parameter name xss .
In Haskell, the Monoid typeclass (not to be confused with Monad) is a class for types which have a single most natural operation for combining values, together with a value which doesn't do anything when you combine it with others (this is called the identity element).
From HaskellWiki. The Semigroup represents a set with an associative binary operation. This makes a semigroup a superset of monoids. Semigoups have no other restrictions, and are a very general typeclass.
Expanding on my comment, here's a first crack. The modulus is enforced by type, but not the canonical choice of representative: that's just done by computation, so would necessitate an abstraction barrier. Types of bounded numbers are also available, but they take a bit more work.
Enter, {-# LANGUAGE KitchenSink #-}
. I mean (actually the not too bad)
{-# LANGUAGE DataKinds, GADTs, KindSignatures, FlexibleInstances #-}
and let's get cracking.
Firstly, just by reflex, I introduce the Hasochistic natural numbers:
data Nat = Z | S Nat -- type-level numbers
data Natty :: Nat -> * where -- value-level representation of Nat
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
class NATTY n where -- value-level representability
natty :: Natty n
instance NATTY Z where
natty = Zy
instance NATTY n => NATTY (S n) where
natty = Sy natty
To my mind, that's just what you do when you want to declare a datatype and then allow other types to depend on its values. Richard Eisenberg's "singletons" library automates the construction.
(If the example goes on to use numbers to index vectors, some people point out that vectors of ()
can also serve as singletons for Nat
. They're technically correct, of course, but misguided. When we think of Natty
and NATTY
as systematically generated from Nat
, they're an entitlement we can exploit or not as we see fit, not an extra to justify. This example does not involve vectors, and it would be perverse to introduce vectors just to have singletons for Nat
.)
I hand-roll a bunch of conversion functions and Show
instances, so we can see what we're doing, apart from anything else.
int :: Nat -> Integer
int Z = 0
int (S n) = 1 + int n
instance Show Nat where
show = show . int
nat :: Natty n -> Nat
nat Zy = Z
nat (Sy n) = S (nat n)
instance Show (Natty n) where
show = show . nat
Now we're ready to declare Mod
.
data Mod :: Nat -> * where
(:%) :: Integer -> Natty n -> Mod (S n)
The type carries the modulus. The values carry an unnormalized representative of the equivalence class, but we had better figure out how to normalize it. Division for unary numbers is a peculiar sport which I learned as a child.
remainder :: Natty n -- predecessor of modulus
-> Integer -- any representative
-> Integer -- canonical representative
-- if candidate negative, add the modulus
remainder n x | x < 0 = remainder n (int (nat (Sy n)) + x)
-- otherwise get dividing
remainder n x = go (Sy n) x x where
go :: Natty m -- divisor countdown (initially the modulus)
-> Integer -- our current guess at the representative
-> Integer -- dividend countdown
-> Integer -- the canonical representative
-- when we run out of dividend the guessed representative is canonical
go _ c 0 = c
-- when we run out of divisor but not dividend,
-- the current dividend countdown is a better guess at the rep,
-- but perhaps still too big, so start again, counting down
-- from the modulus (conveniently still in scope)
go Zy _ y = go (Sy n) y y
-- otherwise, decrement both countdowns
go (Sy m) c y = go m c (y - 1)
Now we can make a smart constructor.
rep :: NATTY n -- we pluck the modulus rep from thin air
=> Integer -> Mod (S n) -- when we see the modulus we want
rep x = remainder n x :% n where n = natty
And then the Monoid
instance is easy:
instance NATTY n => Monoid (Mod (S n)) where
mempty = rep 0
mappend (x :% _) (y :% _) = rep (x + y)
I chucked in some other things, too:
instance Show (Mod n) where
show (x :% n) = concat ["(", show (remainder n x), " :% ", show (Sy n), ")"]
instance Eq (Mod n) where
(x :% n) == (y :% _) = remainder n x == remainder n y
With a little convenience...
type Four = S (S (S (S Z)))
we get
> foldMap rep [1..5] :: Mod Four
(3 :% 4)
So yes, you do need dependent types, but Haskell is dependently typed enough.
This is the same answer as given by @pigworker, but written in a less painful (more efficient, nicer syntax) way.
{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}
module Mod(Mod) where
import Data.Proxy
import GHC.TypeLits
data Mod (n :: Nat) = Mod Integer
instance (KnownNat n) => Show (Mod n) where
showsPrec p (Mod i) = showParen (p > 0) $
showsPrec 0 i . showString " :% " . showsPrec 0 (natVal (Proxy :: Proxy n))
instance Eq (Mod n) where
Mod x == Mod y = x == y
instance forall n . (KnownNat n) => Num (Mod n) where
Mod x + Mod y = Mod $ (x + y) `mod` natVal (Proxy :: Proxy n)
Mod x - Mod y = Mod $ (x - y) `mod` natVal (Proxy :: Proxy n)
Mod x * Mod y = Mod $ (x * y) `mod` natVal (Proxy :: Proxy n)
fromInteger i = Mod $ i `mod` natVal (Proxy :: Proxy n)
abs x = x
signum x = if x == 0 then 0 else 1
instance (KnownNat n) => Monoid (Mod n) where
mempty = 0
mappend = (+)
instance Ord (Mod n) where
Mod x `compare` Mod y = x `compare` y
instance (KnownNat n) => Real (Mod n) where
toRational (Mod n) = toRational n
instance (KnownNat n) => Enum (Mod n) where
fromEnum = fromIntegral
toEnum = fromIntegral
instance (KnownNat n) => Integral (Mod n) where
quotRem (Mod x) (Mod y) = (Mod q, Mod r) where (q, r) = quotRem x y
toInteger (Mod i) = i
And we get
> foldMap fromInteger [1..5] :: Mod 4
3 :% 4
> toInteger (88 * 23 :: Mod 17)
1
> (3 :: Mod 4) == 7
True
This module also illustrates the point I made in a comment in your question about Eq. Outside the Mod module you can't cheat and use the representation.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With