在Haskell中使用自然数是否有实用的方法？

Question

我正在学习Haskell,并希望在一些构造函数中强制使用正整数(1,2,3,...),但我似乎只能找到'Int'和'Integer'数据类型.

我可以使用规范

data Nat = Zero | Succ Nat

但后来我不能用1,4,......来表示它们.

所以我问,有没有办法实现这个目标？(就像在C中使用'unsigned')

提前致谢.

编辑:正如CA McCann所解释的那样,我将把它隐藏在一个模块中.另外,我必须添加以下链接: http: //haskell.org/haskellwiki/Smart_constructors以获取有关该主题的摘要.感谢您抽出宝贵时间回答!

Answer 1

通常有两种方法:您给出的归纳定义,或者使用其他东西进行内部表示的抽象数据类型.

请注意,归纳表示对于大数字而言并不是非常有效; 然而,它可以是懒惰的,这可以让你做一些事情,比如看看两个nat中哪一个更大,而不进一步评估较小的那个.

抽象数据类型是在单独的模块中定义的并且不导出其构造函数的类型,示例是IO或Data.Set.Set.你可以定义这样的东西:

module Nat (Nat() {- etc. -} ) where

newtype Nat = Nat { unNat :: Integer }

...在哪里导出各种操作Nat,即使内部表示只是公正的Integer,你也要确保没有Nat构造带有负值的类型值.

在这两种情况下,如果你想使用数字文字,你需要一个fromInteger附加到Num类型类的定义,这对于自然数字来说是完全错误的但是很好.

如果你不介意制作一个破坏的实例只是为了获得语法细节,你可以这样做:

instance Num Nat where
    Zero + n = n
    n + Zero = n
    (Succ n1) + (Succ n2) = Succ . Succ $ n1 + n2

    fromInteger 0 = Zero
    fromInteger i | i > 0 = Succ . fromInteger $ i - 1

......等等,用于其他功能.对于抽象数据类型方法也可以这样做,只是注意不要deriving用来获取自动Num实例,因为它会愉快地破坏你的非负约束.

Answer 2

您可以使用Data.Word中的Word32,它对应于C中的uint32_t.

使用Word32,您会遇到与C中的无符号类型相同的问题,尤其是上溢和下溢.如果要确保不会发生这种情况,则需要将其包装为newtype并仅导出智能构造函数.因此,不可能有加法,减法等,并且不存在上溢或下溢的风险.例如,如果要支持添加,可以添加和导出用于添加无符号整数的函数,但检查溢出(并且会降低性能).它可能看起来像这样:

module NT(UInt, addUInts) where

import Data.Word

newtype UInt = UInt Word32
  deriving (Show)

mkUInt :: Word32 -> UInt
mkUInt = UInt

addUInts :: UInt -> UInt -> Maybe UInt
addUInts (UInt u1) (UInt u2) =
  let u64 :: Word64
      u64 = fromIntegral u1 + fromIntegral u2
  in if u64 > fromIntegral (maxBound :: Word32)
       then Nothing
       else Just (UInt (fromIntegral u64))