Haskell Ableitungsmechanismus für Agda

Question

Ich frage mich, ob es in Agda irgendetwas gibt, das Haskells deriving Eq-Klausel ähnelt --- dann habe ich eine zugehörige Frage unten, ebenso.

Beispiel: Angenommen, ich habe Typen für eine Spielzeug-Sprache,

data Type : Set where 
    Nat : Type 
    Prp : Type 

Dann kann ich entscheidbar Gleichheit durch Mustervergleich und C-c C-a,

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

implementieren Ich bin gespannt, ob dies kann ähnlich der Art und Weise, wie es in Haskell gemacht wird, mechanisiert oder automatisiert zu sein:

data Type = Nat | Prp deriving Eq 

Vielen Dank!

Während wir auf das Thema Arten sind, würde ich gerne meine formalen Typen als Agda-Typen realisieren: Nat ist nur natürliche Zahlen, während Prp kleine Vorschläge ist.

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

Leider funktioniert das nicht. Ich habe versucht, dies mit dem Heben zu beheben, aber es ist fehlgeschlagen, da ich keine Ahnung habe, wie man mit dem Heben von Höhen arbeitet. Jede Hilfe wird geschätzt!

Ein Beispiel für die Verwendung der obigen Funktion wäre,

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

Dankes- mich für humouring!

Answer 1

Das Kapitel "7.3.2. Ableiten von Operationen mit Datentypen" von A Cosmology of Datatypes zeigt, wie Sie Operationen mithilfe von Beschreibungen ableiten können. Allerdings ist das abgeleitete dort eher schwach.

Die Grundidee besteht darin, Datentypen unter Verwendung einiger Kodierungen erster Ordnung, dh in Form eines generischen Datentyps, darzustellen und Operationen für diesen Datentyp zu definieren, so dass alles, was davon kodiert wird, von diesen generischen Operationen gehandhabt werden kann . Ich habe eine einfache Version dieser Maschine ausgearbeitet here.

Sie können eine stärkere Eq ableiten, wenn Sie ein geschlossenes Universum haben. Mit einer ähnlichen Beschreibungen Ansatz (sollte gleichermaßen ausdrucksvoll sein, aber ich habe nicht überprüft) und ein geschlossenes Universum ich definierte generische showhere, die z. einen Vektor von Tupeln zu drucken, nachdem Sie die Konstruktoren Name:

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 

wo Vec in Bezug auf eine ähnliche Desc Datentyp definiert ist. Der Fall Eq sollte ähnlich, aber ausgeklügelter sein.

Hier ist, wie Lift verwendet werden können:

⟦_⟧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 

Wenn A : Set α dann Lift A : Set (α ⊔ ℓ) für jede ℓ. Wenn Sie also ℕ : Set und Set : Set₁ haben, möchten Sie ℕ von Set auf Set₁ heben, was nur Lift ℕ ist - in einfachen Fällen müssen Sie ℓ nicht explizit angeben.

Um ein Element eines Datentyps zu erstellen, der in Lift verpackt ist, verwenden Sie lift (wie in lift 0). Und um dieses Element zurück zu bekommen, benutzen Sie lower, also sind lift und lower Inversen von einander. Beachten Sie jedoch, dass lift (lower x) nicht unbedingt im selben Universum wie x liegt, weil lift (lower x) "aktualisiert" ℓ.

Answer 2

Für eine praktische Umsetzung von "Ableiten Eq" in Agda können Sie sich Ulfs Agda-Präludium bei https://github.com/UlfNorell/agda-prelude ansehen. Insbesondere enthält das Modul Tactic.Deriving.Eq Code zum automatischen Erzeugen einer entscheidbaren Gleichheit für eine ziemlich allgemeine Klasse von (einfachen und indizierten) Datentypen.