如何理解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 provides two kinds of syntax for defining data types. The first, Haskell style syntax, defines a regular algebraic data type...

The second, more general kind of data type, is defined using Agda or GADT style syntax. This syntax defines a data type that is parameterised by some values (in the Vect example, a value of type Nat and a value of type Type).

GADT 由 Haskell 引入，阅读例如https://en.wikibooks.org/wiki/Haskell/GADT 或搜索 GADT 可以为您提供第二种样式的额外说明。

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

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

How to understand the type declaration and definition for List and Vect in Idris lang?

types

programming-languages

dependent-type

idris