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

Question

Idris文档中有以下行：

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回购，发现：

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

它与Vect的类型声明有相似的模式，所以看起来很好。但是我在源代码中找不到CCD_ 1。此外，我找不到Vect的类型定义。

所以，我的困惑是：

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

Answer 1

没有单独的"类型定义"；以及"；类型声明"；在伊德里斯；这只是编写类型定义的两种方法。参见语法指南：

Idris提供了两种用于定义数据类型的语法。第一个是Haskell风格的语法，定义了一个正则代数数据类型。。。

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

GADT由Haskell介绍，阅读例如。https://en.wikibooks.org/wiki/Haskell/GADT或者搜索GADT可以为您提供第二种风格的额外解释。

除了允许命名elem、x和data List a = Nil | (::) a (List a)0之外，List的GADT样式定义等效于data List a = ...。