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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With