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

В настоящее время я создаю упорядоченный векторный тип данных и пытаюсь создать операции из этого типа данных, но получаю сообщение об ошибке:

(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


operation typechecking agda
person SharkMangler    schedule 17.12.2015    source источник
comment
Ой, да, это была ошибка. Я починил, это должно быть заказано-????   -  person SharkMangler    schedule 17.12.2015

Ответы (1)


arrow_upward
2
arrow_downward

Во-первых, тип [_]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)
person Cactus    schedule 17.12.2015
comment
Понятно, я добавил в свой файл дополнительную информацию, а именно (_<A_ : A → A → ????), и я считаю, что это также вызывает проблемы с моим типом данных. Это проблема с операцией true () или где-то еще? - person SharkMangler; 17.12.2015
comment
Хотел бы я понять что-либо из этого. - person paulotorrens; 17.12.2015
comment
@SharkMangler И вообще, где это true определено? Конечно, это не может быть конструктор Bool из _3 _... может вы имели в виду T? У вас есть полная версия, которая действительно проверяет типы, если вы закомментируете определение [_]o????? - person Cactus; 17.12.2015
comment
@PauloTorrens не стесняйтесь задавать дополнительные вопросы (как новые)! - person Cactus; 17.12.2015
comment
что, если выбор A не параметрическим, повлияет на операцию [_] выключения? - person SharkMangler; 17.12.2015
comment
истинная операция - это операция типа bool-to-Set для быстрого исправления ошибки, которую я получал при определении свойства упорядоченного вектора. true : ???? → Set true tt = truth true ff = absurd - person SharkMangler; 17.12.2015
comment
Если вы привязываете A на уровне модуля, это означает, что он будет одинаковым A везде внутри модуля, поэтому вы не можете выбрать что-то другое для A в [_]o????. Для интуиции вы также можете подумать о том, где появилось бы определение _<A_, если бы [_]o???? было разрешено изменить выбор _7 _... - person Cactus; 17.12.2015
comment
@SharkMangler, который true доступен в стандартной библиотеке как Data.Bool.T FYI. Кроме того, разве вам не понадобится от _<A_ больше, чем просто случайная двоичная логическая функция? Откуда вы планируете получить этот true (min <A head) аргумент для `_ :: _`? - person Cactus; 17.12.2015
comment
Не следует ли просто изменить A на что-то вроде B в определении [_]o???? исправить это? Спасибо за помощь. Агду очень сложно понять! - person SharkMangler; 17.12.2015
comment
Я не использую стандартную библиотеку для своего класса. Такого модуля не было. Я считаю, что для своего класса они тестируют только натуральные числа, но я должен предоставить упорядоченный вектор для всех наборов, поскольку он выходит за рамки моих текущих возможностей для таких вещей. - person SharkMangler; 17.12.2015
comment
Итак, либо у вас есть определение ordered-???? параметрический в выборе A и _<A_, либо вам нужно исправить их (но это исправление может исходить из параметра более высокого уровня, в вашем случае модуль параметр). - person Cactus; 17.12.2015
comment
@SharkMangler, если вы не используете стандартную библиотеку, то этот вопрос можно закрыть как не по теме, потому что он не содержит всего необходимого кода, поскольку вы никогда не определяли _1 _... - person Cactus; 17.12.2015
comment
Помогло бы определение ℕ? Новое в правилах stackoverflow. - person SharkMangler; 17.12.2015
comment
Идеальной версией вашего вопроса была бы такая, в которой у вас есть весь код, необходимый для проверки типов, а затем у вас есть определение единственной функции, с которой у вас есть проблемы. Я заполнял пробелы, предполагая, что ваш ℕ - это тот, что был от Data.Nat, и, откровенно говоря, игнорировал материал true, потому что это был единственный способ добиться прогресса. - person Cactus; 17.12.2015