haskell - 我可以让 KnownNat n 来暗示 KnownNat (n * 3) 等吗？

Question

我正在处理这种形状的数据类型，使用线性中的V:

type Foo n = V (n * 3) Double -> Double

将其固定在 n 上非常重要，因为我希望能够确保在编译时传递正确数量的元素。这是我的程序的一部分，已经运行良好，与我在这里所做的事情无关。

对于任何 KnownNat n，我可以生成一个 Foo n 来满足我的程序所需的行为。就这个问题而言，这可能是一些愚蠢的事情，例如

mkFoo :: KnownNat (n * 3) => Foo n
mkFoo = sum

或者更有意义的例子，它可以生成一个相同长度的随机V，并在两者上使用dot。这里的 KnownNat 约束是多余的，但实际上，需要它来创建 Foo。我制作一个 Foo 并将其用于我的整个程序(或多个输入)，因此这保证了我无论何时使用它，我都会在具有相同长度的东西上使用，并且在相同长度的东西上使用Foo 的结构决定了。

最后，我有一个为 Foo 提供输入的函数:

bar :: KnownNat (n * 3) => Proxy n -> [V (n * 3) Double]

bar 实际上是我使用 n * 3 作为类型函数而不是手动扩展它的原因。原因是 bar 可能通过使用三个长度为 n 的向量并将它们全部附加在一起作为长度为 n * 3 的向量来完成其工作。此外，从语义上来说，n 对于函数来说是比 n * 3 更有意义的参数。这也让我禁止使用不正确的值，例如 n 不是 3 的倍数等。

现在，以前，只要我在开始时定义了类型同义词，一切都会正常工作:

type N = 5

然后我可以将 Proxy::Proxy N 传递给 bar，并使用 mkFoo::Foo N。一切都运行良好。

-- works fine
doStuff :: [Double]
doStuff = let inps = bar (Proxy :: Proxy N)
          in  map (mkFoo :: Foo N) inps

但现在我希望能够在运行时通过从文件或命令行参数加载信息来调整 N。

我尝试通过调用 reflectNat 来做到这一点:

doStuff :: Integer -> Double
doStuff n = reflectNat 5 $ \pn@(Proxy :: Proxy n) ->
              let inps = bar (Proxy :: Proxy n)
              in  map (mkFoo :: Foo n) inps

但是...bar 和 mkFoo 需要 KnownNat (n * 3)，但 reflectNat 只是给出我KnownNat n。

有什么方法可以概括 reflectNat 给我的证明来满足 foo 吗？

Answer 1

所以，三个月后，我一直在寻找实现这一目标的好方法，但我最终确定了一个非常简洁的技巧，不需要任何一次性的新类型；它涉及使用 constraints 中的 Dict 图书馆；你可以轻松地写一个:

natDict :: KnownNat n => Proxy n -> Dict (KnownNat n)
natDict _ = Dict

triple :: KnownNat n => Proxy n -> Dict (KnownNat (n * 3))
triple p = reifyNat (natVal p * 3) $
             \p3 -> unsafeCoerce (natDict p3)

一旦获得Dict (KnownNat (n * 3)，您就可以对其进行模式匹配以获取范围内的(n * 3)实例:

case triple (Proxy :: Proxy n) of
  Dict -> -- KnownNat (n * 3) is in scope

您实际上也可以将它们设置为通用:

addNats :: (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Dict (KnownNat (n * m))
addNats px py = reifyNat (natVal px + natVal py) $
                  \pz -> unsafeCoerce (natDict pz)

或者，您可以将它们设为运算符，然后使用它们来“组合”字典:

infixl 6 %+
infixl 7 %*
(%+) :: Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m))
(%*) :: Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m))

您可以执行以下操作:

case d1 %* d2 %+ d3 of
  Dict -> -- in here, KnownNat (n1 * n2 + n3) is in scope

我已经将其封装在一个不错的库中， typelits-witnesses 我一直在使用。谢谢大家的帮助!