在Haskell中,如何将整数转换为n等于整数的代理(n::KnownNat)?

一般来说,你不能。a的含义 KnownNat n 约束条件是 n 是类型级自然数 使用编译时已知的值 . 一个 Integer 表示已知的整数值 运行时 ,它可能会受到运行时才知道的各种因素的影响(例如用户输入、随机性、文件系统的状态、访问数据库、从文件系统中读取等)。

目的 Data.Vector.Sized 是为了表演 编译时 边界检查,当然,如果不知道编译时的大小,就不能执行这些检查。一旦你有了 整数 ,无法神奇地将其转换为 Nat 因为这需要在编译时预测它最终在运行时所拥有的值,而事实上,它甚至不可能每次都是相同的值。

根据你想做什么,可能有多种方法来编码你想要的。例如,您可以使用 packFinite 要在运行时生成整数在给定范围内的证据,可以使用 knownLength 在未知大小的向量上运行计算,但这两种方法都不允许您对 纳特 从一个 整数 ,他们只是说服他们键入system,在 整数 实际上超出了你承诺的范围。