我正在阅读Dependent Types at Work。在参数化类型的介绍中,作者提到在这个声明中:
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
List
的类型是 Set → Set
,而 A
成为这两个构造函数的隐式参数,即:
List
的类型是 Set → Set
,并且 A
成为这两个构造函数的默认参数。
[] : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A
好的,我试着以稍微不同的方式重写它。
data List : Set → Set where
[] : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A
很遗憾,这并不起作用(我尝试学习Agda已经两天左右了,但根据我所了解的,这是因为构造函数参数化在Set₀
上,因此List A
必须在Set₁
中)。
事实上,以下内容被接受:
data List : Set₀ → Set₁ where
[] : {A : Set₀} → List A
_::_ : {A : Set₀} → A → List A → List A
然而,我不再能使用{A : Set} → ... → List (List A)
(这是完全可以理解的)。
所以我的问题是:List (A : Set) : Set
和List : Set → Set
之间的实际区别是什么?
感谢您的时间!
List
定义为Set → Set
以防止类型系统不一致,那么是什么机制使得List (A : Set) : Set
“起作用”?因为对我来说(来自Haskell背景),它们两个似乎都是data List :: * -> * where (...)
,但一个有效而另一个无效。谢谢! - Vitus