9

我正在为大学开发一个小型图书馆，该图书馆在循环组中进行整数计算；像：

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

'Integers (% n)'清楚地形成一个以'0 (% n)'作为单位元素的加法运算。然而，只有当两个被相加的操作数的模数相同时，加法才有意义：a (% n) + b (% n)有意义，而a (% n) + b (% m)没有。

有没有办法用 Haskell 的类型系统来强制执行这一点？恒等元素当然也是如此mempty：如何0 (% n)构造？可以n以某种方式保存在类型系统中吗？

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

4

3 回答 3

17

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

输入，{-# 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 的依赖类型已经足够了。

于 2016-09-24T10:18:58.037 回答
13

这与@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 模块之外，您不能作弊并使用该表示。

于 2016-09-25T07:14:32.507 回答
5

除了前面的答案之外，您可能对模块化算术包感兴趣，该包将其实现为具有非常好的语法的库。

>>> import Data.Modular
>>> 10 * 11 :: ℤ/7
5
于 2016-09-26T07:04:04.267 回答