Haskell类型级文字Nat:状态？

Question

GHC具有类型级字面Nats.我可以阅读一些关于它们的内容,例如:

https://ghc.haskell.org/trac/ghc/wiki/TypeNats

不幸的是,似乎没有关于它们的文档,我尝试用它们几乎没有任何实际工作.

本页的评论18 提到了这个大小参数化Vecs的简单例子(我添加了LANGUAGE编译指示和一个import语句):

{-# 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应该可用于此类事情吗？如果是这样,我该如何实现(+++)函数？如果没有,他们的用例是什么？

Answer 1

正如评论者所提到的，类型检查器目前无法实现这种等式，因为它们需要代数。然而你和我都知道n + m = n1 + m + 1，n = n1 + 1没有人教过 GHC 类型检查器如何执行这种算术。在 Ada、Idris 或 Coq 等语言中，您可以教编译器这些规则，或者算术规则可能会在库中提供给您，但在 Haskell 中，类型检查器有点严格（但很多）在我看来，对现实世界的编程更友好）并且不幸的是你必须求助于类型检查器插件。

\n\n

据我所知，在这个问题上最积极的人是 I ​​avor Diatchki。这篇论文位于愚蠢的 ACM 付费墙后面，但您可以在 YouTube \xe2\x80\x94 上找到他在 Haskell Symposium 2015 上的演讲，解释得非常清楚！他的演讲使用了与你的相同的例子，即非常流行的向量。他在 GHC 存储库中的分支致力于将其合并到主线 GHC 中，但据我所知，还没有设定日期。现在你必须使用类型检查器插件，这还不错。毕竟，Plugins/Typechecker 的最初目标是实现这样有趣的工作，而不必将所有内容合并到源代码中。模块化是值得一提的！

\n