时间戳

首页 > 解决方案 > 为Haskell中的每个整数创建一个类型？

haskell - 为Haskell中的每个整数创建一个类型？

问题描述

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

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...

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

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 中创建这样的数据类型？

标签： haskell

解决方案

正如评论中所指出的，这个想法是利用自然数的类型级表示，因此您有 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

当您仅使用 naturals 来“标记”一个类型时，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"，无论这意味着什么，它都可以采用类型为 form 的代理值proxy n，并返回与类型级别参数对应的实际整数n。幸运的是，我们的原始元素的类型正好Z n适合类型模式，所以通过运行，我们得到了与中的类型级别对应的值级别。proxy nnatVal elIntegernZ 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)

推荐阅读