Generic
It's a library for doing generic programming in Agda.
The library is tested with Agda-2.6.1 and Agda-2.6.1.2 and likely does not work with other versions of Agda.
A quick taste
Deriving decidable equality for vectors:
open import Data.Vec using (Vec) renaming ([] to []ᵥ; _∷_ to _∷ᵥ_)
instance VecEq : ∀ {n α} {A : Set α} {{aEq : Eq A}} -> Eq (Vec A n)
unquoteDef VecEq = deriveEqTo VecEq (quote Vec)
xs : Vec ℕ 3
xs = 2 ∷ᵥ 4 ∷ᵥ 1 ∷ᵥ []ᵥ
test₁ : xs ≟ xs ≡ yes refl
test₁ = refl
test₂ : xs ≟ (2 ∷ᵥ 4 ∷ᵥ 2 ∷ᵥ []ᵥ) ≡ no _
test₂ = refl
Same for Data.Star:
open import Data.Star
instance StarEq : ∀ {i t} {I : Set i} {T : Rel I t} {i j}
{{iEq : Eq I}} {{tEq : ∀ {i j} -> Eq (T i j)}} -> Eq (Star T i j)
unquoteDef StarEq = deriveEqTo StarEq (quote Star)
Internally
Descriptions of constructors are defined as follows:
mutual
Binder : ∀ {ι} α β γ -> Arg-info -> ι ⊔ lsuc (α ⊔ β) ≡ γ -> Set ι -> Set γ
Binder α β γ i q I = Coerce q (∃ λ (A : Set α) -> < relevance i > A -> Desc I β)
data Desc {ι} (I : Set ι) β : Set (ι ⊔ lsuc β) where
var : I -> Desc I β
π : ∀ {α} i
-> (q : α ≤ℓ β)
-> Binder α β _ i (cong (λ αβ -> ι ⊔ lsuc αβ) q) I
-> Desc I β
_⊛_ : Desc I β -> Desc I β -> Desc I β
Constructors are interpreted in the way described in Descriptions (in the CompProp module). That Coerce stuff is elaborated in Emulating cumulativity in Agda.
A description of a data type is a list of named constructors
record Data {α} (A : Set α) : Set α where
no-eta-equality
constructor packData
field
dataName : Name
parsTele : Type
indsTele : Type
consTypes : List A
consNames : All (const Name) consTypes
For regular data types A is instantiated to Type, for described data types A is instantiated to Desc I β for some I and β. Descriptions also store the name of an original data type and telescopes of types of parameters and indices. Name and Type come from the Reflection module.
There is a reflection machinery that allows to parse regular Agda data types into their described counterparts. An example from the Examples/ReadData.agda module:
data D {α β} (A : Set α) (B : ℕ -> Set β) : ∀ {n} -> B n -> List ℕ -> Set (α ⊔ β) where
c₁ : ∀ {n} (y : B n) xs -> A -> D A B y xs
c₂ : ∀ {y : B 0} -> (∀ {n} (y : B n) {{xs}} -> D A B y xs) -> List A -> D A B y []
D′ : ∀ {α β} (A : Set α) (B : ℕ -> Set β) {n} -> B n -> List ℕ -> Set (α ⊔ β)
D′ = readData D
pattern c₁′ {n} y xs x = #₀ (relv n , relv y , relv xs , relv x , lrefl)
pattern c₂′ {y} r ys = !#₁ (relv y , r , irrv ys , lrefl)
inj : ∀ {α β} {A : Set α} {B : ℕ -> Set β} {n xs} {y : B n} -> D A B y xs -> D′ A B y xs
inj (c₁ y xs x) = c₁′ y xs x
inj (c₂ r ys) = c₂′ (λ y -> inj (r y)) ys
outj : ∀ {α β} {A : Set α} {B : ℕ -> Set β} {n xs} {y : B n} -> D′ A B y xs -> D A B y xs
outj (c₁′ y xs x) = c₁ y xs x
outj (c₂′ r ys) = c₂ (λ y -> outj (r y)) ys
So universe polymorphism is fully supported, as well as implicit and instance arguments, multiple (including single or none) parameters and indices, irrelevance (partly), higher-order inductive occurrences and you can define functions over described data types just like over the actual ones (though, pattern synonyms are not equal in power to proper constructors).
There is a generic procedure that allows to coerce elements of described data type to elements of the corresponding regular data types, e.g. outj can be defined as
outj : ∀ {α β} {A : Set α} {B : ℕ -> Set β} {n xs} {y : B n} -> D′ A B y xs -> D A B y xs
outj d = guncoerce d
Internally it's a bit of reflection sugar on top of a generic fold defined on described data types (the Function/FoldMono.agda module).
It's possible to coerce the other way around:
unquoteDecl foldD = deriveFoldTo foldD (quote D)
inj : ∀ {α β} {A : Set α} {B : ℕ -> Set β} {n xs} {y : B n} -> D A B y xs -> D′ A B y xs
inj = gcoerce foldD
foldD is a derived (via reflection) indexed fold (like foldr on Vec) on D. The procedure that derives indexed folds for regular data types is in the Lib/Reflection/Fold.agda module.
D′ computes to the following term:
λ {.α} {.β} A B {n} z z₁ →
μ
(packData
-- dataName
(quote D)
-- parsTele
(implRelPi (pureDef (quote Level)) "α"
(implRelPi (pureDef (quote Level)) "β"
(explRelPi (sort (set (pureVar 1))) "A"
(explRelPi (pureDef (quote ℕ) ‵→ sort (set (pureVar 2))) "B"
unknown))))
-- indsTele
(implRelPi (pureDef (quote ℕ)) "n"
(appVar 1 (explRelArg (pureVar 0) ∷ []) ‵→
appDef (quote List)
(implRelArg (pureDef (quote lzero)) ∷
explRelArg (pureDef (quote ℕ)) ∷ [])
‵→
sort
(set
(appDef (quote _⊔_)
(explRelArg (pureVar 5) ∷ explRelArg (pureVar 6) ∷ [])))))
-- consTypes
(implRelDPi ℕ
(λ rx →
explRelDPi (B (unrelv rx))
(λ rx₁ →
explRelDPi (List ℕ)
(λ rx₂ →
explRelDPi A (λ rx₃ → var (unrelv rx , unrelv rx₁ , unrelv rx₂)))))
∷
implRelDPi (B 0)
(λ rx →
implRelDPi ℕ
(λ rx₁ →
explRelDPi (B (unrelv rx₁))
(λ rx₂ →
instRelDPi (List ℕ)
(λ rx₃ → var (unrelv rx₁ , unrelv rx₂ , unrelv rx₃))))
⊛ explIrrDPi (List A) (λ rx₁ → var (0 , unrelv rx , [])))
∷ [])
-- consNames
(quote c₁ , quote c₂ , tt))
(n , z , z₁)
Actual generic programming happens in the Property subfolder. There is generic decidable equality defined over described data types. It can be used like this:
xs : Vec (List (Fin 4)) 3
xs = (fsuc fzero ∷ fzero ∷ [])
∷ᵥ (fsuc (fsuc fzero) ∷ [])
∷ᵥ (fzero ∷ fsuc (fsuc (fsuc fzero)) ∷ [])
∷ᵥ []ᵥ
test : xs ≟ xs ≡ yes refl
test = refl
Equality for desribed Vecs, Lists and Fins is derived automatically.
The Property/Reify.agda module implements coercion from described data types to Terms. Since stored names of described constructors are taken from actual constructors, reified elements of described data types are actually quoted elements of regular data types and hence the former can be converted to the latter (like with guncoerce, but deeply and accepts only canonical forms):
record Reify {α} (A : Set α) : Set α where
field reify : A -> Term
macro
reflect : A -> Term -> TC _
reflect = unify ∘ reify
open Reify {{...}} public
instance
DescReify : ∀ {i β} {I : Set i} {D : Desc I β} {j}
{{reD : All (ExtendReify ∘ proj₂) D}} -> Reify (μ D j)
DescReify = ...
open import Generic.Examples.Data.Fin
open import Generic.Examples.Data.Vec
open import Data.Fin renaming (Fin to StdFin)
open import Data.Vec renaming (Vec to StdVec)
xs : Vec (Fin 4) 3
xs = fsuc (fsuc (fsuc fzero)) ∷ᵥ fzero ∷ᵥ fsuc fzero ∷ᵥ []ᵥ
xs′ : StdVec (StdFin 4) 3
xs′ = suc (suc (suc zero)) ∷ zero ∷ (suc zero) ∷ []
test : reflect xs ≡ xs′
test = refl
Having decidable equality on B we can derive decidable equality on A if there is an injection A ↦ B. To construct an injection we need two functions to : A -> B, from : B -> A and a proof from-to : from ∘ to ≗ id. to and from are gcoerce and guncoerce from the above and from-to is another generic function (defined via reflection again, placed in Reflection/DeriveEq.agda: fromToClausesOf generates clauses for it) which uses universe polymorphic n-ary cong under the hood.
There are also generic elim in Function/Elim.agda (the idea is described in Deriving eliminators of described data types and lookup in Function/Lookup.agda (broken currently).
Limitations
-
No support for mutually recursive data types. They can be supported, I just haven't implemented that.
-
No support for inductive-inductive or inductive-recursive data types. The latter can be done at the cost of complicating the encoding.
-
No coinduction.
-
You can't describe a non-strictly positive data type. Yes, I think it's a limitation. I have an idea about how non-strictly positive and inductive-inductive data types can be described (it doesn't give you a way to define safe things safely, but this probably can be added).
-
Records can be described (see
Examples/Data/Product.agda), but η-laws don't hold for them, because constructors containlift refl : tt ≡ ttand(p q : tt ≡ tt) -> p ≡ qdoesn't hold definitionally.μis also adatarather thanrecord(records confuse the termination checker, though, there are{-# TERMINATING #-}pragmas anyway), so this breaks η-expansion too. -
Ornaments may or may not appear later (in the way described in Unbiased ornaments). I don't find them very vital currently.
-
No forcing of indices.
Liftcan be described, though.