Agda定义Relation归纳类型时List Set不是合法类型的原因是什么？

问题核心原因 #

问题的本质是Agda对归纳数据类型的宇宙层级约束：你定义的Relation类型是A → Set，即它的每个实例都位于Set₀（最基础的类型宇宙）层级，因此它的所有构造子的参数类型的宇宙层级都不能超过Set₀。

两个map函数的本质差异 #

• map-2的返回类型是Set，不管输入是什么，它最终都会把列表里的所有元素用乘积类型拼接成一个单个的Set₀层级的类型，完全符合构造子参数的要求。
• map-1的返回类型是List Set：Set本身的类型是Set₁，因此List Set的宇宙层级是Set₁，高于Relation所处的Set₀，自然无法作为Set₀层级的构造子的参数类型。

为什么List Set在其他场景可以正常使用 #

你看到的合法用法都没有要求List Set成为Set₀层级的参数类型：

1. 定义map-1的时候，你只是把List Set作为函数的返回值，没有要求它适配Set₀的约束。
2. 定义HList的时候，List Set是作为类型索引使用，而非构造子的参数类型。HList的构造子的实际参数是A和HList xs，都属于Set₀层级，没有违反约束。

如果确实想要保留map-1的用法，只要把它的返回值包装成异构列表即可，修改expand构造子的类型如下：

expand : (a : A) → HList (map-1 Relation (relation-1 a)) → Relation a

此时HList (map-1 Relation (relation-1 a))的类型是Set₀，符合构造子参数的层级要求。

内容的提问来源于stack exchange，提问作者Theodora