Механизм получения Haskell для Agda

Мне интересно, есть ли в Agda что-нибудь похожее на предложение deriving Eq в Haskell - тогда у меня также есть связанный вопрос ниже.

Например, предположим, что у меня есть типы для игрушечного языка,

data Type : Set where
  Nat  : Type
  Prp : Type

Затем я могу реализовать разрешимое равенство путем сопоставления с образцом и C-c C-a,

_≟ₜ_ : Decidable {A = Type} _≡_
Nat ≟ₜ Nat = yes refl
Nat ≟ₜ Prp = no (λ ())
Prp ≟ₜ Nat = no (λ ())
Prp ≟ₜ Prp = yes refl

Мне любопытно, можно ли это механизировать или автоматизировать каким-то образом подобно тому, как это делается в Haskell:

data Type = Nat | Prp deriving Eq

Спасибо!

Пока мы говорим о типах, я хотел бы реализовать свои формальные типы как типы Agda: Nat - это просто натуральные числа, а Prp - это небольшие предложения.

⟦_⟧Type : Type → Set ?
⟦ Nat ⟧Type = ℕ
⟦ Prp ⟧Type = Set

К сожалению, это не работает. Я пытался исправить это с помощью подъема, но у меня ничего не вышло, так как я понятия не имел, как использовать подъем по уровню. Любая помощь приветствуется!

Пример использования вышеуказанной функции:

record InterpretedFunctionSymbol : Set where
  field
   arity   : ℕ
   src tgt : Type
   reify   : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type

Спасибо, что потешили меня!


signature haskell agda
person Musa Al-hassy    schedule 24.03.2016    source источник

Ответы (2)


arrow_upward
7
arrow_downward

Глава «7.3.2. Получение операций по типам данных» в Космология типов данных показывает, как выводить операции с помощью описаний. Хотя производный Eq там слабоват.

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

Вы можете получить более сильную Eq, если у вас замкнутая вселенная. Используя подход, аналогичный описанию (должен быть одинаково выразительным, но я не проверял) и закрытую вселенную, я определил общий show здесь, что позволяет, например, чтобы напечатать вектор кортежей после того, как вы назовете конструкторы:

instance
  named-vec : {A : Type} -> Named (vec-cs A)
  named-vec = record { names = "nil" ∷ "cons" ∷ [] }

test₂ : show (Vec (nat & nat) 3 ∋ (7 , 8) ∷ᵥ (9 , 10) ∷ᵥ (11 , 12) ∷ᵥ []ᵥ)
      ≡ "(cons 2 (7 , 8) (cons 1 (9 , 10) (cons 0 (11 , 12) nil)))"
test₂ = prefl

где Vec определяется в терминах типа данных, аналогичных Desc. Случай Eq должен быть похожим, но более сложным.

Вот как можно использовать Lift:

⟦_⟧Type : Type → Set₁
⟦ Nat ⟧Type = Lift ℕ
⟦ Prp ⟧Type = Set

ex₁ : ∀ A -> ⟦ A ⟧Type
ex₁ Nat = lift 0
ex₁ Prp = ℕ

ex₂ : ∀ A -> ⟦ A ⟧Type -> Maybe ℕ
ex₂ Nat n = just (lower n) -- or (ex₂ Nat (lift n) = just n)
ex₂ Prp t = nothing

Если A : Set α, то Lift A : Set (α ⊔ ℓ) для любого ℓ. Итак, когда у вас есть ℕ : Set и Set : Set₁, вы хотите поднять ℕ с Set до Set₁, что составляет всего Lift ℕ - в простых случаях вам не нужно явно указывать ℓ.

Чтобы создать элемент типа данных, заключенный в Lift, вы используете lift (как в lift 0). И чтобы вернуть этот элемент, вы используете lower, поэтому lift и lower противоположны друг другу. Однако обратите внимание, что lift (lower x) не обязательно находится в той же вселенной, что и x, потому что lift (lower x) «обновляет» ℓ.

ОБНОВЛЕНИЕ: ссылка show сейчас не работает (мне следовало использовать постоянную ссылку). Но теперь есть лучший пример: целая библиотека, производная Eq для обычных типов данных Agda.

person user3237465    schedule 25.03.2016
comment
Большое Вам спасибо; Я с нетерпением жду возможности прочитать процитированную диссертацию и процитированный блог ^ _ ^ - person Musa Al-hassy; 28.03.2016

arrow_upward
2
arrow_downward

Для практической реализации «получения Eq» в Agda вы можете взглянуть на agda-prelude Ульфа по адресу https://github.com/UlfNorell/agda-prelude. В частности, модуль Tactic.Deriving.Eq содержит код для автоматической генерации разрешимого равенства для довольно общего класса (простых и индексированных) типов данных.

person Jesper    schedule 25.03.2016
comment
Может ли он получить Eq (Vec A n), имеющий Eq A в области видимости? - person user3237465; 25.03.2016