Agda типа Проверка ошибок

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) 

Это нац модуль

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_ быть параметры для модуля, I думаю, что это совсем неправильный подход, и 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)