为Haskell中的每个Integer创建一个类型? [英] Create a type for each Integer in Haskell?

问题描述

我想在Haskell中创建一个表示整数mod n 的数据类型，该数据类型是 Num 的实例，以帮助执行简单的模块化算术运算.我的第一次尝试看起来像这样

I would like to create a data type in Haskell that represents the integers mod n, and which is an instance of Num to help perform simple modular arithmetic operations. My first attempt at this looked like this

data Z n e = El n e
instance (Show n, Show e) => Show (Z n e) where
    show (El n e) = show e ++ " (mod " ++ show n ++ ")"

instance (Integral k, Integral e) => Num (Z k e) where
    (+) (El n a) (El m b) = El n (mod (a + b) n)
    (-) (El n a) (El m b) = El n (mod (a - b) n)
    (*) (El n a) (El m b) = El n (mod (a * b) n)
    negate (El n a) = El n (mod (0 - a) n)
    abs (El n a) = El n a
    signum (El n a) = El n a
    fromInteger i = -- problematic...

这可以编译，但是有问题，不仅因为由于 k 超出范围而不清楚如何实现 fromInteger ，而且还因为它允许添加整数 mod 4 ，且整数 mod 5 没有类型错误.在我的第二次尝试中，我试图解决这些问题

This compiles but is problematic not only because its unclear how to implement fromInteger since k is out of scope, but also because it is permissible to add an integer mod 4 with an integer mod 5 without a type error. In my second attempt I tried to resolve these issues

data Z n = El Integer
instance (Show n) => Show (Z n) where
    show (El n e) = show e ++ " (mod " ++ show n ++ ")"

instance (Integral k) => Num (Z k) where
    (+) (El k a) (El k b) = El k (mod (a + b) k)
    (-) (El k a) (El k b) = El k (mod (a - b) k)
    (*) (El k a) (El k b) = El k (mod (a * b) k)
    negate (El k a) = El k (mod (0 - a) k)
    abs (El k a) = El k a
    signum (El k a) = El k a
    fromInteger i = El (fromIntegral i) k

但是我在实现 Num 接口时遇到了麻烦，因为 k 的定义有冲突，但仍然超出范围.如何在Haskell中创建这样的数据类型?

but I am running into trouble implementing the Num interface because of conflicting definitions of k which is still out of scope. How can I make such a data type in Haskell?

推荐答案

如注释中所述，其想法是利用自然数的类型级别表示形式，因此对于2，3或3分别具有可识别的类型4等.这需要扩展:

As noted in the comments, the idea is to make use of a type-level representation of natural numbers, so you have separate identifiable types for 2 versus 3 versus 4, etc. This requires an extension:

{-# LANGUAGE DataKinds #-}

有两种主要方法可以将自然值表示为类型.第一种是定义递归数据类型:

There are two main methods for representing naturals as types. The first is to define a recursive data type:

data Nat' = Z | S Nat'

， DataKinds 扩展名会自动提升为类型级别.然后，您可以将其用作类型级别的标记，以定义一系列相关但不同的类型:

which the DataKinds extension automatically lifts to the type level. You can then use this as, among other things, a type-level tag to define a family of related but distinct types:

{-# 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 )提升到类型级别.它的工作方式大致相同:

The second is to use a built-in GHC facility that automatically lifts integer literals, like 2 and 3 to the type level. It works much the same way:

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

当您仅使用自然符号来标记"类型时，通常使用 Nat 的 GHC.TypeLits 版本更为方便.如果您必须实际对类型进行类型级别的计算，则使用递归版本更容易完成某些计算.

When you're using naturals only to "tag" a type, it's generally more convenient to use the GHC.TypeLits version of Nat. If you have to actually do type-level computations on the types, some computations are more easily done using the recursive version.

由于我们只需要使用自然字符作为标记，因此我们可以坚持使用 GHC.TypeLits 解决方案.因此，我们将像这样定义您的数据类型:

Since we only need the naturals as tags, we can stick with the GHC.TypeLits solution. So, we'd define your data type like so:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
import GHC.TypeLits
data Z (n :: Nat) = El Integer

在 Show 实例中，我们需要利用 GHC.TypeLits 中的其他功能将类型级别的 Nat 转换为我们可以在印刷表示形式中包含的值级 Integer :

In the Show instance, we need to make use of some other facilities in GHC.TypeLits to convert the type-level Nat to a value-level Integer that we can include in the printed representation:

instance (KnownNat n) => Show (Z n) where
  show el@(El e) = show e ++ " (mod " ++ show (natVal el) ++ ")"

这里正在发生魔术！ natVal 函数具有签名:

There's magic going on here! The natVal function has signature:

natVal :: forall n proxy. KnownNat n => proxy n -> Integer

意味着对于"KnownNat" ，无论意味着什么，它都可以采用类型为 proxy n 形式的代理值，并返回对应于的实际整数类型级参数 n .幸运的是，我们的原始元素的类型为 Z n ，它恰好适合 proxy n 类型的模式，因此通过运行 natVal el ，我们可以获得值级别 Integer 对应于 Z n 中类型级别 n .

meaning that for a "KnownNat", whatever that means, it can take a proxy value whose type is of form proxy n, and return the actual integer corresponding to the type-level argument n. Fortunately, our original element has type Z n which fits the proxy n type pattern just fine, so by running natVal el, we get the value-level Integer corresponding to the type-level n in Z n.

我们将在 Integral 实例中使用相同的魔术:

We'll use the same magic in the Integral instance:

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 构造函数中消失了，因为它不是数据级别的数量.可以在需要的地方使用 KnownNat 实例使用 natVal el 对其进行检索.

Note that the k disappears from the El constructor, because it's not a data-level quantity. Where needed, it can be retrieved using natVal el using the KnownNat instance.

完整程序为:

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

这篇关于为Haskell中的每个Integer创建一个类型?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！