Haskell：パラメータに依存するもののために `Monoid`インスタンスを書く方法

Question

私はcyclic groupで整数計算を行う大学の小さなライブラリに取り組んでいます。以下のようなもの：

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

'整数（％n）は'は明らかに識別素子として'0（％n）が' と付加下モノイドを形成します。しかし、加算は、加算される2つのオペランドのモジュロが同じである場合にのみ意味をなさない：a (% n) + b (% n)は意味をなさないが、a (% n) + b (% m)はそうではない。

ハスケル型システムでこれを強制する方法はありますか？ memptyアイデンティティ要素についても同じことが当てはまります。0 (% n)はどのように構築できますか？ nは何とか型システムに保管できますか？

また、これらのような構造体には従属型の使用が必要ですか？

Answer 1

私のコメントでは、最初の亀裂が広がっています。モジュラスは型によって強制されますが、代表的なものの標準的な選択ではありません。それは単に計算によって行われるため、抽象化の障壁が必要になります。有界数の型も使用できますが、もう少し作業が必要です。

を入力してください。{-# 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 

：

はまず、単に反射によって、私はHasochistic自然数を導入します。 Richard Eisenbergの "singletons"ライブラリは、構築を自動化します。

（例はインデックスベクトルに番号を使用するために行く場合は、一部の人は()のベクトルはまたNatのためにシングルトンとしての役割を果たすことができることを指摘している。彼らは技術的には、正しいもちろん、しかし、見当違いだ。我々はNattyについて考えるときそしてNATTYは、Natから体系的に生成されたものであり、当てはまるものとして利用できるかどうかは分かりませんが、これはベクトルを含まないため、ベクトルを導入してNat 。）

私は、変換関数とShowインスタンスを手渡しているので、私たちは何をしているのか分かります他のものとは別に、g。

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) 

はい、依存型が必要ですが、ハスケルは十分に型付けされています。

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