5

这是一个关于 Haskell 中 Data.Reflection 的类型问题。反射让我接受一个 Int 并将其转换为一种类型。

下面的函数 f 和 g 是我们对合理事物的最佳尝试，如果您有更好的方法，让我们拥有它！

例如，我可以通过执行以下操作添加数字 mod 41：

import Data.Reflection
import Data.Proxy

newtype Zq q i = Zq i deriving (Eq)
instance (Reifies q i, Integral i) => Num (Zq q i) where
   (...)
zqToIntegral :: (Reifies q i, Integral i) => Zq q i -> i
   (...)

f :: forall i . (Integral i) => i -> (forall q . Reifies q i => Zq q i) -> i
f modulus k = 
    reify modulus (\ (_::Proxy t) -> zqToIntegral (k :: Zq t i)

然后

>>:t (f 41 (31+15))
(f 41 (31+15)) :: Integral i => i

但是，我们想编写如下函数：

g :: forall i . (Integral i) => i -> (forall q . Reifies q i => Zq q i) -> Zq q i
g modulus k = 
    reifyIntegral modulus (\ (_::Proxy t) -> (k :: Zq t i)

并想得到：

>>:t (g 41 (31+15))
(g 41 (31+15)) :: <some type info> => Zq q i

不同之处在于我们希望能够返回一个使用 reified int 的类型。上述定义的至少一个问题是 rank-2 类型 q 对返回类型不可见。

Data.Reflection 中 reify 的签名是

reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r

据我们所知，这需要 rank-2 类型，并且我们不知道（如果确实可能）如何将此类型公开给函数的返回类型。

4

1 回答 1

1

您可以将值提升为类型。但是该类型无法逃避执行提升的功能。这就是 rank 2 类型的工作方式。g想象一下，如果我们能像你描述的那样写作。然后，给定一些用户输入值，我们可以Zq在运行时得到不同的 qs。

但是我们能用它们做什么呢？

如果我们有两个Zq相同的q，我们可以添加它们。但是直到运行时我们才知道它们是否相同！现在检查类型为时已晚，因为我们需要在编译时决定是否可以添加它们。如果您忽略处于幻像位置的事实q，这与您不能在编译时根据输入返回 anInt或 a的函数的原因相同（当然，您可以使用 an ）。BoolEither

因此，如评论中所述，您可以做一些不同的事情。

您可以做的一件事就是在运行时返回模数（即 的值级版本q）以及您的结果。然后您可以随时使用它。

看起来像这样：

g :: forall i . (Integral i) => i -> (forall q . Reifies q i => Zq q i) -> (i,i)
g modulus k = reify modulus (\ m@(_::Proxy t) -> (zqToIntegral (k :: Zq t i), reflect m))

您可以做的另一件事是像这样使用存在主义：

data ZqE i = forall q. ZqE (Zq q i)

h :: forall i . (Integral i) => i -> (forall q . Reifies q i => Zq q i) -> ZqE i
h modulus k = reify modulus (\ (_::Proxy t) -> ZqE (k :: Zq t i))

现在我们对 ZqE 唯一能做的就是解压它并返回其他也不会q直接暴露在类型中的东西。

请注意，我们无法知道q任意两个ZqE中的 是否相等，因此我们不能直接将它们组合在一起，而是应该在同一个reify调用下创建它们。这不是一个错误，而是一个功能！

于 2013-02-06T03:53:39.270 回答