在 Haskell 中使用 Data.Reflection 返回具体化类型

Question

这是一个关于 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

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

Data.Reflection 中 reify 的签名是

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

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

Answer 1

您可以将值提升为类型。但类型无法逃脱执行提升操作的函数。这就是 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调用下创建它们。这不是一个错误，而是一个功能！