Haskell类型级别文字Nat:状态？
GHC具有类型级别的文字Nats。例如，我可以在这里读到一些关于它们的东西：
https://ghc.haskell.org/trac/ghc/wiki/TypeNats
不幸的是，关于它们的文档似乎很少，我尝试用它们做的几乎没有任何实际有效的方法。
来自this page的注释18提到了这个大小参数化的Vecs的简单示例(我添加了语言编译指示和一个导入语句)：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n+1) a
(+++) :: Vec n a -> Vec m a -> Vec (n+m) a
Nil +++ bs = bs
(a :> as) +++ bs = a :> (as +++ bs)它当时不能工作，但后来应该修改了实现，这样它就能工作了。那是5年前的事了。但它在我的GHC 7.10.1上不起作用：
trash.hs:15:20:
Could not deduce ((n + m) ~ ((n1 + m) + 1))
from the context (n ~ (n1 + 1))
bound by a pattern with constructor
:> :: forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a,
in an equation for ‘+++’
at trash.hs:15:2-8
NB: ‘+’ is a type function, and may not be injective
Expected type: Vec (n + m) a
Actual type: Vec ((n1 + m) + 1) a
Relevant bindings include
bs :: Vec m a (bound at trash.hs:15:15)
as :: Vec n1 a (bound at trash.hs:15:7)
(+++) :: Vec n a -> Vec m a -> Vec (n + m) a
(bound at trash.hs:14:1)
In the expression: a :> (as +++ bs)
In an equation for ‘+++’: (a :> as) +++ bs = a :> (as +++ bs)这是怎么回事？类型级别的文字Nats应该对这种事情有用吗？如果是，我该如何实现(+++)函数？如果不是，它们的用例是什么？
回答 1
Stack Overflow用户
发布于 2015-10-29 05:23:01
正如评论者所提到的，类型检查器目前无法履行这个等式，因为它们需要代数。虽然你和我都知道n + m = n1 + m + 1给了n = n1 + 1，但没有人教过GHC类型检查器如何执行这种算术。在Ada、Idris或Coq这样的语言中，你可以教编译器这些规则，或者算术规则可以在库中提供给你，但在Haskell中，类型检查器有点僵化(但在我看来，对现实世界的编程来说要友好得多)，不幸的是，你不得不求助于类型检查器插件。
据我所知，在这个问题上最积极的人是one Iavor Diatchki。这篇论文就在愚蠢的ACM付费墙后面，但你可以找到他的Haskell Symposium 2015 talk here on YouTube --它解释得很好！他的演讲使用了与您相同的示例，即一直流行的向量。His branch in the GHC repository致力于将其合并到主线GHC中，但据我所知还没有设定日期。现在你不得不使用typechecker插件，这并不是很糟糕。毕竟，最初的goal of Plugins/Typechecker是为了支持像这样有趣的工作，而不必将所有内容都合并到源代码中。对于模块化来说，这是有道理的！
https://stackoverflow.com/questions/31918427
复制相似问题