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

Question

关于KnownNats，我想知道我是否也可以吃蛋糕。 .我可以编写使用 Nats 的代码吗？可能都是KnownNats和 UnknownNats (SomeNats？)。

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

编辑

对安德拉斯·科瓦奇的回答:

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

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

Answer 1

这里有一些可能很有趣的东西......

{-# 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 中的其他功能，它也可以与运行时信息一起使用。

只需将其添加到上面的代码中，然后尝试一下。

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

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

阅读 Integer从标准输入。

创建 SomeNat -typed 值，如果输入为负数，则模式匹配失败。对于这样一个简单的示例，处理该错误只会妨碍您。

这是真正的魔力。模式匹配 case表达式，使用 ScopedTypeVariables绑定(bind)(静态未知)Nat -kinded 类型到类型变量 n .

最后，创建一个 Bar具有特定 n 的值作为它的类型变量，然后用它做事。