避免类型级自然的类约束

我正在使用模块中的Nat类型GHC.TypeLits,无可否认地说程序员接口应该在一个单独的库中定义.在任何情况下,GHC.TypeLits都有一个KnownNat带有类函数的类,natVal它将编译时Nat转换为运行时Integer.还有一个类型函数(+)可以增加编译时间Nat.

问题在于(KnownNat n1, KnownNat n2),GHC无法得出这一点KnownNat (n1 + n2).

每当我添加类型级别自然时,这都会导致需要添加的约束爆炸.

另一种方法是自己定义自然数字,如下所示:

data Nat = Zero | Succ Nat

或者使用类似自然的库.但似乎傻不使用其内置的GHC纳茨,这也可以让您很好的类型使用文字数字(即0,1),而不必定义:

N0 = Zero
N1 = Succ N0
etc...

围绕这个问题是否存在GHC KnownNat限制在整个地方都需要？或者我应该忽略GHC.TypeLits我的问题的模块？

这个GHC类型检查器插件正是这样做的(KnownNat从已经可用的其他约束中获得"复杂" 约束):https://hackage.haskell.org/package/ghc-typelits-knownnat

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

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

到源文件的开头(很像一个LANGUAGEpragma),或者在包文件中全局添加它作为选项.

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