在 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 -> 列表 AA
类型的一些元素和 A
类型的列表并返回一个新列表?
这似乎是直觉,但这并不映射到我所知道的递归数据类型定义的概念(来自 haskell),例如
data Tree a = Leaf a | Branch (Tree a) (Tree a)
问题 那么这是什么类型的呢?这里涉及到 Agda 的哪些概念?
最佳答案
在 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
关于types - Agda 中列表的定义,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/44067718/