Haskell:如何为依赖于参数的东西编写一个`Monoid`实例

Question

我正在为大学开设一个小型图书馆,在一个循环组中进行整数计算; 像:

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

'整数(%n)'明显形成一个幺半群,加上'0(%n)'作为同一性元素.但是,只有当添加的两个操作数的模数相同时,a (% n) + b (% n)才有意义:有意义,而a (% n) + b (% m)不是.

有没有办法用Haskell的类型系统强制执行此操作？对于mempty身份元素当然也是如此:如何0 (% n)构建？可以n以某种方式保存在类型系统中？

或者像这样的结构是否需要使用依赖类型？

Answer 1

扩展我的评论,这是第一次破解.模数是按类型强制执行的,而不是代表性的规范选择:这只是通过计算完成的,因此需要一个抽象障碍.有界数字的类型也可用,但它们需要更多的工作.

输入,{-# 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

在我看来,这就是当你想要声明一个数据类型然后允许其他类型依赖于它的值时你所做的.Richard Eisenberg的"单身人士"图书馆使建筑自动化.

(如果这个例子继续使用数字来索引向量,有些人指出,向量()也可以作为单例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

这个模块还说明了我在关于Eq的问题中的评论中提出的观点.在Mod模块之外,您不能作弊并使用表示.

Answer 3

除了之前的答案,您可能对模块算术包感兴趣,该程序包将其实现为具有非常好语法的库.

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