Haskell: Jak napisać instancję `Monoid` dla czegoś, co zależy od parametrów

Question

Pracuję nad małą biblioteką dla uniwersytetu, która wykonuje obliczenia całkowite w cyclic group; Rzeczy, takie jak:

(3 (% 11)) + (10 (% 11)) 
--> (2 (% 11)) 

'liczb całkowitych (% N)' wyraźnie tworzą monoid z dodatkiem z '0 (% N)' jako element neutralny. Jednak dodanie ma sens tylko wtedy, gdy modulo dwóch dodawanych operandów jest takie samo: a (% n) + b (% n) ma sens, a a (% n) + b (% m) nie.

Czy istnieje sposób na wymuszenie tego przy użyciu systemu typu Haskella? To samo odnosi się oczywiście do elementu tożsamości mempty: Jak można skonstruować 0 (% n)? Czy można w jakiś sposób zachować system znaków?

Czy takie struktury wymagają użycia typów zależnych?

Answer 1

Rozszerzając mój komentarz, oto pierwsze pęknięcie. Moduł jest wymuszany przez typ, ale nie na kanonicznym wyborze przedstawiciela: to jest właśnie wykonywane przez obliczenia, więc wymagałoby bariery abstrakcji. Dostępne są również typy ograniczonych liczb, ale wymagają one nieco więcej pracy.

Enter, {-# LANGUAGE KitchenSink #-}. Mam na myśli (właściwie nie jest tak źle)

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

i zacznijmy pękać.

Po pierwsze, po prostu odruchowo, wprowadzam Hasochistic liczby naturalne:

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 

moim zdaniem, to właśnie to, co robisz, gdy chcesz zadeklarować typ danych, a następnie pozostawić inne rodzaje zależy od jej wartości . Biblioteka "singletonów" Richarda Eisenberga automatyzuje konstrukcję.

(Jeżeli na przykład idzie używać numerów indeksów na wektorach, niektórzy wskazują, że wektory () może również służyć jako singletons dla Nat. Są technicznie poprawne, oczywiście, ale błędne. Gdy myślimy o Natty i NATTY jako systemowo generowane z Nat, są one uprawnieniem, które możemy wykorzystać lub nie, jak uważamy za stosowne, a nie dodatkowym do uzasadnienia.Ten przykład nie obejmuje wektorów, i byłoby to perwersyjne, aby wprowadzić wektory tylko po to, aby mieć singletony dla Nat .)

Ręcznie przetaczam kilka funkcji konwersji i instancji Show, abyśmy mogli zobaczyć, co robimy g, oprócz czegokolwiek innego.

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 

Teraz jesteśmy gotowi, aby zadeklarować Mod.

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

Typ przenosi moduł. Wartości zawierają nienormowany reprezentant klasy równoważności, ale lepiej wymyślimy, jak to znormalizować. Podział na liczby unarne jest szczególnym sportem, którego nauczyłem się jako dziecko.

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) 

Teraz możemy zrobić inteligentnego konstruktora.

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 

A potem wystąpienie Monoid jest proste:

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

I rzucił w niektórych innych rzeczy, zbyt:

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 

Przy odrobinie wygody ...

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

otrzymujemy

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

Więc tak, potrzebujesz rodzajów zależnych, ale Haskell jest zależnie wpisany na tyle.

Answer 2

To jest ta sama odpowiedź, którą podaje @pigworker, ale napisana mniej bolesną (bardziej wydajną, ładniejszą składnią).

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

i otrzymujemy

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

Moduł ten przedstawia również punkt zrobiłem w komentarzu w swoim pytaniu o równaniu. Poza modułem Mod nie można oszukiwać i używać reprezentacji.

Answer 3

Oprócz poprzednich odpowiedzi, może zainteresować Cię pakiet , który implementuje to jako bibliotekę z bardzo dobrą składnią.

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