阿格达类型检查错误

Question

我目前正在有序矢量数据类型，我试图创建从数据类型的操作，但我得到一个错误：

(Set (.Agda.Primitive.lsuc ℓ)) != Set 
when checking that the expression A has type Set ℓ 

这是数据类型

module ordered-vector (A : Set) (_<A_ : A → A →) where 

data ordered- : {A : Set}→ A → ℕ → Set where 
     [] : {a : A} → ordered- a 0 
     _::_ : (head : A) {min : A} → {n : ℕ} → (tail : ordered- min n) → true (min <A head) → ordered- head (suc n) 

这是操作：

[_]o : ∀ {ℓ} {A : Set ℓ} → A → ordered- A 1 
[ x ]o = x :: [] 

我相信下面的代码是数据类型更正确。我如何保留定义的缺点的正确性？

data ordered- {ℓ} (A : Set ℓ) : ℕ → Set ℓ where 
    [] : ordered- A 0 
    _::_ : (head : A) {min : A} → {n : ℕ} → ordered- min n → true (min <A head) → ordered- head (suc n) 

这是NAT模块

http://lpaste.net/147233

Answer 1

首先的[_]o类型没有太大的意义，因为你正在传递参数的类型（类型为x）作为ordered-的索引;我相信你正在尝试做

[_]o : ∀ {ℓ} {A : Set ℓ} → (a : A) → ordered- a 1 

改为。

如果相应改变的[_]o的类型，你仍然会得到错误信息

(Set ℓ) != Set 
when checking that the expression a has type A 

，这是因为你的[_]o尝试的定义为电平多态的，但你的ordered-定义是不。

您可以让[_]o “笨”：

[_]o : ∀ {A : Set} → (a : A) → ordered a 1 
[ x ]o = x ∷ [] 

或使ordered- “聪明”：

data ordered- {ℓ} {A : Set ℓ} : A → ℕ → Set ℓ where 
    [] : {a : A} → ordered- a 0 
    _∷_ : (head : A) {min : A} → {n : ℕ} → (tail : ordered- min n) → true (min <A head) → ordered- head (suc n) 

但是，如果你想A和_<A_是参数，你的模块，我认为这是完全错误的做法，并ordered-应该根本就不会在选择A在所有参数：

module ordered-vector (A : Set) (_<A_ : A → A →) where 
    data ordered- : A → ℕ → Set where 
    [] : {a : A} → ordered- a 0 
    _∷_ : (head : A) {min : A} → {n : ℕ} → (tail : ordered- min n) → true (min <A head) → ordered- head (suc n)