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

Question

我正在处理这种形状的数据类型,使用Vfromlinear:

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

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

Answer 2

我发布了另一个答案，因为它更直接，编辑前一个答案没有意义。

\n\n

事实上，使用这个技巧（即使不是爱德华·克梅特发明的，也很受欢迎），来自反思 reifyNat：

\n\n

{-# LANGUAGE GADTs #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE KindSignatures #-}\n{-# LANGUAGE TypeOperators #-}\n{-# LANGUAGE ScopedTypeVariables #-}\n{-# LANGUAGE FlexibleContexts #-}\nimport GHC.TypeLits\nimport Data.Proxy\nimport Unsafe.Coerce\n\nnewtype MagicNat3 r = MagicNat3 (forall (n :: Nat). KnownNat (n * 3) => Proxy n -> r)\n\ntrickValue :: Integer -> Integer\ntrickValue = (*3)\n\n-- No type-level garantee that the function will be called with (n * 3)\n-- you have to believe us\ntrick :: forall a n. KnownNat n => Proxy n -> (forall m. KnownNat (m * 3) => Proxy m -> a) -> a\ntrick p f = unsafeCoerce (MagicNat3 f :: MagicNat3 a) (trickValue (natVal p)) Proxy\n\ntest :: forall m. KnownNat (m * 3) => Proxy m -> Integer\ntest _ = natVal (Proxy :: Proxy (m * 3))\n

\n\n

所以当你运行它时：

\n\n

\xce\xbb *Main > :t trick (Proxy :: Proxy 4) test :: Integer\ntrick (Proxy :: Proxy 4) test :: Integer :: Integer\n\xce\xbb *Main > trick (Proxy :: Proxy 4) test :: Integer\n12\n

\n\n

这一技巧基于这样一个事实：在 GHC 中，单成员类字典（如KnownNat）由成员本身表示。事实KnownNat证明是这样的Integer。所以我们就unsafeCoerce在那里。通用量化使其从外部听起来如此。

\n