我可以有一个未知的KnownNat吗？ [英] Can I have an unknown KnownNat?

问题描述

我不知道我是否可以吃我的蛋糕，也可以吃 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）一个类型。

如果我不知道图像大小，我将不得不在运行时类型中对其进行编码。只是想知道。

解决方案

<$ p $ b $ { - ＃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 < -  readLn 
让SomeNat = someNatVal i 
 case someNat 
 SomeNat（_ :: Proxy n） - >做
让b :: Bar n 
 b =酒吧hello！ 
 print $ bar b 
  

让我们来分析这里发生的事情。

1. 从标准输入读取整数。
   
2. 创建一个 SomeNat -typed值，如果输入是负值，则失败模式匹配。对于这样一个简单的例子来说，处理这个错误就会成为现实。


3. 这是真正的魔力。使用 ScopedTypeVariables 与 case 表达式进行模式匹配，以绑定（静态未知） Nat -kinded类型转换为类型变量 n 。


4. 最后，创建一个 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.

Edit

Answer 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.TypeLits
import Data.Proxy

data Bar (n :: Nat) = Bar String deriving Show

bar :: 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 b

Let's break down what happens here.

1. Read an Integer from stdin.
2. 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.
3. 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.
4. Finally, create a Bar value with that particular n as its type variable and then do things with it.

这篇关于我可以有一个未知的KnownNat吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！