アガダのHaskell導出機構

Question

アガダには、Haskellのderiving Eq節に似たものがあれば、私は以下の関連する質問もあります。例えば

、私はおもちゃ-言語の種類があると、

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 

悲しいことに、これはうまくいきません。私は持ち上げてこれを修正しようとしましたが、私はレベル持ち上げを使う方法の手がかりがないので失敗しました。どんな助けもありがとう！私をhumouringため

上記の関数の使用例は次のようになり、

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

お礼を！

Answer 1

A Cosmology of Datatypesの「7.3.2。データ型の操作の実行」の章では、説明を使用して操作を導出する方法を示しています。けれども、導かれたEqはかなり弱いです。

基本的な考え方は、何らかの1次エンコーディング、つまりいくつかの汎用データ型を使用してデータ型を表現し、このデータ型に対して操作を定義することで、これらの汎用操作。私はこの機械の簡単なバージョンhereを精緻化しました。

閉じたユニバースを使用している場合は、より強い値のEqを派生させることができます。同様の表現方法（等しく表現しなければならないが、私はチェックしなかった）と閉鎖された宇宙を使用して、汎用のshowhereと定義した。 VecがDescデータ型に類似の用語で定義されて

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 

：あなたはコンストラクタに名前を付けた後、タプルのベクトルを印刷します。 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)は「更新」ℓです。

Answer 2

Agdaで「Eqの導出」を実際に実装するには、Ulfのagda-prelude（https://github.com/UlfNorell/agda-prelude）を参照してください。特に、Tactic.Deriving.Eqモジュールには、（一般的なクラスの）単純なデータ型に対して、決定可能な等価性を自動的に生成するためのコードが含まれています。