Haskell issuing mechanism for Agda

Question

I am wondering if there is anything in Agda similar to the Haskell deriving Eq suggestion --- then I have a related question below.

For example, suppose I have types for a toy language,

 data Type : Set where Nat : Type Prp : Type 

Then I can implement solvable equality by matching with the sample and Cc Ca ,

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

I am curious if this can be mechanized or automatic in some way similar to how this is done in Haskell:

 data Type = Nat | Prp deriving Eq 

Thank you!

While we are talking about types, I would like to implement my formal types as Agda types: Nat are just natural numbers, and Prp are small sentences.

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

Unfortunately this will not work. I tried to fix this with a lift, but I couldn’t, because I don’t know how to use a level rise. Any help is appreciated!

An example of using the above function would be,

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

Thank you for courting me!

Answer 1

The chapter "7.3.2. Deriving Derivatives by Data Types" "Cosmology of Data Types" shows how to output operations using descriptions. Although, the resulting Eq rather weak.

The main idea is to represent data types using some first-order encoding, that is, in terms of some general data type, and to define operations on this data type, so everything encoded in terms of this can be processed by these generic operations. I developed a simple version of this mechanism here .

You can get a stronger Eq if you have a closed universe. Using an approach similar to the description (it should be equally expressive, but I didn’t check it) and the closed universe, I defined a general show here , which allows, for example, to print the vector of tuples after the name of 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 defined in terms of a data type of type Desc . The case of Eq should be similar, but more complex.

Here's how to use 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 

If A : Set α , then Lift A : Set (α ⊔ ℓ) for any ℓ . Therefore, when you have ℕ : Set and Set : Set₁ , you want to raise ℕ from Set to Set₁ , which is just Lift ℕ - in simple cases you do not need to explicitly specify ℓ .

To create a data type element wrapped in Lift , you use Lift (for example, in lift 0 ). And to return this element, use lower , so Lift and lower are inverse to each other. Note that lift (lower x) does not necessarily lie in the same universe as x , because lift (lower x) “updates” ℓ .

Answer 2

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