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

问题描述

关于KnownNats，我想知道我是否可以吃我的蛋糕.我可以编写使用 Nats 的代码，它们可能是 KnownNats 和 UnknownNats(SomeNats?).

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?).

例如，如果我有一个依赖类型的向量 Vec (n :: Nat) a，我可以编写在编译和运行时都知道大小的代码吗?问题是我不想为静态和动态大小的事物"复制整个代码.而且我不想通过在数据结构中存储大小而失去静态保证.

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.

回答安德拉斯·科瓦奇:

Answer to András Kovács:

我的具体用例是从磁盘读取图像(幸运的是固定大小)，然后从中提取补丁，所以基本上我有一个函数 extractPatch :: (KnownNat w2,KnownNat h2) =>图像 w1 h1 a ->补丁 w2 h2 a 其中 Image 和 Patch 都是公共 Mat (w :: Nat) (h :: Nat) 的实例代码>一种类型.

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)

好吧，这毫无意义.但这是使用 KnownNat 获取编译时信息的示例.但是由于 GHC.TypeLits 中的其他函数，它也可以与运行时信息一起使用.

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. 从标准输入读取 Integer.
2. 从中创建一个 SomeNat 类型的值，如果输入为负，则模式匹配失败.对于这样一个简单的示例，处理该错误只会成为障碍.
3. 这才是真正的魔法.使用 case 表达式进行模式匹配，使用 ScopedTypeVariables 将(静态未知的)Nat 类型绑定到类型变量 n.
4. 最后，创建一个 Bar 值，使用该特定的 n 作为它的类型变量，然后用它做一些事情.

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屋！