哈斯克爾：如何編寫一個`Monoid`實例取決於參數

Question

我正在爲一個小型圖書館的大學做整數計算在cyclic group;喜歡的東西：

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

'整數（％N）'清楚地形成下加入幺與'0（％N）'身份元素。但是，只有當兩個操作數的模數相同時，加法纔有意義：a (% n) + b (% n)有意義，而a (% n) + b (% m)則不適用。

有什麼辦法可以用Haskell的類型系統強制執行嗎？當然，mempty標識元素也是如此：0 (% n)如何構建？ n可以保存在類型系統中嗎？

或者像這樣的結構需要使用依賴類型嗎？

Answer 1

擴展我的評論，這是第一個裂縫。模數是按類型強制執行的，但不是代表性的典型選擇：這只是通過計算完成的，所以需要一個抽象障礙。有限數字的類型也是可用的，但他們需要更多的工作。

Enter，{-# LANGUAGE KitchenSink #-}。我的意思是（實際上不是太差）

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

讓我們開始吧。

首先，僅僅通過神經反射，我介紹Hasochistic自然數：

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依賴於足夠的類型。

Answer 2

這與@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模塊之外，您無法作弊並使用該表示。

Answer 3

除了之前的答案，您可能會對軟件包感興趣，該軟件包將其作爲具有非常好語法的庫實現。

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