haskell - 避免对类型级别自然的类约束

Question

我正在使用 Nat 模块中的 GHC.TypeLits 类型，它诚然表示程序员接口(interface)应该在单独的库中定义。在任何情况下， GHC.TypeLits 都有一个类 KnownNat 和一个类函数 natVal ，它将编译时间 Nat 转换为运行时 Integer 。还有一个类型函数 (+) ，它增加了编译时间 Nat 秒。

问题是给定 (KnownNat n1, KnownNat n2) ，GHC 无法推导出 KnownNat (n1 + n2) 。

这导致每当我添加类型级别的自然属性时，都需要添加大量的约束。

一种替代方法是自己定义自然数，如下所示:

data Nat = Zero | Succ Nat

或者也许使用像 type-natural 这样的库。但是不使用 GHC 中内置的 Nats 似乎很愚蠢，它还允许您在类型中很好地使用文字数字(即 0 、 1 )，而不必定义:

N0 = Zero
N1 = Succ N0
etc...

无论如何，这个问题是否到处都需要 GHC KnownNat 约束？还是我应该忽略 GHC.TypeLits 模块来解决我的问题？

Answer 1

这个 GHC 类型检查器插件正是这样做的(派生“复杂”KnownNat 来自其他可用的约束):https://hackage.haskell.org/package/ghc-typelits-knownnat

如果“类型检查器插件”听起来有点吓人(起初对我来说是这样)，它实际上使用起来非常简单。只需将它作为依赖项添加到您的包文件中(或 cabal 安装它)，就像任何其他包一样，然后添加:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

到源文件的开头(很像 LANGUAGE pragma)，或将其作为选项全局添加到包文件中。

同一作者还有另一个插件，对于使用 typelit Nats 也非常有用: https://hackage.haskell.org/package/ghc-typelits-natnormalise .这个能够推断 GHC 自己放弃的 Nat 类型表达式的相等性:像 n + (m + 1) ~ (n + 1) + m 这样的东西当 GHC 试图证明“预期”和“实际”类型匹配时，就会出现这种情况。