Haskell Deriving Mechanism for Agda

The "7.3.2. Deriving operations on datatypes" chapter of A Cosmology of Datatypes shows how to derive operations using descriptions. Though, the derived Eq is rather weak there.

The basic idea is to represent data types using some first-order encoding, i.e. in terms of some generic data type, and define operations on this data type, so everything encoded in terms of it can be handled by these generic operations. I elaborated a simple version of this machinery here.

You can derive a stronger Eq, if you have a closed universe. Using a similar to descriptions approach (should be equally expressive, but I didn't check) and a closed universe I defined generic show here, which allows e.g. to print a vector of tuples after you name the constructors:

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

where Vec is defined in terms of a similar to Desc data type. The Eq case should be similar, but more sophisticated.

Here is how Lift can be used:

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

If A : Set α then Lift A : Set (α ⊔ ℓ) for any ℓ. So when you have ℕ : Set and Set : Set₁, you want to lift ℕ from Set to Set₁, which is just Lift ℕ — in simple cases you don't need to provide ℓ explicitly.

To construct an element of a data type wrapped in Lift you use lift (like in lift 0). And to get this element back you use lower, so lift and lower are inverses of each other. Note though that lift (lower x) doesn't necessarily lie in the same universe as x, because lift (lower x) "refreshes" ℓ.

UPDATE: the show link is broken now (I should have used a permalink). But there is a better example now: an entire library that derives Eq for regular Agda data types.

For a practical implementation of "deriving Eq" in Agda, you can take a look at Ulf's agda-prelude at https://github.com/UlfNorell/agda-prelude. In particular, the module Tactic.Deriving.Eq contains code for automatically generating decidable equality for a quite general class of (simple and indexed) data types.