在 Haskell 中使用 Data.Reflection 时由于类型不明确而无法显示

Question

我是Haskell的新手，我试图创建一个类型，代表任何实例的积分在一些模数。我在网上找到了一些示例代码，我正在使用它，所以我的类型定义看起来像这样:

data Zn n a = Zn !a !a

大多数事情都像我想的那样工作;我可以显示，添加，减去等。

instance (Integral a, Show a) => Show (Zn n a) where
   show (Zn n x) = printf "(%s mod %s)" (show (mod x n)) (show n)
instance (Integral a, Reifies n a) => Num (Zn n a) where
  Zn n x + Zn _ y = Zn n (mod (x + y) n)
  Zn n x - Zn _ y = Zn n (mod (x - y) n)
  Zn n x * Zn _ y = Zn n (mod (x * y) n)
  negate (Zn n x) = Zn n (n - x)
  abs = id
  signum x@(Zn _ 0) = x
  signum (Zn n _) = Zn n 1
  fromInteger x = Zn n (mod (fromInteger x) n)
    where n = reflect (Proxy :: Proxy n)

znToIntegral :: Integral a => Zn n a -> a
znToIntegral (Zn n x) = fromIntegral x

但是，我不能显示对这些类型进行算术运算的结果。例如，在GHCi中:

*Main> let x = Zn 5 3
*Main> x
(3 mod 5)
*Main> let y = Zn 5 7
(2 mod 5)
*Main> let z = x + y
*Main> z
<interactive>:6:1:
    No instance for (Integral a0) arising from a use of ‘print’
    The type variable ‘a0’ is ambiguous
    Note: there are several potential instances:
      instance Integral GHC.Int.Int16 -- Defined in ‘GHC.Int’
      instance Integral GHC.Int.Int32 -- Defined in ‘GHC.Int’
      instance Integral GHC.Int.Int64 -- Defined in ‘GHC.Int’
      ...plus 9 others
    In a stmt of an interactive GHCi command: print it

我发现这个问题已经出现在许多其他的方式，我已经尝试实现这些数字，并了解如何数据。反射包工作给我带来了一些麻烦。我也很好奇其他在别人看来更自然的实现。我最初尝试做的是

newtype Zn n a = Zn a

和切换，因为我认为它会简化事情，它没有特别。干杯!

Answer 1

在这个特殊的例子中，Zn是一个内部实现细节，它不应该用于构造数字。理想情况下，Zn甚至不应该从库中导出。相反，我们应该使用fromInteger和数字字面值来构造。

模量是通过反射在fromInteger中引入的，出于性能原因，我们只将其存储在Zn中，以避免进一步使用reflect(尽管我认为reflect默认情况下没有太多开销，因此我们可能不会从该方案中获得太多好处)。如果我们只使用fromInteger来创建新的Zn -s，那么在Reifies约束下，模量将在整个计算过程中保持一致。另一方面，如果我们手动将模量插入Zn，那么Zn的那一部分将始终具有该模量，而reify(我们提供隐式配置的方式)根本不会影响它。换句话说，它打乱了我们假定的不变量。

使用例子:

foo :: (Integral a, Reifies s a) => Zn s a -> Zn s a -> Zn s a
foo a b = e where
  c = 123
  d = a * b - 3
  e = negate (d + c)
showAFooResult = reify 12 ((Proxy :: Proxy s) -> show (foo 3 4 :: Zn s Int))
-- fooResult == "(0 mod 12)"

在foo的主体中，当我们使用reify插入12后，所有内容都将以CC_15为模数。

如果我们斜视一下，foo只是一个函数，它需要一个额外的Integral参数，它在内部用作模数。我们可以使用reify提供实参，使用Proxy中的s索引。

如果我们不提供任何值来插入Reifies孔，那么我们就不能取出值。当然我们不能打印它，就像我们不能打印一个函数一样。

我们可以打印Zn 5 5，因为它的类型是Num a => Zn n a，所以我们没有空白要填充。另一方面，Zn 5 5 + Zn 5 5具有类型(Integral a, Reifies n a) => Zn n a，因为我们在Num实例中指定了Reifies n a约束，当然+的使用需要Num实例。这里我们必须使用reify(或调用它的其他辅助函数)来提取结果。

Answer 2

比较一下，这里有一个不存储模数的实现，并且总是使用reflect:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
import Data.Reflection
import Data.Proxy
import Text.Printf
newtype Zn a s = Zn { getZ :: a }
instance (Integral a, Show a, Reifies s a) => Show (Zn a s) where
       show x = 
           let 
               p = reflect (Proxy::Proxy s)           
           in
               printf "(%s mod %s)" (show (mod (getZ x) p)) (show p)
instance (Integral a, Reifies s a) => Num (Zn a s) where
      Zn x + Zn y = Zn (mod (x + y) (reflect (Proxy::Proxy s)))
      Zn x - Zn y = Zn (mod (x - y) (reflect (Proxy::Proxy s)))
      Zn x * Zn y = Zn (mod (x * y) (reflect (Proxy::Proxy s)))
      negate (Zn x) = Zn ((reflect (Proxy::Proxy s)) - x)
      abs = id
      signum x@(Zn 0) = x
      signum _ = Zn 1
      fromInteger x = Zn (mod (fromInteger x) p)
            where p = reflect (Proxy :: Proxy s)

一些辅助函数:

znToIntegral :: Integral a => Zn a s -> a
znToIntegral (Zn x) = fromIntegral x
-- Convince the compiler that the phantom type in the proxy
-- is the same as the one in the Zn
likeProxy :: Proxy s -> Zn a s -> Zn a s
likeProxy _ = id
withZn :: Integral a => a -> (forall s. Reifies s a => Zn a s) -> a
withZn p z = reify p $ proxy -> znToIntegral . likeProxy proxy $ z 

使用示例:

main :: IO ()
main = print $ withZn (7::Int) (Zn 3 + Zn 5)