为Haskell中的每个Integer创建一个类型？

如评论中所述，其想法是利用自然数的类型级别表示，因此对于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 -- error: different types

第二种是使用内置的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 -- type error

当您仅使用自然语言来“标记”类型时，通常使用的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

意味着对于a而言"KnownNat"，无论意味着什么，它都可以采用类型为形式的代理值proxy n，并返回与type-level参数相对应的实际整数n。幸运的是，我们原来的元素具有类型Z n符合该proxy n类型模式就好了，这样通过运行natVal el，我们获得的价值层面Integer与该类型相应级别n在Z n。

我们将在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)

注意，构造函数中的k消失消失了El，因为它不是数据级别的数量。在需要的地方，可以natVal el使用KnownNat实例进行检索。

完整的程序是：

{-# 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)