Notice: (Future) improvement to Glue usability

[plt-amy]

This is just a note to inform everyone of the possibility for an improvement in usability when Agda 2.8.0 drops. Currently the Glue type is exposed as a wrapper that uncurries the system given to it (to apply primGlue) using two lambdas:

Glue : (A : Type ℓ) {φ : I}
       → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
       → Type ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

This has the unfortunate side-effect of, when it can not reduce, duplicating the system everywhere that Agda prints it back to the user, e.g. in the wanted boundary for the definition of uaIdEquiv, which I think everyone finds pretty hard to read:

Type ℓ
———— Boundary (wanted) —————————————————————————————————————
j = i0 ⊢ A
j = i1 ⊢ A
i = i0 ⊢ Cubical.Core.Glue.primGlue A
         (λ .x →
            (λ { (j = i0) → A , idEquiv A ; (j = i1) → A , idEquiv A }) _ .fst)
         (λ .x →
            (λ { (j = i0) → A , idEquiv A ; (j = i1) → A , idEquiv A }) _ .snd)
i = i1 ⊢ A

On 2.7.0.1, this is the best you can do. But for the upcoming version we merged agda/agda#7543, which let display pragmas (a slightly arcane feature that let you specify how Agda should print back a normal form) have nested function applications in them. This makes it possible to recover the surface-level Glue application from the internal primGlue, as long as one of the systems is named. E.g. we replace Glue by

private module G (A : Type ℓ) {φ : I} (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A)) where
  glue-tys : Partial φ (Type ℓ')
  glue-tys (φ = i1) = Te 1=1 .fst

  Glue : Type ℓ'
  Glue = primGlue A glue-tys λ { (φ = i1) → Te 1=1 .snd }

open G using (Glue) public

It's important that glue-sys is defined as a top-level pattern matching function, so that it cannot compute to Te _ .fst until φ = i1. Since systems are compared facewise, these definitions of Glue are convertible, but the new lets us match on this named system in a DISPLAY pragma:

-- in the same module!
{-# DISPLAY primGlue {ℓ} {ℓ'} A {φ} (G.glue-tys _ Te) _ = Glue {ℓ} {ℓ'} A {φ} Te #-}

Now, if we ask for the boundary of uaIdEquiv again, we get the following, which I think is an objective improvement.

Type ℓ
———— Boundary (wanted) —————————————————————————————————————
j = i0 ⊢ A
j = i1 ⊢ A
i = i0 ⊢ Glue A
         (λ { (j = i0) → A , idEquiv A ; (j = i1) → A , idEquiv A })
i = i1 ⊢ A

---

Note: reconstructing the full application of Glue in the display form seems a bit redundant, since display forms do not have to have well-typed RHSes. But display forms are applied to the results of other display forms, so it's important for compositionality if we want to make other Glue types display in an even nicer form... For example, we can name the system used for ua as well!

private module U {A B : Type ℓ} (e : A ≃ B) where
  ua-sys : ∀ i → Partial (i ∨ ~ i) (Σ[ T ∈ Type ℓ ] T ≃ B)
  ua-sys i (i = i0) = A , e
  ua-sys i (i = i1) = B , idEquiv B

  ua : A ≡ B
  ua i = Glue B (ua-sys i)

open U using (ua) public
{-# DISPLAY Glue _ (U.ua-sys e i) = ua e i #-}

Now the boundary looks like this, which while I think is an improvement, does have the downside of no longer making it possible to spot that uaIdEquiv actually makes sense, since the actual boundary does not mention ua-sys internally and so does not print as an application of ua.

Type ℓ
———— Boundary (wanted) —————————————————————————————————————
j = i0 ⊢ A
j = i1 ⊢ A
i = i0 ⊢ ua (idEquiv A) j
i = i1 ⊢ A

Type ℓ
———— Boundary (actual) —————————————————————————————————————
j = i0 ⊢ A
j = i1 ⊢ A
i = i0 ⊢ Glue A (λ ._ → A , idEquiv A)
i = i1 ⊢ A

[plt-amy]

Note 2: In the 1Lab we can also make a display form for p ∙∙ q ∙∙ r, but this relies on the wrapper we use for hcomp, which puts the base face in the system also. In the cubical library, the only thing we can actually match on (the system) does not mention the middle path q. We can almost recover q as the second argument of hcomp, but there it is applied to a dimension, so the recovered term is incorrect. Concretely, adding

{-# DISPLAY hcomp (doubleComp-faces p r i) q = (p ∙∙ q ∙∙ r) i #-}

causes the normal form of p ∙∙ q ∙∙ r (e.g. in the type of doubleCompPath-filler) to display as λ i → (p ∙∙ q i ∙∙ r) i, which is incorrect. This could be solved by parameterising doubleCompPath-faces over q as well (even though it wouldn't be used!), but this function is used elsewhere in the library, so this is a more invasive change.

Note 3: Even then, since display forms (even internally) can't match on whether a function is constant, it's impossible to get refl ∙∙ p ∙∙ q to display as p ∙ q. Of course, redefining p ∙ q with a specialized, named system would recover this possibility and still be convertible to refl ∙∙ p ∙∙ q.

[plt-amy]

I'm not opening a pull request right now since it wouldn't be mergeable until the new Agda version is released, and I'd rather not wait to let everyone know because I'd probably forget! But if you want to have me in the commit log when/if this improvement is accepted, here is a patch with the right committer info that can be applied as

$ curl https://gist.githubusercontent.com/plt-amy/d3d4313a7ce853e9e8bb1fa6c12fe4ec/raw/9da0e4d53273418752033d39b7171f14fdf47e3a/0001-Use-named-systems-for-nicer-display-forms.patch | git am

and then pushed by any maintainer.