Spaceless field projections from variables and constants?

[mikeshulman]

As discussed at #27, this issue is to consider the possibility of allowing foo.bar to fall back to being interpreted as a field projection foo .bar if there is no constant named foo.bar (i.e. bar in namespace foo) currently in scope.

• The parser would be unchanged. In particular, f a.b would still parse as f (a.b) even if the a.b is being interpreted as a .b. This contrasts with f a .b which is interpreted as (f a) .b and is not currently going to change. So this is a possible source of confusion.
• If there's going to be a "default" between the two possible interpretations, the constant one is the correct default, since the field projection one can always be disambiguated by adding a space. Since there is no obvious way to disambiguate the constant one if it's what's intended, I also don't see a way to issue a warning or given an error in case of ambiguity, since there would be no way to silence the warning if the constant interpretation is the intended one (short of renaming things).
• Multiple field projections would be chainable this way: a.b.c could mean a .b .c if there are no constants a.b.c or a.b in scope (if there is the latter, it would be interpreted as a.b .c, even if the latter doesn't typecheck). However, as soon as one field projection has a space, so must all later ones: you cannot write a .b.c for a .b .c.
• This would permit a cute sort of punning between records and namespaces. For instance, given a (bundled) kind of algebraic structure, we can define an instance of that structure, and then prove additional lemmas about it in a namespace with the same name as the structure:

def Magma : Type ≔ sig (
  t : Type,
  plus : t → t → t,
)

def ℕ : Magma ≔ (
  t ≔ data [ zero. | suc. (_ : ℕ.t) ],
  plus ≔ x y ↦ match y [ zero. ↦ x | suc. y ↦ suc. (ℕ.plus x y) ],
)

section ℕ ≔
  def plus_assoc (x y z : ℕ.t) : Id ℕ.t (ℕ.plus (ℕ.plus x y) z) (ℕ.plus x (ℕ.plus y z)) ≔
    match z [
    | zero. ↦ refl (ℕ.plus x y)
    | suc. z ↦ suc. (plus_assoc x y z)
    ]
end

Then ℕ.plus and ℕ.plus_assoc have the same convenient syntax for the user of the library, even though one of them is a field projection and one of them is a namespaced constant. Moreover, if we one day decide to refactor the library by incorporating some lemmas into the structure:

def Semigroup : Type ≔ sig (
  t : Type,
  plus : t → t → t,
  plus_assoc : (x y z : t) → Id t (plus (plus x y) z) (plus x (plus y z)),
)

def ℕ : Semigroup ≔ (
  t ≔ data [ zero. | suc. (_ : ℕ.t) ],
  plus ≔ x y ↦ match y [ zero. ↦ x | suc. y ↦ suc. (ℕ.plus x y) ],
  plus_assoc ≔ x y z ↦
    match z [
    | zero. ↦ refl (ℕ.plus x y)
    | suc. z ↦ suc. (ℕ.plus_assoc x y z)
    ],
)

the user's syntaxes ℕ.plus and ℕ.plus_assoc would not change.

I'm curious what others think of this. @ElifUskuplu, @FrozenWinters, @TOTBWF, @txa, @akaposi, @favonia?

[mikeshulman]

A note that the current plan for higher coinductive types involves field names with numerical suffixes separated by dots. For instance, a 2-dimensional higher field induces two fields of the doubly-degenerate type, denoted .fld.12 and .fld.21. I don't think that should make this proposal unworkable. If we forbid ordinary field names and constant names from consisting entirely of digits (probably a good idea) then something like a.b.1.c can only be interpreted as a .b.1 .c, so there is no additional ambiguity introduced.