haskell - 在 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

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

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

如果我们有两个 Zq同q ，我们可以添加它们。但是直到运行时我们才知道它们是否是相同的 q!现在检查类型为时已晚，因为我们需要在编译时决定是否可以添加它们。如果您忽略 q 的事实处于幻象位置，这与您不能拥有返回 Int 的函数的原因相同或 Bool在编译时，基于输入(当然，您可以使用 Either )。

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

您可以做的一件事就是在运行时返回模数(即 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))

你可以做的另一件事是像这样使用existentials:

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 下创建它们。称呼。这不是错误，而是一个功能!