Proposal: new flag --cubical-compatible replacing --without-K

[andreasabel]

Agda dev discussion on 2022-03-23 (@UlfNorell @nad @MatthewDaggitt @jespercockx).
Problem we address:

• buggy/incomplete/expensive code for cubical stuff affects users that just want --without-K.
• @MatthewDaggitt: "cubical" errors popping up when there was no mention of anything "cubical" (not even in flags)

New semantics:

• --cubical-compatible is the current --without-K: implies the new --without-K, triggers code that prepares stuff for --cubical (hcomps etc.)

• --without-K just ensures compatibility with univalence

• ? --without-K will be on by default

  Code that breaks because --without-K is now silently on should give informative error to user with a suggestions to maybe turn on --with-K. This affects:

  • termination checker: when termination fails, should try whether it would succeed --with-K and report this to the user
  • pattern matching: when if fails due to absence of K, suggest to user --with-K (do we have this already?)
  • If --without-K is supplied as option where it does have no effect (i.e., unless --with-K is globally on), alert the user of the new flag --cubical-compatible (because they might have wanted this instead).

Also, when a --cubical or --cubical-compatible module imports a module that is not --cubical-compatible, should this be an error? We could also lazily throw errors when hcomps etc. are missing, but then we need to point back to the module which fails to define them due to lack of --cubical-compatible (s/le/ility/).

[anuyts]

It may be sound to have both the cubical operators (but not Glue) and K, though I don't know the details, see A Cubical Language for Bishop Sets.
Edit: It seems they're not actually substantiating such claims for large types.

[nad]

See #3750.

[jespercockx]

I think we should think very carefully and perhaps do a poll before making a change to the default behaviour of Agda such as making --without-K be enabled by default.

[nad]

I don't think we should change the default, that might break a lot of code for little benefit.

[nad]

New semantics:

• --cubical-compatible is the current --without-K: implies the new --without-K, triggers code that prepares stuff for --cubical (hcomps etc.)

• --without-K just ensures compatibility with univalence

In what sense is --without-K supposed to ensure compatibility with univalence? The fix of issue #5448 relies on the new treatment of inductive families. Here is some self-contained code that uses postulated univalence:

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Sigma using (Σ; _,_; fst)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Primitive using (Level; _⊔_)

private
  variable
    a b        : Level
    A B        : Set a
    eq p x y z : A
    P          : A → Set p

------------------------------------------------------------------------
-- Some lemmas related to equality

-- Standard lemmas.

trans : x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : (f : A → B) → x ≡ y → f x ≡ f y
cong _ refl = refl

-- This variant of subst is accepted by Agda 2.6.2, but not by the
-- current development version.

subst : (@0 P : A → Set p) → x ≡ y → P x → P y
subst _ refl p = p

------------------------------------------------------------------------
-- Erased

-- The type constructor Erased.

record Erased (@0 A : Set a) : Set a where
  constructor [_]
  field
    @0 erased : A

-- Some standard properties of modalities. These two lemmas can be
-- proved if we assume function extensionality. They can also be
-- proved if we turn on --with-K.

postulate
  []-cong      : Erased (x ≡ y) → [ x ] ≡ [ y ]
  []-cong-refl : []-cong [ refl {x = x} ] ≡ refl {x = [ x ]}

------------------------------------------------------------------------
-- Univalence

-- Equivalences.

_≃_ : Set a → Set b → Set (a ⊔ b)
A ≃ B =
  Σ (A → B) λ f →
  Σ (B → A) λ f⁻¹ →
  Σ (∀ x → f (f⁻¹ x) ≡ x) λ f-f⁻¹ →
  Σ (∀ x → f⁻¹ (f x) ≡ x) λ f⁻¹-f →
  ∀ x → cong f (f⁻¹-f x) ≡ f-f⁻¹ (f x)

-- Erased univalence.

postulate
  @0 univ          : A ≃ B → A ≡ B
  @0 subst-id-univ : subst (λ A → A) (univ eq) x ≡ eq .fst x

-- Some definitions combining subst and univ.

subst-univ : (@0 P : Set a → Set p) → @0 A ≃ B → P A → P B
subst-univ P eq p = subst (λ ([ x ]) → P x) ([]-cong [ univ eq ]) p

@0 subst-univ-subst :
  {eq : A ≃ B} →
  subst-univ P eq p ≡ subst P (univ eq) p
subst-univ-subst {B = B} {eq = eq}
  rewrite univ eq | []-cong-refl {x = B} = refl

@0 subst-univ-id : subst-univ (λ A → A) eq x ≡ eq .fst x
subst-univ-id = trans subst-univ-subst subst-id-univ

------------------------------------------------------------------------
-- A concrete example of something "bad"

-- The not function.

not : Bool → Bool
not true  = false
not false = true

-- An equivalence defined using not.
--
-- The proof is omitted in order to save space.

@0 swap : Bool ≃ Bool
swap = not , omitted
  where
  postulate
    omitted : _

-- A boolean that should be false.

should-be-false : Bool
should-be-false = subst-univ (λ A → A) swap true

-- We can prove that should-be-false is false.

@0 is-false : should-be-false ≡ false
is-false = subst-univ-id

-- However, if we run the following code, then "True" is printed.

postulate
  print : Bool → IO ⊤

{-# COMPILE GHC print = print #-}

main : IO ⊤
main = print should-be-false

I don't think the code above should be accepted, and if Agda 2.6.3-0a9a5dd is used, then we get the following error message:

Agda.Primitive.Cubical.primTransp (λ i → P (x i)) φ
(subst P refl
 (Agda.Primitive.Cubical.primTransp (λ i → P x₁) φ
  x₂)) is not usable at the required modality
when checking the definition of subst

The code is accepted by Agda 2.6.2.

You might argue that the code uses some postulates related to Erased, and is therefore irrelevant to our discussion. However, these postulates can be proved using (non-erased) univalence, from which we get function extensionality.

[andreasabel]

Revised proposal:

• Just add --cubical-compatible as alias for --without-K and mention it in the documentation.
• --with-K will be the antagonist of --cubical-compatible.

Rationale:
As shown by @nad, current (2.6.2.x) --without-K does not guarantee compatibility with univalence, and we do not know how to implement such a flag without the --cubical-compatible stuff.

[nad]

As an aside the following code that does not make use of @0 is accepted by both Agda 2.6.2 and a recent development version:

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Bool using (Bool; true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Sigma using (Σ; _,_; fst)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Primitive using (Level; _⊔_)

private
  variable
    a b p  : Level
    A B    : Set a
    eq x y : A

------------------------------------------------------------------------
-- Some lemmas related to equality

-- Standard lemmas.

cong : (f : A → B) → x ≡ y → f x ≡ f y
cong _ refl = refl

subst : (P : A → Set p) → x ≡ y → P x → P y
subst _ refl p = p

------------------------------------------------------------------------
-- Univalence

-- Equivalences.

_≃_ : Set a → Set b → Set (a ⊔ b)
A ≃ B =
  Σ (A → B) λ f →
  Σ (B → A) λ f⁻¹ →
  Σ (∀ x → f (f⁻¹ x) ≡ x) λ f-f⁻¹ →
  Σ (∀ x → f⁻¹ (f x) ≡ x) λ f⁻¹-f →
  ∀ x → cong f (f⁻¹-f x) ≡ f-f⁻¹ (f x)

-- Univalence.

postulate
  univ          : A ≃ B → A ≡ B
  subst-id-univ : subst (λ A → A) (univ eq) x ≡ eq .fst x

------------------------------------------------------------------------
-- A concrete example of something "bad"

-- The not function.

not : Bool → Bool
not true  = false
not false = true

-- An equivalence defined using not.
--
-- The proof is omitted in order to save space.

swap : Bool ≃ Bool
swap = not , omitted
  where
  postulate
    omitted : _

-- A boolean that should be false.

should-be-false : Bool
should-be-false = subst (λ A → A) (univ swap) true

-- We can prove that should-be-false is false.

is-false : should-be-false ≡ false
is-false = subst-id-univ

-- However, if we run the following code, then "True" is printed.

postulate
  print : Bool → IO ⊤

{-# COMPILE GHC print = print #-}

main : IO ⊤
main = print should-be-false

I don't think this is a problem: The GHC backend erases equality proofs for --without-K and --erased-cubical (and --with-K), and having non-erased univalence is not compatible with that. If one wants to use non-erased univalence, and compile the code, then one should use --cubical (with a potential future version of Agda with support for compiling such code).

[nad]

• --with-K will be the antagonist of --cubical-compatible.

I don't know exactly what this means, but I guess there should be no change: one can currently import code that uses --without-K from modules that use --with-K, but not vice versa.

[UlfNorell]

The only change (PR: #5862) is adding the flag --cubical-compatible as an alias for --without-K and updating the documentation to reflect that --cubical-compatible is the new, party-approved named.

[nad]

I'd like to note that I find the name a little strange, given that code that uses --cubical-compatible will be compatible with "everything", including --with-K. However, perhaps --compatible-with-everything-including-cubical is too long.

[UlfNorell]

Code using --cubical-compatible is also compatible with the natural numbers, but I don't think it would help to put that in the name. Do you have a list of things that you need --cubical-compatible for, that aren't cubical?

[nad]

I import modules that use --without-K from modules that use --with-K, --erased-cubical, and --cubical.

[UlfNorell]

What's your point? Do you think it should be explicit in the name of the option that it doesn't break compatibility with --with-K?

[nad]

What's your point? Do you think it should be explicit in the name of the option that it doesn't break compatibility with --with-K?

If we have to include something like cubical (to satisfy @MatthewDaggitt's request), then perhaps it would also make sense to include something like K.

[andreasabel]

Maybe --without-K had the advantage to explicitly stating one change (dropping K from unification) but the disadvantage of not stating the rest of the package (termination checking, cubical boilerplate).
On the other hand --cubical-compatible hints that some stuff is done to ensure --cubical will work in importing modules, but isn't specific about any technical details (such as dropping K).

Imo, we haven't gained much really by renaming the option and may just create churn for the customers. In the end, it is down to RTFM in any case...

[martinescardo]

OK. So I am not using cubical and I still need --without-K for formalizing univalent mathematics. Will I be forced to write the misleading --cubical-compatible if all I want is --without-K in my code?

[andreasabel]

Yeah, this is a problem. For the moment, --without-K is still there as a synonym.
What we would actually want is a --without-K that does not prepare for --cubical. Maybe we could change the semantics of --without-K to just:

1. no K in pattern matching
2. modifications to the termination checker that enable HoTT postulates.
3. forbid large indices (UPDATE following @martinescardo)

Actually, 2. and 3. are also strictly more than "without K", but maybe this could be tolerated.

[martinescardo]

Doesn't --without-K also change the universe levels of certain definitions with data? (Again in theory to retain HoTT/UF compatibility.)

I don't really understand (2), by the way.

[andreasabel]

I don't really understand (2), by the way.

Maybe a good entry point for digging:

• Coinduction incompatible with univalence [WAS: Structural termination order incompatible with univalence] #1023

[nad]

OK. So I am not using cubical and I still need --without-K for formalizing univalent mathematics. Will I be forced to write the misleading --cubical-compatible if all I want is --without-K in my code?

Perhaps a better name would be --compatible-with-univalence (or --compatible-with-univalence-and-uip).

[nad]

Maybe we could change the semantics of --without-K to just:

1. no K in pattern matching

2. modifications to the termination checker that enable HoTT postulates.

3. forbid large indices (UPDATE following @martinescardo)

As noted above this does not suffice to ensure compatibility with univalence.

[martinescardo]

I am still not happy with renaming --without-K to --cubical-compatible. It will create a lot of confusion in the HoTT/UF community. My Agda code is not cubical, and I am not planing to make it cubical, but its in HoTT/UF and does need the absence of the K axiom. Cubical is less general, and in particular, at present, cubical proofs are not valid in all infty-toposes, and this is a main reason I am not using cubical (among others). My code can be run with cubical, but this is another matter. One should not confuse cubical type theory with HoTT/UF.

[martinescardo]

People were doing HoTT/UF in Lean and then this became impossible in the new versions of Lean. I really hope this doesn't happen with Agda as well.

[andreasabel]

@martinescardo : A new proposal is at #6049 (comment).

[plt-amy]

Marking this not-in-changelog in favour of #6049.