A compiler for Cubical Agda programs where all cubical parts have been marked as erased

[nad]

Perhaps it is possible to compile Cubical Agda programs where all the cubical parts have been marked as erased.

I brought this up during the current Agda meeting, and someone (@txa?) suggested that it should be possible to do better. If I understood correctly the suggestion was that, in a setting without glue, it should be possible to erase all paths and transports (without marking them as erased). However, it's not obvious to me how this could be done.

For instance, consider the following code:

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical

f : {@0 A : Set} {@0 x y : A} → x ≡ y → A
f p = p i0

One might imagine that it would be possible to handle the application of a path to 0 or 1 by returning one of the endpoints, but as can be seen above the endpoints might be erased. A fix might be to add an implicit @0 annotation to all path arguments and disallow the definition of f, but then we're basically back to my original suggestion.

Another question concerns functions from the interval. Can they be treated in the same way as paths?

[nad]

I discussed this with @Saizan. He suggested that, in the absence of glue, we could compile the interval to the unit type, and paths to functions from the unit type.

I don't think we should have yet another variant of Agda (with glue marked as erased). However, we could have a simple analysis that keeps track of which expressions use glue in non-erased contexts, and then refuse to compile main if the analysis says that main uses glue.

[nad]

We might have to switch off some optimisations. Currently the propositional equality type is compiled to something like the unit type.

[Saizan]

That should be fine if all the cubical stuff is erased?

[nad]

These things are subtle (see #4784), so I don't know. However, I was thinking of the compiler for programs where glue is erased, but perhaps not other cubical things.

[nad]

Perhaps it is possible to compile Cubical Agda programs where all the cubical parts have been marked as erased.

Marking all cubical parts as erased might not be so nice. For instance, the builtins are currently not marked as erased in Agda.Primitive.Cubical. It might be better to ensure that no cubical thing can be reached from main, and only compile the reachable things (compare #4733). The reachability relation should take erasure into account. However, it is not obvious to me exactly how this reachability relation should be defined.

One question is whether type signatures (which are checked in an erased context) can be ignored. Consider the following example:

data D : Set where
  c₀ : D
  c₁ : D → D

@0 D′ : Set
D′ = D

f : D′ → D′
f c₀     = c₀
f (c₁ y) = y

Here we can see that D is reachable from f by inspecting only the body of f, the type signature is not needed. Now consider the following code:

A : Set
A = …

@0 Id : Set → Set
Id x = x

f : Id A → A
f x = x

Which identifiers are reachable from f? Presumably not Id, which is erased. However, can A be reached? Note that the body of A might make use of non-erased univalence, and that the current GHC backend does not compile f in the same way for all definitions of A.

[nad]

An alternative to the idea to check which things are reachable from main, based on a discussion with @andreasabel:

• Make it possible to have erased import statements: every symbol brought into scope by such a statement would be erased.
• Add a flag --erased-cubical, which enables a variant of Cubical Agda in which cubical features are only allowed in erased settings. This flag is coinfective for regular import statements, but not for erased ones. Regular cubical code can be imported, but only via erased import statements. (The --cubical flag thus becomes less coinfective.)

A contrived example:

{-# OPTIONS --cubical #-}

module Propositional-truncation where

open import Agda.Builtin.Cubical.Path

data ∥_∥ (A : Set) : Set where
  ∣_∣     : A → ∥ A ∥
  trivial : ∀ x y → x ≡ y

{-# OPTIONS --erased-cubical #-}

module Propositional-truncation.Erased where

@0 open import Agda.Builtin.Cubical.Path
@0 import Propositional-truncation as PT

data ∥_∥ (A : Set) : Set where
  ∣_∣        : A → ∥ A ∥
  @0 trivial : ∀ x y → x ≡ y

@0 ∥∥→∥∥ : {A : Set} → PT.∥ A ∥ → ∥ A ∥
∥∥→∥∥ PT.∣ x ∣           = ∣ x ∣
∥∥→∥∥ (PT.trivial x y i) = trivial (∥∥→∥∥ x) (∥∥→∥∥ y) i

If this works, then we could perhaps later allow more features (like paths) in non-erased code.

[JacquesCarette]

Ooh, nice. Propositional truncation is probably the one thing outside core Agda that I'd really like to be able to use.

[nad]

I'm trying to make Agda parse erased import statements:

open @0 import Agda.Primitive

(Here @0 is placed after open to emphasise that it applies to the entire import statement, not just the "opening". I do not plan to allow the syntax @0 open import M.)

The next step is to ensure that all symbols obtained from such an import statement are actually erased. If the information about whether a symbol is erased or not had been part of the scope, then this would presumably have been easy. Would it make sense to include this information in the scope? I guess another approach would be to copy the module and create wrappers for all definitions, but that sounds unnecessarily expensive. Any thoughts?

[nad]

I guess another approach would be to copy the module and create wrappers for all definitions, but that sounds unnecessarily expensive.

The current module macro code handles this kind of copying, and it would be easy to change the quantity of the copied definitions, but there is one problem: statements like open import M es are treated like the following code:

import M as Fresh
open Fresh es

I think I can make open @0 import M behave like the following code (where I pretend that @0 open M is valid syntax):

import M as Fresh
@0 open Fresh

However, this is not good enough: the names exposed by the open statement can reduce to names in M, and these names are not necessarily erased.

In fact, this is a general problem with the explanation of erased import statements given above: "every symbol brought into scope by such a statement would be erased". This is not sufficient, because such symbols could reduce to code that should be treated as erased.

[nad]

Another approach that might work:

• We keep track of which "language" is used for each definition (--without-K, --cubical, --erased-cubical, --with-K).
• In --erased-cubical modules definitions with the language --cubical are treated as erased.
• We could either skip the erased import statements, or require the use of the annotations. Would the annotations make it more obvious to users what is going on? Would they be annoying? I think I prefer having the annotations.

[nad]

• Add a flag --erased-cubical, which enables a variant of Cubical Agda in which cubical features are only allowed in erased settings. This flag is coinfective for regular import statements, but not for erased ones.

The last sentence does not make sense to me. The flag should not be coinfective. It should be fine to import modules that use --without-K and --erased-cubical, as well as code that uses --cubical (via erased import statements). Only modules that use --erased-cubical or --cubical may import modules that use --erased-cubical.

[nad]

I have implemented a first draft of --erased-cubical, and performed initial testing.

I did not change the import statement syntax.

Currently all cubical features are allowed when --erased-cubical is used, except for non-erased higher constructors and the builtins/primitives in Agda.Builtin.Cubical.Glue and Agda.Builtin.Cubical.HCompU. Are there any other primitives that should be disallowed?

The next step is to add support for compiling code that uses --erased-cubical.

[nad]

Are there any other primitives that should be disallowed?

Currently at least the following builtins/primitives are allowed:

• builtinPath
• builtinPathP
• builtinInterval
• builtinSub
• builtinSubIn
• builtinIOne
• builtinPartial
• builtinPartialP
• builtinIsOne
• builtinItIsOne
• builtinIsOne1
• builtinIsOne2
• builtinIsOneEmpty
• builtinId
• builtinConId
• primIMin
• primIMax
• primINeg
• primPOr
• primComp
• primTransp
• primHComp
• primIdJ
• primPartial
• primPartialP
• primDepIMin
• primIdFace
• primIdPath
• primIdElim
• primSubOut

Let me guess how these could be compiled:

• Paths/dependent paths: Functions from the unit type. (Does the thunking serve some purpose?)
• The interval/IsOne: The unit type.
• Partial/PartialP/Sub: The underlying type.
• primPOr: Could this function just return one of its arguments?
• Transport/composition: The identity function.
• Id: The unit type?

[Saizan]

I'm not sure you should forbid the primitives from Agda.Builtin.Cubical.HCompU, those do not introduce higher paths and are there to support composition in the universe.

Partial/PartialP already reduce to function types from IsOne .. so it would make sense to compile them as functions from unit.

Id should be compiled much like paths, as it's a path with a flag for when it counts as reflexive. However if composition is the identity the extra flag can be ignored.

primPOr (and elements of Partial in general) are tricky because you can define

f : (i : I) ->  Partial (i `max` ~ i) Bool
f i = primPOr (\ _ -> true) (\ _ -> false)

and then f i0 itIsOne = true and f i1 itIsOne = false, maybe the interval should be compiled as booleans rather than unit? On the other hand the interesting uses of primPOr and elements of Partial are for the argument to hcomp which we would ignore when compiling, so they wouldn't be a problem if we had a good way to restrict them to only appear there.

[nad]

See also #5601.