Post-fork language consolidation #1

amyliao commented 2026年04月20日 14:19:10 +02:00

We've inherited almost half a million type theories, controlled by something like 30 different command-line flags, along with almost 20 years of miscellaneous accumulated cruft. I don't think this is maintainable. I think the following features should be removed:

• Every language mode except for full cubical (so: --with-K, --without-K, --cubical-compatible, --cubical=erased, and --cubical=no-glue). This includes some features that do not make sense for full cubical mode:
  • --injective-type-constructors
  • --large-indices
  • compilation (in general).
• Sized types, which are known to be inconsistent, hence also:
  • src/size-solver
  • --no-guardedness
• Musical coinduction
• Every modal system:
  • --erasure, --erased-matches
  • --experimental-irrelevance, --irrelevant-projections
  • --cohesion, --flat-split
  • --polarity
  • --guarded
• Variants on the sort system:
  • --level-universe
  • --no-two-level
  • --no-prop
  • --cumulativity
  • --no-universe-polymorphism
  • --type-in-type, --omega-in-omega
• Rewrite rules
• The unused MEASURE pragma, which was kept for backwards compatibility
• The STATIC pragma, used for compilation

The result should be an implementation of a two-level type theory whose fibrant fragment is De Morgan cubical type theory with a universe of strict propositions. The two "teaching" options --no-pattern-matching and --no-copatterns seem like they affect the type theory, but they only do so locally to a module, and their implementation is very contained (unlike e.g. --no-universe-polymorphism), so they can be kept without great burden.

Note: a previous version of the proposed downsizing recovered limited definitional proof-irrelevance by keeping the irrelevance modality, but, given that irrelevant record fields are a very dodgy feature, I think it makes more sense to keep Prop, which is better understood.

We've inherited almost half a million type theories, controlled by something like 30 different command-line flags, along with almost 20 years of miscellaneous accumulated cruft. I don't think this is maintainable. I think the following features should be **removed**: - [x] Every language mode except for *full cubical* (so: `--with-K`, `--without-K`, `--cubical-compatible`, `--cubical=erased`, and `--cubical=no-glue`). This includes some features that do not make sense for full cubical mode: - [x] `--injective-type-constructors` - [x] `--large-indices` - [x] **compilation** (in general). - [x] Sized types, which are known to be inconsistent, hence also: - [x] `src/size-solver` - [x] `--no-guardedness` - [x] Musical coinduction - [x] _Every_ modal system: - [x] `--erasure`, `--erased-matches` - [x] `--experimental-irrelevance`, `--irrelevant-projections` - [x] `--cohesion`, `--flat-split` - [x] `--polarity` - [x] `--guarded` - [ ] Variants on the sort system: - [ ] `--level-universe` - [x] `--no-two-level` - [ ] `--no-prop` - [x] `--cumulativity` - [x] `--no-universe-polymorphism` - [x] `--type-in-type`, `--omega-in-omega` - [x] Rewrite rules - [x] The unused `MEASURE` pragma, which was kept for backwards compatibility - [x] The `STATIC` pragma, used for compilation The result should be an implementation of a two-level type theory whose fibrant fragment is De Morgan cubical type theory with a universe of strict propositions. The two "teaching" options `--no-pattern-matching` and `--no-copatterns` _seem_ like they affect the type theory, but they only do so locally to a module, and their implementation is very contained (unlike e.g. `--no-universe-polymorphism`), so they can be kept without great burden. **Note:** a previous version of the proposed downsizing recovered limited definitional proof-irrelevance by keeping the irrelevance modality, but, given that irrelevant record fields are a very dodgy feature, I think it makes more sense to keep `Prop`, which is better understood.

amyliao commented 2026年04月27日 16:55:27 +02:00

Even though irrelevant record fields are harder to come by now, you can still write "boxed unboxings" using copattern matching. These combine with the map ∥ A ∥ → Squash A to give ⊥.

recordSquash{l}(A:Typel):Typelwhereconstructorliftfield.lower:Ano-squash-⊥:Squash⊥→⊥no-squash-⊥()squash-global-choice:Squash(∀{A:Type}→SquashA→A)squash-global-choice.lower(liftx)=x

Even though irrelevant record fields are harder to come by now, you can still write "boxed unboxings" using copattern matching. These combine with the map `∥ A ∥ → Squash A` to give `⊥`. ```agda record Squash {l} (A : Type l) : Type l where constructor lift field .lower : A no-squash-⊥ : Squash ⊥ → ⊥ no-squash-⊥ () squash-global-choice : Squash (∀ {A : Type} → Squash A → A) squash-global-choice .lower (lift x) = x ```