我可以让KnownNat n暗示KnownNat（n * 3）等吗？ [英] Can I get KnownNat n to imply KnownNat (n * 3), etc?
问题描述
我正在处理这种形状的数据类型，使用 linear 中的 V ：
type Foo n = V（n * 3）Double - > Double
固定在 n 很重要，因为我希望能够确保在编译时传递正确数目的元素。这是我的程序的一部分，已经运行良好，与我在这里做的事情无关。
对于任何 KnownNat n ，我可以生成满足我的程序需要的行为的 Foo n 。对于这个问题，它可能是一些愚蠢的东西，例如：
mkFoo :: KnownNat（n * 3）=> Foo n
mkFoo = sum
或者对于更有意义的示例，它可以生成一个随机 V 具有相同的长度，并在两者上使用点。这里的 KnownNat 约束是多余的，但实际上，需要做一个 Foo 。我做了一个 Foo ，并将其用于我的整个程序（或多个输入），所以这保证了我每当使用它时都使用相同的东西长度以及 Foo 的结构决定的事情。
Foo ： bar :: KnownNat（n * 3 ）=>代理n - > [V（n * 3）Double]
bar 为什么我使用 n * 3 作为类型函数，而不是仅仅手动扩展它。原因是 bar 可能通过使用长度 n 的三个向量来完成它的工作并将它们作为一个向量附加在一起长度 n * 3 。而且， n 对于函数来说是一个更有意义的参数，在语义上比 n * 3 更有意义。这也让我不能容忍不正确的值，比如不是3的倍数的 n 的其他值。
现在，之前，只要我在开头定义了一个类型同义词，一切都可以正常工作：
type N = 5
然后我可以传入 Proxy :: Proxy N 到 bar ，并使用 mkFoo :: Foo N 。
- 正常工作
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） - >
让inps = bar（Proxy :: Proxy n）
in map（mkFoo :: Foo n）inps
但是... bar 和 mkFoo require KnownNat n * 3），但 reflectNat 只是给我 KnownNat n 。
有什么办法可以概括证明 reflectNat 让我满足 foo
我发表了另一个答案，因为它更直接，编辑以前没有任何意义。 p>
实际上使用这个技巧（如果不是由Edward Kmett发明的话就会普及），从反思 reifyNat ：
<$ p $
{ - ＃LANGUAGE数学类型＃ - }
{ - ＃语言类型签名＃ - }
{ - ＃LANGUAGE TypeOperators＃ - }
{ - ＃LANGUAGE ScopedTypeVariables＃ - }
{ - ＃LANG UAGE FlexibleContexts＃ - }
import GHC.TypeLits
import Data.Proxy
import Unsafe.Coerce
newtype MagicNat3 r = MagicNat3（forall（n :: Nat） 。 KnownNat（n * 3）=>代理n - > r）
trickValue :: Integer - >整数
trickValue =（* 3）
- 没有类型级别的保证函数将被调用（n * 3）
- 您必须相信我们
trick：forall a n。 KnownNat n =>代理n - > （m m KnownNat（m * 3）=> Proxy m - > a） - >
技巧p f = unsafeCoerce（MagicNat3 f :: MagicNat3 a）（trickValue（natVal p））代理
test :: forall m。 KnownNat（m * 3）=>代理m - >整数
test _ = natVal（Proxy :: Proxy（m * 3））
当你运行它时：
λ* Main> ：t trick（Proxy :: Proxy 4）test :: Integer
trick（Proxy :: Proxy 4）test :: Integer :: Integer
λ* Main>技巧（Proxy :: Proxy 4）test :: Integer
12
因为在GHC中，一个成员类字典（如 KnownNat ）由成员本身表示。在 KnownNat 情况下，它变成了整数。所以我们只是 unsafeCoerce 它。通用量化使它从外部发出。
I'm working with data types of this shape, using V from linear:
type Foo n = V (n * 3) Double -> Double
Having it fixed on n is pretty important, because I want to be able to ensure that I'm passing in the right number of elements at compile-time. This is a part of my program that already works well, independent of what I'm doing here.
For any KnownNat n, I can generate a Foo n satisfying the behavior that my program needs. For the purposes of this question it can be something silly like
mkFoo :: KnownNat (n * 3) => Foo n
mkFoo = sum
Or for a more meaningful example, it can generate a random V of the same length and use dot on the two. The KnownNat constraint here is redundant, but in reality, it's needed to do make a Foo. I make one Foo and use it for my entire program (or with multiple inputs), so this guarantees me that whenever I use it, I'm using on things with the same length, and on things that the structure of the Foo dictates.
And finally, I have a function that makes inputs for a Foo:
bar :: KnownNat (n * 3) => Proxy n -> [V (n * 3) Double]
bar is actually the reason why i'm using n * 3 as a type function, instead of just manually expanding it out. The reason is that bar might do its job by using three vectors of length n and appending them all together as a vector of length n * 3. Also, n is a much more meaningful parameter to the function, semantically, than n * 3. This also lets me disallow improper values like n's that aren't multiples of 3, etc.
Now, before, everything worked fine as long as I defined a type synonym at the beginning:
type N = 5
And I can just then pass in Proxy :: Proxy N to bar, and use mkFoo :: Foo N. And everything worked fine.
-- works fine
doStuff :: [Double]
doStuff = let inps = bar (Proxy :: Proxy N)
in map (mkFoo :: Foo N) inps
But now I want to be able to adjust N during runtime by loading information from a file, or from command line arguments.
I tried doing it by calling 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 require KnownNat (n * 3), but reflectNat just gives me KnownNat n.
Is there any way I can generalize the proof that reflectNat gives me to satisfy foo ?
I post another answer as it is more direct, editing the previous won't make sense.
In fact using the trick (popularised if not invented by Edward Kmett), from reflections reifyNat:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
import GHC.TypeLits
import Data.Proxy
import Unsafe.Coerce
newtype MagicNat3 r = MagicNat3 (forall (n :: Nat). KnownNat (n * 3) => Proxy n -> r)
trickValue :: Integer -> Integer
trickValue = (*3)
-- No type-level garantee that the function will be called with (n * 3)
-- you have to believe us
trick :: forall a n. KnownNat n => Proxy n -> (forall m. KnownNat (m * 3) => Proxy m -> a) -> a
trick p f = unsafeCoerce (MagicNat3 f :: MagicNat3 a) (trickValue (natVal p)) Proxy
test :: forall m. KnownNat (m * 3) => Proxy m -> Integer
test _ = natVal (Proxy :: Proxy (m * 3))
So when you run it:
λ *Main > :t trick (Proxy :: Proxy 4) test :: Integer
trick (Proxy :: Proxy 4) test :: Integer :: Integer
λ *Main > trick (Proxy :: Proxy 4) test :: Integer
12
The trick is based on the fact that in GHC the one member class dictionaries (like KnownNat) are represented by the member itself. In KnownNat situation it turns out to be Integer. So we just unsafeCoerce it there. Universal quantification makes it sound from the outside.
这篇关于我可以让KnownNat n暗示KnownNat（n * 3）等吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
