Agda-stdlib: Generic congN?

Created on 30 Dec 2018  Β·  7Comments  Β·  Source: agda/agda-stdlib

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

library-design question
Source
picture gallais

Most helpful comment

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 {!!} {!!} {!!} {!!}
picture gallais on 12 Jan 2019
🎉2

All 7 comments

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) {!!} {!!} {!!} {!!} {!!}
gallais picture gallais on 30 Dec 2018

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 picture MatthewDaggitt on 12 Jan 2019

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

MatthewDaggitt picture MatthewDaggitt on 12 Jan 2019

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

gallais picture gallais on 12 Jan 2019

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:

MatthewDaggitt picture MatthewDaggitt on 12 Jan 2019

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 {!!} {!!} {!!} {!!}
gallais picture gallais on 12 Jan 2019
🎉2

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.

effectfully picture effectfully on 13 May 2019
👍1
Was this page helpful?
0 / 5 - 0 ratings

Related issues

gallais picture gallais  Β·  8Comments
MatthewDaggitt picture MatthewDaggitt  Β·  5Comments
langston-barrett picture langston-barrett  Β·  7Comments
JacquesCarette picture JacquesCarette  Β·  8Comments
asr picture asr  Β·  3Comments