Arity-generic programming in Agda -

how write arity-generic functions in agda? possible write dependent , universe polymorphic arity-generic functions?

i'll take n-ary composition function example.

the simplest version

open import data.vec.n-ary  comp : ∀ n {α β γ} {x : set α} {y : set β} {z : set γ}      -> (y -> z) -> n-ary n x y -> n-ary n x z comp  0      g y = {!!} comp (suc n) g f = {!!} 

here how n-ary defined in data.vec.n-ary module:

n-ary : ∀ {ℓ₁ ℓ₂} (n : ℕ) → set ℓ₁ → set ℓ₂ → set (n-ary-level ℓ₁ ℓ₂ n) n-ary 0    b = b n-ary (suc n) b = → n-ary n b 

i.e. comp receives number n, function g : y -> z , function f, has arity n , resulting type y.

in comp 0 g y = {!!} case have

goal : z y    : y g    : y -> z 

hence hole can filled g y.

in comp (suc n) g f = {!!} case, n-ary (suc n) x y reduces x -> n-ary n x y , n-ary (suc n) x z reduces x -> n-ary n x z. have

goal : x -> n-ary n x z f    : x -> n-ary n x y g    : y -> z 

c-c c-r reduces hole λ x -> {!!}, , goal : n-ary n x z, can filled comp n g (f x). whole definition is

comp : ∀ n {α β γ} {x : set α} {y : set β} {z : set γ}      -> (y -> z) -> n-ary n x y -> n-ary n x z comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x) 

i.e. comp receives n arguments of type x, applies f them , applies g result.

the simplest version dependent g

when g has type (y : y) -> z y

comp : ∀ n {α β γ} {x : set α} {y : set β} {z : y -> set γ}      -> ((y : y) -> z y) -> (f : n-ary n x y) -> {!!} comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x) 

what should there in hole? can't use n-ary n x z before, because z function now. if z function, need apply something, has type y. way of type y apply f n arguments of type x. our comp @ type level:

comp : ∀ n {α β γ} {x : set α} {y : set β}      -> (y -> set γ) -> n-ary n x y -> set (n-ary-level α γ n) comp  0      z y = z y comp (suc n) z f = ∀ x -> comp n z (f x) 

and comp is

comp : ∀ n {α β γ} {x : set α} {y : set β} {z : y -> set γ}      -> ((y : y) -> z y) -> (f : n-ary n x y) -> comp n z f comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x) 

a version arguments different types

there "arity-generic datatype-generic programming" paper, describes, among other things, how write arity-generic functions, receive arguments of different types. idea pass vector of types parameter , fold pretty in style of n-ary:

arrty : {n : n} → vec set (suc n) → set arrty {0}     (a :: []) = arrty {suc n} (a :: as) = → arrty 

however agda unable infer vector, if provide length. hence paper provides operator currying, makes function, explicitly receives vector of types, function, receives n implicit arguments.

this approach works, doesn't scale universe polymorphic functions. can avoid these problems replacing vec datatype _^_ operator:

_^_ : ∀ {α} -> set α -> ℕ -> set α ^ 0     = lift ⊤ ^ suc n = × ^ n 

a ^ n isomorphic vec n. our new n-ary is

_->ⁿ_ : ∀ {n} -> set ^ n -> set -> set _->ⁿ_ {0}      _      b = b _->ⁿ_ {suc _} (a , r) b = -> r ->ⁿ b 

all types lie in set simplicity. comp is

comp : ∀ n {xs : set ^ n} {y z : set}      -> (y -> z) -> (xs ->ⁿ y) -> xs ->ⁿ z comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x) 

and version dependent g:

comp : ∀ n {xs : set ^ n} {y : set}      -> (y -> set) -> (xs ->ⁿ y) -> set comp  0      z y = z y comp (suc n) z f = ∀ x -> comp n z (f x)  comp : ∀ n {xs : set ^ n} {y : set} {z : y -> set}      -> ((y : y) -> z y) -> (f : xs ->ⁿ y) -> comp n z f comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x) 

fully dependent , universe polymorphic comp

the key idea represent vector of types nested dependent pairs:

sets : ∀ {n} -> (αs : level ^ n) -> ∀ β -> set (mono-^ (map lsuc) αs ⊔ⁿ lsuc β) sets {0}      _       β = set β sets {suc _} (α , αs) β = Σ (set α) λ x -> x -> sets αs β 

the second case reads "there type x such other types depend on element of x". our new n-ary trivial:

fold : ∀ {n} {αs : level ^ n} {β} -> sets αs β -> set (αs ⊔ⁿ β) fold {0}      y      = y fold {suc _} (x , f) = (x : x) -> fold (f x) 

an example:

postulate   explicit-replicate : (a : set) -> (n : ℕ) -> -> vec n  test : fold (set , λ -> ℕ , λ n -> , λ _ -> vec n)  test = explicit-replicate 

but types of z , g now?

comp : ∀ n {β γ} {αs : level ^ n} {xs : sets αs β} {z : {!!}}      -> {!!} -> (f : fold xs) -> comp n z f comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x) 

recall f had type xs ->ⁿ y, y hidden in end of these nested dependent pairs , can depend on element of x xs. z had type y -> set γ, hence need append set γ xs, making xs implicit:

_⋯>ⁿ_ : ∀ {n} {αs : level ^ n} {β γ}       -> sets αs β -> set γ -> set (αs ⊔ⁿ β ⊔ γ) _⋯>ⁿ_ {0}      y      z = y -> z _⋯>ⁿ_ {suc _} (_ , f) z = ∀ {x} -> f x ⋯>ⁿ z 

ok, z : xs ⋯>ⁿ set γ, type has g? (y : y) -> z y. again need append nested dependent pairs, since y again hidden, in dependent way now:

Πⁿ : ∀ {n} {αs : level ^ n} {β γ}    -> (xs : sets αs β) -> (xs ⋯>ⁿ set γ) -> set (αs ⊔ⁿ β ⊔ γ) Πⁿ {0}      y      z = (y : y) -> z y Πⁿ {suc _} (_ , f) z = ∀ {x} -> Πⁿ (f x) z 

and finally

comp : ∀ n {αs : level ^ n} {β γ} {xs : sets αs β}      -> (xs ⋯>ⁿ set γ) -> fold xs -> set (αs ⊔ⁿ γ) comp  0      z y = z y comp (suc n) z f = ∀ x -> comp n z (f x)  comp : ∀ n {β γ} {αs : level ^ n} {xs : sets αs β} {z : xs ⋯>ⁿ set γ}      -> Πⁿ xs z -> (f : fold xs) -> comp n z f comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x) 

a test:

length : ∀ {α} {a : set α} {n} -> vec n -> ℕ length {n = n} _ = n  explicit-replicate : (a : set) -> (n : ℕ) -> -> vec n explicit-replicate _ _ x = replicate x  foo : (a : set) -> ℕ -> -> ℕ foo = comp 3 length explicit-replicate  test : foo bool 5 true ≡ 5 test = refl 

note dependency in arguments , resulting type of explicit-replicate. besides, set lies in set₁, while ℕ , a lie in set — illustrates universe polymorphism.

remarks

afaik, there no comprehensible theory implicit arguments, don't know, how stuff work, when second function (i.e. f) receives implicit arguments. test:

foo' : ∀ {α} {a : set α} -> ℕ -> -> ℕ foo' = comp 2 length (λ n -> replicate {n = n})  test' : foo' 5 true ≡ 5 test' = refl 

is passed @ least.

comp can't handle functions, if universe, type lies, depends on value. example

explicit-replicate' : ∀ α -> (a : set α) -> (n : ℕ) -> -> vec n explicit-replicate' _ _ _ x = replicate x  ... because result in invalid use of setω ... error : ∀ α -> (a : set α) -> ℕ -> -> ℕ error = comp 4 length explicit-replicate' 

but it's common agda, e.g. can't apply explicit id itself:

idₑ : ∀ α -> (a : set α) -> -> idₑ _ _ x = x  -- ... because result in invalid use of setω ... error = idₑ _ _ idₑ 

---

the code.