我可以有一个未知的KnownNat吗？

本文介绍了我可以有一个未知的KnownNat吗？的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述 29岁程序员，3月因学历无情被辞！ 我不知道我是否可以吃我的蛋糕，也可以吃 KnownNats 。我可以编写使用 Nats 的代码，它们可能都是 KnownNats 和 UnknownNats （ SomeNats ？）。 > Vec（n :: Nat）a ，我可以编写在编译和运行时知道大小的代码吗？事情是，我不想复制整个代码的静态和动态大小的事情。我不想通过在数据结构中存储大小来失去静态的保证。 编辑 回答AndrásKovács： 我的具体用例是从磁盘读取图像（幸运的是固定大小），然后从中提取补丁，所以基本上我有一个函数 extractPatch ::（KnownNat w2，KnownNat h2）=>图像w1 h1 a - >补丁w2 h2 a其中图像和补丁是常见的 Mat（w :: Nat）（h :: Nat）一个类型。 如果我不知道图像大小，我将不得不在运行时类型中对其进行编码。只是想知道。解决方案 { - ＃LANGUAGE DataKinds，KindSignatures，ScopedTypeVariables＃ - } import GHC.TypeLits import Data.Proxy data Bar（n :: Nat）= Bar字符串派生Show bar :: KnownNat n =>栏n - > （String，Integer） bar b @（Bar s）=（s，natVal b） KnownNat 获取编译时信息的例子。但是感谢 GHC.TypeLits 中的其他函数，它也可以用于运行时信息。 只需将它添加到上面的代码中，然后试试。 main :: IO（） main = do i 让SomeNat = someNatVal i case someNat SomeNat（_ :: Proxy n） - >做让b :: Bar n b =酒吧hello！ print $ bar b 让我们来分析这里发生的事情。 从标准输入读取整数。 创建一个 SomeNat -typed值，如果输入是负值，则失败模式匹配。对于这样一个简单的例子来说，处理这个错误就会成为现实。 这是真正的魔力。使用 ScopedTypeVariables 与 case 表达式进行模式匹配，以绑定（静态未知） Nat -kinded类型转换为类型变量 n 。 最后，创建一个 Bar 值与该特定 n 作为其类型变量，然后对其进行处理。 I wonder if I can have my cake and eat it too regarding KnownNats. Can I write code that uses Nats that may be both KnownNats and UnknownNats (SomeNats?).For example if I have a dependently typed vector Vec (n :: Nat) a, can I write code that works both if the size is known at compile and at runtime? Thing is that I don't want to duplicate the whole code for statically and dynamically sized "things". And I don't want to lose static guarantees by storing sizes in the data structure.EditAnswer to András Kovács:My specific usecase is reading images from disk (which are luckily of fixed size) and then extracting patches from that, so basically I have a function extractPatch :: (KnownNat w2, KnownNat h2) => Image w1 h1 a -> Patch w2 h2 a where both Image and Patch are instances of a common Mat (w :: Nat) (h :: Nat) a type.If I wouldn't know the image size I would have to encode this in "runtime types". Just wondering. 解决方案 Here's something potentially interesting...{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}import GHC.TypeLitsimport Data.Proxydata Bar (n :: Nat) = Bar String deriving Showbar :: KnownNat n => Bar n -> (String, Integer)bar b@(Bar s) = (s, natVal b)Ok, it's very pointless. But it's an example of using KnownNat to get at compile-time information. But thanks to the other functions in GHC.TypeLits, it can be used with run-time information as well.Just add this on to the above code, and try it out.main :: IO ()main = do i <- readLn let Just someNat = someNatVal i case someNat of SomeNat (_ :: Proxy n) -> do let b :: Bar n b = Bar "hello!" print $ bar bLet's break down what happens here.Read an Integer from stdin.Create a SomeNat-typed value from it, failing the pattern-match if the input was negative. For such a simple example, handling that error just gets in the way.Here's the real magic. Pattern-match with a case expression, using ScopedTypeVariables to bind the (statically unknown) Nat-kinded type to the type variable n.Finally, create a Bar value with that particular n as its type variable and then do things with it. 这篇关于我可以有一个未知的KnownNat吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！ 上岸，阿里云！