如何理解 Idris lang 中 List 和 Vect 的类型声明和定义？

Question

Idris doc 中有以下几行：

data List a = Nil | (::) a (List a)

data Vect : Nat -> Type -> Type where
   Nil  : Vect Z a
   (::) : a -> Vect k a -> Vect (S k) a

我假设第 1 行是 List 的类型定义，其余的是 Vect 的类型声明。 我认为应该有声明和定义，所以我查看了Idris repo 并发现：

data List : (elem : Type) -> Type where
  Nil : List elem
  (::) : (x : elem) -> (xs : List elem) -> List elem

这与 Vect 的类型声明具有相似的模式，所以看起来不错。但我在源代码中找不到data List a = Nil | (::) a (List a)。另外，我找不到 Vect 的类型定义。

所以，我的困惑是：

• 为什么我在源代码中找不到data List a = Nil | (::) a (List a)？
• Vect 的实际类型定义是什么？

Answer 1

Idris 中没有单独的“类型定义”和“类型声明”；这些只是编写类型定义的两种方法。见Syntax Guide：

Idris 提供了两种定义数据类型的语法。第一种是 Haskell 风格的语法，它定义了一个常规的代数数据类型……

第二种更通用的数据类型是使用 Agda 或 GADT 样式语法定义的。此语法定义了由某些值参数化的数据类型（在Vect 示例中，类型为Nat 的值和类型为Type 的值）。

GADT 是由 Haskell 引入的，例如阅读https://en.wikibooks.org/wiki/Haskell/GADT 或者搜索 GADT 可以给你更多关于第二种风格的解释。

除了允许命名elem、x 和xs 之外，List 的 GADT 样式定义等同于 data List a = ...。