Agda 中列表的定义

Question

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

我很难理解最后一行。前段时间学习了一些Haskell，所以对cons运算符比较熟悉。

因此，要么你有一个类型为 List A 的空列表，要么你使用类型为 A -> List A -> List A 的函数 :: 创建一个新值，它采用一些元素类型 A 和类型列表 A 和 returns 新列表？

这似乎是直觉，但这并不映射到我所知道的递归数据类型定义的概念（来自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

Definition of List in Agda