扩展我的评论，这是第一个裂缝。模数是由类型强制的，但不是代表的规范选择：这只是通过计算完成的，因此需要抽象障碍。有界数的类型也是可用的，但它们需要更多的工作。
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
在我看来，这正是当您想要声明数据类型然后允许其他类型依赖于其值时所做的事情。理查德·艾森伯格（Richard Eisenberg）的“单例”库使构建自动化。
（如果这个例子继续使用数字来索引向量，有些人指出向量()也可以作为单例Nat。当然，他们在技术上是正确的，但却被误导了。当我们想到Natty and 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)))
we get
> foldMap rep [1..5] :: Mod Four
(3 :% 4)
所以是的，你确实需要依赖类型，但 Haskell 的依赖类型已经足够了。
