How to abstract from data type parameters in class instances?

Question

As a toy project, I would like to understand how to model mathematical groups in Haskell in general.

To start us off, we begin by observing that a to be defined Group is just a Monoid with inversion.

class (Monoid m) => Group m where
    minvert :: m -> m

Next, we first restrict ourselves to cyclic groups and start by defining the cyclic group of order 12.

data Cyclic12 = Cyclic12 Int deriving (Show, Eq)

Finally, we instantiate both classes for Cyclic12.

instance Monoid Cyclic12 where
    mempty = Cyclic12 0
    mappend (Cyclic12 x) (Cyclic12 y) = Cyclic12 ((x + y) `mod` 12)

instance Group Cyclic12 where
    minvert (Cyclic12 x) = Cyclic12 ((0 - x) `mod` 12)

How do I abstract the previous definition from the specific value of 12 to allow a more generic definition of different cyclic groups?

Ideally, I would like to write definitions like

instance Monoid (Cyclic k) where
    mempty = Cyclic k 0
    mappend (Cyclic k x) (Cyclic k y) = Cyclic k ((x + y) `mod` k)

instance Group (Cyclic k) where
    minvert (Cyclic k x) = Cyclic k ((0 - x) `mod` k)

But with a data definition like

data Cyclic = Cyclic Int Int deriving (Show, Eq)

we still don't get very far, because k is "not in scope". Regarding its apparent triviality I have a feeling to be missing out on some fundamental concept here. Thanks in advance for your help.

Answer 1

You must make the order of the cyclic group part of the type. One way of doing this is to use the builtin type level natural numbers GHC gives us.

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}

import GHC.TypeLits
import Data.Proxy (Proxy(..))

data Cyclic (n :: Nat) = Cyclic Integer deriving (Show, Eq)

Which lets us make the two instances pretty easily:

instance KnownNat n => Monoid (Cyclic n) where
    mempty = Cyclic 0
    Cyclic x `mappend` Cyclic y = Cyclic $ (x + y) `mod` natVal (Proxy :: Proxy n)

instance KnownNat n => Group (Cyclic n) where
    minvert (Cyclic x) = Cyclic $ negate x `mod` natVal (Proxy :: Proxy n)

The KnownNat part of the signature basically says that whatever n :: Nat ends up being, it is something whose value we should be able to extract using natVal.

Then, once loaded in GHCi:

ghci> :set -XDataKinds
ghci> type Z12 = Cyclic 12
ghci> mappend (Cyclic 8 :: Z12) (Cyclic 7 :: Z12)
Cyclic 3
ghci> minvert (Cyclic 4 :: Z12)
Cyclic 8

Aside on extensions

• DataKinds lets us have a type parameter n which isn't a type. We say that its kind is not type (*). In this case, n has kind Nat (n :: Nat).
• KindSignatures just lets us write n :: Nat where :: means "has kind" (instead of "has type") when it makes sense.
• ScopedTypeVariables makes it so that the n type variable in Proxy :: Proxy n is the same one as in the instance head instance KnownNat m => Monoid (Cyclic n) where.