Haskell: как написать экземпляр `Monoid` для чего-то, что зависит от параметров

Продолжая мой комментарий, вот первая трещина. Модуль определяется типом, но не каноническим выбором представителя: это делается просто вычислением, поэтому потребуется барьер абстракции. Также доступны типы ограниченных чисел, но они требуют немного больше работы.

Войдите, {-# LANGUAGE KitchenSink #-}. Я имею в виду (на самом деле не так уж и плохо)

{-# LANGUAGE DataKinds, GADTs, KindSignatures, FlexibleInstances #-}

и давайте приступим.

Во-первых, просто рефлекторно, я ввожу хасохистские натуральные числа:

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

На мой взгляд, это именно то, что вы делаете, когда хотите объявить тип данных, а затем разрешить другим типам зависеть от его значений. Библиотека синглтонов Ричарда Айзенберга автоматизирует конструкцию.

(Если в этом примере используются числа для индексации векторов, некоторые люди указывают, что векторы () также могут служить одиночными числами для Nat. Они, конечно, технически правильны, но ошибочны. Когда мы думаем о Natty и NATTY как о систематических сгенерированные из Nat, это право, которое мы можем использовать или не использовать по своему усмотрению, а не лишнее, которое нужно оправдать. В этом примере не используются векторы, и было бы неправильно вводить векторы только для того, чтобы иметь синглтоны для Nat.)

Я вручную набираю кучу функций преобразования и Show экземпляров, чтобы мы могли видеть, что мы делаем, помимо всего остального.

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

Теперь мы готовы объявить Mod.

data Mod :: Nat -> * where
  (:%) :: Integer -> Natty n -> Mod (S n)

Тип несет модуль. Значения несут ненормализованный представитель класса эквивалентности, но нам лучше понять, как его нормализовать. Дивизия унарных чисел - особый вид спорта, которому я научился в детстве.

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)

Теперь мы можем сделать умный конструктор.

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

И тогда экземпляр Monoid просто:

instance NATTY n => Monoid (Mod (S n)) where
  mempty                    = rep 0
  mappend (x :% _) (y :% _) = rep (x + y)

Я добавил еще кое-что:

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

С небольшим удобством ...

type Four = S (S (S (S Z)))

мы получили

> foldMap rep [1..5] :: Mod Four
(3 :% 4)

Так что да, вам нужны зависимые типы, но Haskell достаточно зависимо типизирован.

Это тот же ответ, что и @pigworker, но написанный менее болезненным (более эффективным и приятным синтаксисом) способом.

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

И мы получаем

> foldMap fromInteger [1..5] :: Mod 4
3 :% 4
> toInteger (88 * 23 :: Mod 17)
1
> (3 :: Mod 4) == 7
True

Этот модуль также иллюстрирует мысль, которую я сделал в комментарии к вашему вопросу об уравнении. Вне модуля Mod вы не можете обмануть и использовать представление.

В дополнение к предыдущим ответам вас может заинтересовать модульная арифметика, который реализует это как библиотеку с очень красивым синтаксисом.

>>> import Data.Modular
>>> 10 * 11 :: ℤ/7
5