I am wondering if there is anything in Agda that resembles Haskell's deriving Eq clause ---then I have an associated question below, as well.
For example, suppose I have types for a toy-language,
data Type : Set where
Nat : Type
Prp : Type
Then I can implement decidable equality by pattern matching and C-c C-a,
_≟ₜ_ : Decidable {A = Type} _≡_
Nat ≟ₜ Nat = yes refl
Nat ≟ₜ Prp = no (λ ())
Prp ≟ₜ Nat = no (λ ())
Prp ≟ₜ Prp = yes refl
I'm curious if this can be mechanised or automated somehow similar to the manner it is done in Haskell:
data Type = Nat | Prp deriving Eq
Thank-you!
While we're on the topic of types, I'd like to realise my formal types as Agda types: Nat is just natural numbers while Prp is small propositions.
⟦_⟧Type : Type → Set ?
⟦ Nat ⟧Type = ℕ
⟦ Prp ⟧Type = Set
Sadly this does not work. I tried to fix this with lifting but failed since I haven't a clue on how to use level lifting. Any help is appreciated!
An example usage of the above function would be,
record InterpretedFunctionSymbol : Set where
field
arity : ℕ
src tgt : Type
reify : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type
Thank-you for humouring me!
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.
