types - Agda 中列表的定义

Question

在 Dependently Typed Programming in Agda 的第 4 页上, List 定义如下

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

我很难理解最后一行。之前学过一些 Haskell，所以对 cons 运算符比较熟悉。

因此，要么您有一个类型为 List A 的空列表，要么您使用类型为 A 的函数 :: 创建一个新值 -> 列表 A -> 列表 A，它采用 A 类型的一些元素和 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