Arity-generic programming in Agda

Question

How to write arity-generic functions in Agda? Is it possible to write fully dependent and universe polymorphic arity-generic functions?

Accepted Answer

I'll take an n-ary composition function as an 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 is how `N-ary` is defined in the `Data.Vec.N-ary` module:

```
N-ary : ∀ {ℓ₁ ℓ₂} (n : ℕ) → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
N-ary zero    A B = B
N-ary (suc n) A B = A → N-ary n A B
```

I.e. `comp` receives a number `n`, a function `g : Y -> Z` and a function `f`, which has the arity `n` and the resulting type `Y`.

In the `comp 0 g y = {!!}` case we have

```
Goal : Z
y    : Y
g    : Y -> Z
```

hence the hole can be easily filled by `g y`.

In the `comp (suc n) g f = {!!}` case, `N-ary (suc n) X Y` reduces to `X -> N-ary n X Y` and `N-ary (suc n) X Z` reduces to `X -> N-ary n X Z`. So we have

```
Goal : X -> N-ary n X Z
f    : X -> N-ary n X Y
g    : Y -> Z
```

C-c C-r reduces the hole to `λ x -> {!!}`, and now `Goal : N-ary n X Z`, which can be filled by `comp n g (f x)`. So the 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` to them and then applies `g` to the result.

The simplest version with a 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 be there in the hole? We can't use `N-ary n X Z` as before, because `Z` is a function now. If `Z` is a function, we need to apply it to something, that has type `Y`. But the only way to get something of type `Y` is to apply `f` to `n` arguments of type `X`. Which is just like our `comp` but only at the 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` then 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 with arguments with different types

There is the "Arity-generic datatype-generic programming" paper, that describes, among other things, how to write arity-generic functions, that receive arguments of different types. The idea is to pass a vector of types as a parameter and fold it pretty much in the style of `N-ary`:

```
arrTy : {n : N} → Vec Set (suc n) → Set
arrTy {0}     (A :: []) = A
arrTy {suc n} (A :: As) = A → arrTy As
```

However Agda is unable to infer that vector, even if we provide its length. Hence the paper also provides an operator for currying, which makes from a function, that explicitly receives a vector of types, a function, that receives `n` implicit arguments.

This approach works, but it doesn't scale to fully universe polymorphic functions. We can avoid all these problems by replacing the `Vec` datatype with the `_^_` operator:

```
_^_ : ∀ {α} -> Set α -> ℕ -> Set α
A ^ 0     = Lift ⊤
A ^ suc n = A × A ^ n
```

`A ^ n` is isomorphic to `Vec A n`. Then our new `N-ary` is

```
_->ⁿ_ : ∀ {n} -> Set ^ n -> Set -> Set
_->ⁿ_ {0}      _      B = B
_->ⁿ_ {suc _} (A , R) B = A -> R ->ⁿ B
```

All types lie in `Set` for simplicity. `comp` now 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 a version with a 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 and universe polymorphic `comp`

The key idea is to represent a vector of types as 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 like "there is a type `X` such that all other types depend on an element of `X`". Our new `N-ary` is 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 : ℕ) -> A -> Vec A n

test : Fold (Set , λ A -> ℕ , λ n -> A , λ _ -> Vec A n) 
test = explicit-replicate
```

But what are the types of `Z` and `g` now?

```
comp : ∀ n {β γ} {αs : Level ^ n} {Xs : Sets αs β} {Z : {!!}}
     -> {!!} -> (f : Fold Xs) -> Comp n Z f
comp  0      g y =…

Arity-generic programming in Agda

Solution

Problem