Agda 中 List 的定义

Question

在 Agda 中的依赖类型编程的第 4 页上，List定义如下

infixr 40 _::_
data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

我很难将头环绕在最后一行。前阵子学过一些 Haskell，所以对cons运算符比较熟悉。

那么，要么你有一个空列表，它是 type List A，或者你创建一个带有::type函数的新值A -> List A -> List A，它接受一些 type 元素A和一个 type 列表A并返回一个新列表？

这似乎是直觉，但这并没有映射到我所知道的递归数据类型定义的概念（来自haskell），例如

data Tree a = Leaf a | Branch (Tree a) (Tree a)

问题那么这是一种什么样的类型呢？这里涉及到Agda的哪些概念？

Answer 1

在 Haskell 和 Agda 中有两种定义数据类型的语法。

简单一：

data List a = Nil | a :# List a

更有表现力的一个（在 Haskell 中它用于定义GADTs）：

{-# LANGUAGE GADTs #-}
data List a where
    Nil :: List a
    (:#) :: a -> List a -> List a