List Set 应该是一种排序，但它不是答案

【问题标题】：List Set should be a sort, but it isn'tList Set 应该是一种排序，但它不是
【发布时间】：2021-09-28 10:26:29
【问题描述】：

我刚刚开始使用 Agda 进行一些概念验证。

在这种情况下，我想要一个与下面定义的Relation 具有相似结构的数据类型。

（为简单起见，省略了数据类型A的元素和函数relation-1的定义）。

Relation 定义如下：

open import Data.Product using (_×_)
open import Data.List using (List; _∷_; [])
open import Data.Unit using (⊤)

data A : Set where

relation-1 : A → List A
relation-1 = {!!} 

map-1 : ∀{A : Set} → (A → Set) → List A → List Set
map-1 _ [] = []
map-1 p (a ∷ as) = p a ∷ (map-1 p as) 

map-2 : ∀{A : Set} → (A → Set) → List A → Set
map-2 p [] = ⊤
map-2 p (a ∷ as) = p a × (map-2 p as)

data Relation : A → Set where 
  refl : (a : A) → Relation a
  expand : (a : A) → map-1 Relation (relation-1 a) → Relation a

错误信息是：

List Set should be a sort, but it isn't
when checking that the inferred type of an application
  List Set
matches the expected type
  _43

但是，在将 map-1 替换为 map-2 之后

data Relation : A → Set where 
  refl : (a : A) → Relation a
  expand : (a : A) → map-2 Relation (relation-1 a) → Relation a

不会有类型错误。

我的问题是，当map-1 用于Relation 时，为什么List Set 不是有效类型？

它在map-1 的定义和其他情况下效果很好，例如在异构列表中：

data HList : (List Set) → Set where
  [] : HList []
  _∷_ : {A : Set}{xs : List Set} → A → HList xs → HList (A ∷ xs)

【问题讨论】：

我知道map-1 Relation (relation-1 a) 是一个排序元素List Set，如果relation-1 a 给出[a1, a2, a3]，map-1 Relation (relation-1 a) 将给出Relation a1 :: Relation a2 :: Relation a3 :: []。同样，map-2 Relation (relation-1 a) 给出了Relation a1 x (Relation a2 x Relation a3) 和它的一个元素Set，但是为什么后者在这里是可以接受的呢？是不是因为:: 不是某种类型的构造函数，所以很难为Relation a1 :: Relation a2 :: Relation a3 :: [] 提供证据？
map-1 Relation (relation-1 a) : List Set，所以它的值是一个特定的集合列表，假设列表[A, B] 其中A 和B 是一些具体的Sets。那么你的expand 类型说它的第二个参数应该是[A, B] 类型的东西，但这并不意味着什么......
（删除了我的错误答案）请注意map-1 和map-2 之间的细微差别：map-2 用于空列表生成类型T，您始终可以在其中构建见证；但是 map-1 在这个宇宙中是一个空的类型列表。即使后者意味着一种类型，“空类型列表”的值是什么？
@SassaNF 是的，你是对的。 '::' 是一个值构造函数，因此 List Set 的元素由 Set0 的类型组成，但是，这些元素是原始常量，只能用作索引或类型级别的函数，例如在 HList 或 map-1 中。而 'x' 是一个类型构造函数，其元素的结构是定义良好的原始常量。

标签： agda

【解决方案1】：

我想要的只是 All 这里： https://plfa.github.io/Lists/#21511

【讨论】：