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

我正在处理这种形状的数据类型，使用V from linear:

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

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

For any 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 to 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

But...bar and mkFoo要求KnownNat (n * 3), but reflectNat只是给我KnownNat n.

有什么方法可以概括证明reflectNat让我满足foo ?

所以，三个月后，我一直在寻找实现这一目标的好方法，但我最终决定采用一个非常简洁的技巧，不需要任何一次性的新类型；它涉及使用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

我把它封装在一个漂亮的图书馆里，打字证人我一直在使用的。感谢大家的帮助！