如评论中所述，这个想法是利用自然数的类型级表示，因此您可以拥有单独可识别的类型，例如2与3与4等。 这需要一种扩展：
{-# LANGUAGE DataKinds #-}
将自然数表示为类型有两种主要方法。第一种是定义递归数据类型：
data Nat' = Z | S Nat'
DataKinds 扩展自动将其提升到类型级别。然后，您可以将其用作类型级别标记，以定义一系列相关但不同的类型。
{-# LANGUAGE KindSignatures #-}
data Foo (n :: Nat') = Foo Int
twoFoo :: Foo (S (S Z))
twoFoo = Foo 10
threeFoo :: Foo (S (S (S Z)))
threeFoo = Foo 20
addFoos :: Foo n -> Foo n -> Foo n
addFoos (Foo x) (Foo y) = Foo (x + y)
okay = addFoos twoFoo twoFoo
bad = addFoos twoFoo threefoo
第二种方法是使用 GHC 内置的功能，自动将整数字面量（如
2和
3）提升到类型级别。它的工作方式与第一种方法类似：
import GHC.TypeLits (Nat)
data Foo (n :: Nat) = Foo Int
twoFoo :: Foo 2
twoFoo = Foo 10
threeFoo :: Foo 3
threeFoo = Foo 20
addFoos :: Foo n -> Foo n -> Foo n
addFoos (Foo x) (Foo y) = Foo (x + y)
okay = addFoos twoFoo twoFoo
bad = addFoos twoFoo threefoo
当您仅使用自然数“标记”类型时，通常更方便使用
GHC.TypeLits版本的
Nat。 如果必须在类型上实际执行类型级计算，则某些计算可以使用递归版本更轻松地完成。
由于我们只需要将自然数用作标记，因此我们可以坚持使用
GHC.TypeLits解决方案。 因此，我们应该这样定义您的数据类型：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
import GHC.TypeLits
data Z (n :: Nat) = El Integer
在
Show实例中，我们需要利用
GHC.TypeLits中的其他工具将类型级别的
Nat转换为值级别的
Integer，以便将其包含在打印表示中。
instance (KnownNat n) => Show (Z n) where
show el@(El e) = show e ++ " (mod " ++ show (natVal el) ++ ")"
这里有一些神奇的事情发生了！
natVal函数的签名如下：
natVal :: forall n proxy. KnownNat n => proxy n -> Integer
意味着对于一个"KnownNat"（不知道是什么的）类型，它可以接受一个类型为"proxy n"的代理值，并返回与类型级别参数"n"对应的实际整数。幸运的是，我们的原始元素具有类型"Z n"，非常适合"proxy n"类型模式，因此通过运行"natVal el"，我们得到了与"Z n"中类型级别的"n"相对应的值级别"Integer"。
我们将在"Integral"实例中使用同样的魔法：
instance (KnownNat k) => Num (Z k) where
(+) el@(El a) (El b) = El (mod (a + b) k) where k = natVal el
(-) el@(El a) (El b) = El (mod (a - b) k) where k = natVal el
(*) el@(El a) (El b) = El (mod (a * b) k) where k = natVal el
negate el@(El a) = El (mod (0 - a) k) where k = natVal el
abs el@(El a) = El a where k = natVal el
signum el@(El a) = El 1
fromInteger i = El (fromIntegral i)
请注意，
El构造函数中的
k被省略了，因为它不是数据级量。在需要时，可以使用
KnownNat实例和
natVal el来检索它。
完整程序如下：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
import GHC.TypeLits
data Z (n :: Nat) = El Integer
instance (KnownNat n) => Show (Z n) where
show el@(El e) = show e ++ " (mod " ++ show (natVal el) ++ ")"
instance (KnownNat k) => Num (Z k) where
(+) el@(El a) (El b) = El (mod (a + b) k) where k = natVal el
(-) el@(El a) (El b) = El (mod (a - b) k) where k = natVal el
(*) el@(El a) (El b) = El (mod (a * b) k) where k = natVal el
negate el@(El a) = El (mod (0 - a) k) where k = natVal el
abs el@(El a) = El a where k = natVal el
signum el@(El a) = El 1
fromInteger i = El (fromIntegral i)
它按预期工作：
> :set -XDataKinds
> (El 2 :: Z 5) + (El 3 :: Z 5)
0 (mod 5)
> (El 2 :: Z 5) + (El 3 :: Z 7)
<interactive>:15:18: error:
• Couldn't match type ‘7’ with ‘5’
Expected type: Z 5
Actual type: Z 7
• In the second argument of ‘(+)’, namely ‘(El 3 :: Z 7)’
In the expression: (El 2 :: Z 5) + (El 3 :: Z 7)
In an equation for ‘it’: it = (El 2 :: Z 5) + (El 3 :: Z 7)
Integral k意味着k是一个包含整数（或类似整数）的类型，但你想表达的是k本身就是一个整数。请查阅关于类型级别自然数的相关资料，有很多可供参考。 - luqui