如评论中所述,这个想法是利用自然数的类型级表示,因此您可以拥有单独可识别的类型,例如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