Generic congN?

[gallais]

Recently I've been needing cong₃ so I figured I might as well check whether I can write a generic version. After playing type cosmonaut for a bit, here we are:

open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Data.Vec
open import Data.Vec.All
open import Data.Product
open import Data.Unit
open import Function
open import Level

toLevel : ∀ {n} → Vec Level n → Level
toLevel = foldr _ _⊔_ zero

Sets : ∀ {n} (ls : Vec Level n) → Set (suc (toLevel ls))
Sets []       = Lift _ ⊤
Sets (l ∷ ls) = Set l × Sets ls

arrows : ∀ {n r} (ls : Vec Level n) → Sets ls → Set r → Set (toLevel ls ⊔ r)
arrows []       ds       c = c
arrows (l ∷ ls) (d , ds) c = d → arrows ls ds c

eqs : ∀ {n r} (ls : Vec Level n) (ds : Sets ls) {c : Set r} →
      (f g : arrows ls ds c) → Set (toLevel ls ⊔ r)
eqs []       ds       f g = f ≡ g
eqs (l ∷ ls) (d , ds) f g = {x y : d} → x ≡ y → eqs ls ds (f x) (g y)

cong : ∀ n {ls : Vec Level n} {ds : Sets ls} {r} (c : Set r) →
       (f : arrows ls ds c) → eqs ls ds f f
cong _ {[]}     c f      = refl
cong _ {l ∷ ls} c f refl = cong _ {ls} c (f _)

-- test case

data Tree {l} (A : Set l) : Set l where
  node : Tree ⊤ → Tree A × Tree (A × A) → ⊤ → Tree A →
        (Vec ⊤ 2 → Tree (Vec A 5)) → Tree A

_ : ∀ {k l m n p q r s t u} → node k l m n p ≡ node q r s t u
_ = cong 5 (Tree (Lift (suc (suc zero)) ⊤)) node {!!} {!!} {!!} {!!} {!!}

As you'll have noticed you need to specify the return type of the constructor for inference to work. I don't think we can get anything better without resorting to reflection to inspect the goal directly: there is no reason for Agda to assume the constructor is fully applied.

Thoughts?

Somewhat related: #10

[gallais]

Nevermind my previous comment: it is possible to get even more from the unifier by not using a Vec Level n but rather an equivalent definition which can get solved via eta-expansion & unification.

If we define everything by induction on the natural number then we don't need to specify the return type: it is whatever is leftover after the first n argument types have been used.

open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Data.Unit
open import Data.Product
open import Level as L hiding (zero; suc)
open import Data.Nat.Base

Levels : ℕ → Set
Levels zero    = ⊤
Levels (suc n) = Level × Levels n

toLevel : ∀ n → Levels n → Level
toLevel zero    ls       = L.zero
toLevel (suc n) (l , ls) = l L.⊔ toLevel n ls

Sets : ∀ n (ls : Levels n) → Set (L.suc (toLevel n ls))
Sets zero    ls       = Lift _ ⊤
Sets (suc n) (l , ls) = Set l × Sets n ls

arrows : ∀ n {r} (ls : Levels n) → Sets n ls → Set r → Set (toLevel n ls L.⊔ r)
arrows zero    ls       ds       c = c
arrows (suc n) (l , ls) (d , ds) c = d → arrows n ls ds c

eqs : ∀ n {r} (ls : Levels n) (ds : Sets n ls) {c : Set r} →
      (f g : arrows n ls ds c) → Set (toLevel n ls L.⊔ r)
eqs zero    ls       ds       f g = f ≡ g
eqs (suc n) (l , ls) (d , ds) f g = {x y : d} → x ≡ y → eqs n ls ds (f x) (g y)

cong : ∀ n {ls : Levels n} {ds : Sets n ls} {r} {c : Set r} →
       (f : arrows n ls ds c) → eqs n ls ds f f
cong zero    f      = refl
cong (suc n) f refl = cong n (f _)

-- test case

open import Data.Vec

data Tree {l} (A : Set l) : Set l where
  node : A → Tree ⊤ → Tree A × Tree (A × A) → ⊤ →
         Tree A → (Vec ⊤ 2 → Tree (Vec A 5)) → Tree A

_ : ∀ {k l m n p q r s t u} → node tt k l m n p ≡ node tt q r s t u
_ = cong 5 (node tt) {!!} {!!} {!!} {!!} {!!}

[MatthewDaggitt]

Haha, awesome, I've always wondered about this!

I've been trying to do similar things like write a hole operator (e.g. be able to replace λ c → f a b c d e with f a b ◌ d e). The machinery above looks like it might be useful.

Two questions. Where would we put the machinery and where would we put the new cong. For the latter I guess it should probably go in Relation.Binary.PropositionalEquality under congₙ? I guess we should also try to create substₙ as well.

[MatthewDaggitt]

Next up, get it to work with dependent functions :laughing:

[gallais]

I've been trying to do similar things like write a hole operator (e.g. be able to replace λ c → f a b c d e with f a b ◌ d e). The machinery above looks like it might be useful.

Oooh, I like this idea!

Where would we put the machinery?

Good question. Some of it could go under Data.Product.N-ary.Heterogeneous. It would depart from Data.Product.N-ary which has a special case of 0 and 1 but that makes all the code more complicated without a huge benefit in my opinion.

it should probably go in Relation.Binary.PropositionalEquality under congₙ? I guess we should also try to create substₙ as well.

:+1: to both

[MatthewDaggitt]

Some of it could go under Data.Product.N-ary.Heterogeneous. It would depart from Data.Product.N-ary which has a special case of 0 and 1 but that makes all the code more complicated without a huge benefit in my opinion.

:+1:

[gallais]

subst can indeed be defined in the same manner:

Subst : ∀ n {r} (ls : Levels n) (ds : Sets n ls) →
        (f g : arrows n ls ds (Set r)) → Set (toLevel n ls L.⊔ r)
Subst zero    ls       ds       f g = f → g
Subst (suc n) (l , ls) (d , ds) f g = {x y : d} → x ≡ y → Subst n ls ds (f x) (g y)

subst : ∀ n {ls : Levels n} {ds : Sets n ls} {r} →
        (f : arrows n ls ds (Set r)) → Subst n ls ds f f
subst zero    f x    = x
subst (suc n) f refl = subst n (f _)

postulate
  C : (A B : Set) (m n : ℕ) → Set

_ : ∀ {A B D E m n p q} → C A B m n → C D E p q
_ = subst 4 C {!!} {!!} {!!} {!!}

[effectfully]

Hey guys, I came across this development and I did some work related to arity-generic programming in Agda a few years ago, so I thought you might be interested.

In this Stack Overflow answer I describe how to get n-ary dependent function composition (currently stdlib only supports non-dependent n-ary functions, right?).

In this blog post I further elaborate on how to unify dependent and non-dependent representations of telescopes.

And while we're here, there is also a way to emulate cumulativity of universes which is occasionally helpful when you need to deal with n-ary functions.

I've also implemented n-ary cong here in a composable way (e.g. one can apply congn to itself and that will type check perfectly, which I think is not the case with the current stdlib implementation of n-ary cong).

Hope that can be helpful.