Search code examples
generic-programmingagdadependent-typearity

Arity-generic programming in Agda

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

Solution

  • 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 = g y
comp (suc n) g f = λ x -> comp n g (f x)

    Recall that f previously had type Xs ->ⁿ Y, but Y now is hidden in the end of these nested dependent pairs and can depend on an element of any X from Xs. Z previously had type Y -> Set γ, hence now we need to append Set γ to Xs, making all 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 γ, what type has g? Previously it was (y : Y) -> Z y. Again we need to append something to nested dependent pairs, since Y is again hidden, only in a 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 A n -> ℕ
length {n = n} _ = n

explicit-replicate : (A : Set) -> (n : ℕ) -> A -> Vec A n
explicit-replicate _ _ x = replicate x

foo : (A : Set) -> ℕ -> A -> ℕ
foo = comp 3 length explicit-replicate

test : foo Bool 5 true ≡ 5
test = refl

    Note the dependency in the arguments and the resulting type of explicit-replicate. Besides, Set lies in Set₁, while ℕ and A lie in Set — this illustrates universe polymorphism.

    Remarks

    AFAIK, there is no comprehensible theory for implicit arguments, so I don't know, how all this stuff will work, when the second function (i.e. f) receives implicit arguments. This test:

    foo' : ∀ {α} {A : Set α} -> ℕ -> A -> ℕ
foo' = comp 2 length (λ n -> replicate {n = n})

test' : foo' 5 true ≡ 5
test' = refl

    is passed at least.

    comp can't handle functions, if the universe, where some type lies, depends on a value. For example

    explicit-replicate' : ∀ α -> (A : Set α) -> (n : ℕ) -> A -> Vec A n
explicit-replicate' _ _ _ x = replicate x

... because this would result in an invalid use of Setω ...
error : ∀ α -> (A : Set α) -> ℕ -> A -> ℕ
error = comp 4 length explicit-replicate'

    But it's common for Agda, e.g. you can't apply explicit id to itself:

    idₑ : ∀ α -> (A : Set α) -> A -> A
idₑ _ _ x = x

-- ... because this would result in an invalid use of Setω ...
error = idₑ _ _ idₑ

    The code.