Haskell 类型级别文字 Nat: status?

Question

GHC 具有类型级别的字面量 Nats。例如，我可以在这里阅读一些关于它们的信息：

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

不幸的是，关于它们的文档似乎很少，而且我尝试对它们做的几乎所有事情都没有真正起作用。

this page 的评论 18 提到了这个大小参数化 Vecs 的简单示例（我添加了 LANGUAGE pragma 和 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 中，类型检查器更加严格（但更友好）到现实世界的编程，在我看来），不幸的是你不得不求助于类型检查器插件。

我认识的最积极解决这个问题的人是Iavor Diatchki。那篇论文在愚蠢的 ACM 付费墙后面，但你可以找到他的 Haskell Symposium 2015 talk here on YouTube — 解释得很好！他的演讲使用了与您相同的例子，即广受欢迎的向量。 His branch in the GHC repository 致力于将其合并到主线 GHC 中，但据我所知，没有设置日期。现在你必须使用 typechecker 插件，这还不错。毕竟，最初的goal of Plugins/Typechecker 是为了实现这样有趣的工作，而无需将所有内容合并到源代码中。模块化有话要说！