dot notation deficiency

Stream: general

[Kevin Buzzard]

I've noticed the following phenomenon before (indeed, I think it's been explained to me before) and I just noticed it again when writing this code : if I : ideal R then I can use I.quotient for ideal.quotient I but I can't seem to use I.quotient.mk for ideal.quotient.mk I.

1) Am I right about this or was I just mistaken, or not trying hard enough?

2) If this is true that you can't use dot notation like this, should ideal.quotient.mk be called ideal.quotient_mk and similarly ideal.quotient.lift?

3) Will Lean 4 be any different in this regard?

import ring_theory.ideal.operations

-- let R be a commutative ring and let I,J be ideals of R
variables {R : Type} [comm_ring R] (I J : ideal R)

example : R →+* I.quotient := ideal.quotient.mk I  -- works
example : R →+* I.quotient := I.quotient.mk  -- fails
/-
invalid field notation, type is not of the form (C ...) where C is a constant
  I.quotient
has type
  Type
-/

[Mario Carneiro]

This isn't supposed to work in the first place. The ideal R argument of ideal.quotient.mk is implicit

[Mario Carneiro]

If you want it to work that argument should be explicit

[Kevin Buzzard]

docs#ideal.quotient.mk says it's explicit?

[Eric Wieser]

Submodule avoids this by calling it docs#submodule.mkq instead

[Eric Wieser]

Introducing an abbreviation for Type makes this work:

import ring_theory.ideal.operations

universes u

-- just to carry dot notation
abbreviation ideal.quotient'_type {α : Type u} [comm_ring α] (I : ideal α) := Type u

-- replacement for `ideal.quotient`
abbreviation ideal.quotient' {α : Type u} [comm_ring α] (I : ideal α) : I.quotient'_type := I.quotient

-- in addition to `ideal.quotient.mk`
abbreviation ideal.quotient'_type.mk {α : Type u} [comm_ring α] {I : ideal α}
  (_ : I.quotient'_type := I.quotient') :
  α →+* I.quotient' :=
ideal.quotient.mk I

variables {R : Type} [comm_ring R] (I J : ideal R)

example : R →+* I.quotient' := I.quotient'.mk  -- works

[Mario Carneiro]

Oh I see, field projections have to have atomic names. foo.bar.baz can only be a projection named baz applied to a foo.bar (or a baz projection on a bar projection on a foo), not a projection named bar.baz applied to a foo

[Eric Wieser]

Is the solution here for lean to do something like the following when parsing foo.bar.baz with foo : Foo:

• infer the type of Foo.bar foo
• If it is of type Type, then discard it and evaluate Foo.bar.baz f
• If it is not of type Type but of type Bar, then evaluate Bar.baz (Foo.bar f)

[Eric Wieser]

I'm not sure that's better than embracing a variant of my hack

[Mario Carneiro]

this has to happen at parse time, so the typing information available is fairly limited

[Eric Wieser]

Well it's sophisticated enough to understand coercions I think?

[Mario Carneiro]

not coercions, structure extends

[Eric Wieser]

What I mean by that is that foo.bar_hom works where Foo.bar_hom : add_monoid_hom Foo Foo (and foo : Foo)

[Mario Carneiro]

what is the type of foo in that example?

[Mario Carneiro]

because if it's Foo then that's just regular dot notation

[Mario Carneiro]

it's not like it actually understands that there is a coercion there, it just writes Foo.bar_hom foo and hopes for the best

[Mac]

Mario Carneiro said:

Oh I see, field projections have to have atomic names. foo.bar.baz can only be a projection named baz applied to a foo.bar (or a baz projection on a bar projection on a foo), not a projection named bar.baz applied to a foo

This has to be the case, otherwise there would be ambiguity as to whether foo.bar.baz means baz foo.bar or bar.baz foo.

[Kevin Buzzard]

Ambiguity is fine, there is ambiguity whenever I use something like coe or ext with a few namespaces open, and lean seems to do really well figuring out which one I mean

[Mac]

@Kevin Buzzard The problem here is that the ambiguity increases as the length of the chain increases. For example, foo.bar.baz.bam could be either bar.baz.bam foo, baz.bam foo.bar, or bam foo.bar.baz. Furthermore, unlike many other places in Lean where ambiguity works, there really isn't a clean way for it to Lean to disambiguate between the possible interpretations here (especially since name resolution / dot notation occurs at the parse time -- where type information is not available).

[Kevin Buzzard]

But I've seen lean 3 complain about my ambiguous code before -- "you wrote bar but neither _root_.bar nor foo.bar work" -- so there must be some way that the parser can handle ambiguity?

[Mac]

@Kevin Buzzard I assume you mean property inheritance like this:

structure Foo
def Bar := Foo
def test (x : Bar) := x.val
/-
invalid field 'val', the environment does not contain 'Bar.val'
...
invalid field 'val', the environment does not contain 'Foo.val'
...
-/

In this case, it first tries to resolve val as Bar.val an when that is missing tries Foo.val and then when that fails reports all its attempts. If Bar.val exists, it will always be picked (as Foo.val is only used as a fallback). Technically, as a result, no ambiguity ever occurs.

This doesn't parallel neatly with the foo.bar.baz example for two reasons. First, it isn't clear which of baz foo.bar or bar.baz foo should be the default and which should be the fallback. Second, the existence of property inheritance actually complicates matters. Let's say baz foo.bar is the default and bar.baz foois the fallback. If baz foo.bar fails because baz it is not a member of foo.bar's type, should I fallback to the type's parent's baz or should I fallback to bar.baz foo?

One could resolve such ambiguity with some pre-defined name resolution order. However, it is unclear what that order would be and any such order would make name resolution very time consuming in complex dot notation chains.

[Kevin Buzzard]

Thanks a lot for the detailed comments!

[Mac]

@Kevin Buzzard Thanks! You're welcome! It's fun to talk about the pitfalls of language design. :grinning_face_with_smiling_eyes:

[Eric Wieser]

Mario pointed out in another thread that there's a notation for specifically this problem:

import ring_theory.ideal.operations

-- let R be a commutative ring and let I,J be ideals of R
variables {R : Type} [comm_ring R] (I J : ideal R)

example : R →+* I.quotient := ideal.quotient.mk I  -- works
example : R →+* I.quotient := I^.quotient.mk  -- works!

I propose we refer to this as "super dot" notation because 1) it is super, 2) it gives . super powers, and 3) "super" is a good mnemonic for ^ which is used as superscript in LaTeX.

[Eric Wieser]

The notation was deprecated in Lean v3.2.0, but perhaps we should ignore that

[Yaël Dillies]

Note that it makes you write funky stuff. (equiv.refl _)^.set.compl.symm.trans doesn't work (because equiv.set.compl.symm.trans can't be found), so you must write (equiv.refl _)^.set.compl .symm.trans.

[Floris van Doorn]

Does (equiv.refl _)^.set.compl^.symm^.trans work, so that you're not mixing the two different dot notations?

[Kyle Miller]

#check (equiv.refl _)^.set.compl^.symm^.trans -- OK
#check ((equiv.refl _)^.set.compl).symm.trans -- OK

So once you start with the superdot, you either have to continue with the superdot or use parentheses to interrupt it.

[Patrick Massot]

I found another issue with dot notation: you can't split lines that are over 100 columns, as in

rw I.adic_basis.to_subgroups_basis.to_ring_filter_basis.to_add_group_filter_basis.nhds_zero_has_basis.mem_iff,

[Eric Wieser]

Can't you fix that with parentheses?

[Yaël Dillies]

Are you sure? I think you can add spaces before any dot, as I did above.

[Kevin Buzzard]

Can you also fix it with unbundled is_ring_filter_basis typeclasses on filter bases? This was just the sort of pile-up I was getting when I removed unbundled ring homs and group homs, but it was far less severe (I never had chains anywhere near as long as this) and furthermore there were shortcuts -- e.g. you could maybe make I.adic_basis.to_add_group_filter_basis work directly?

[Kyle Miller]

Yaël Dillies said:

Are you sure? I think you can add spaces before any dot, as I did above.

The one exception seems to be that you can't add spaces before "regular" dots, like the one in equiv.refl.

-- OK
#check (equiv.refl _)
  ^.set.compl
  .symm.trans
-- not ok
#check (equiv.refl _)
  ^.set .compl
  .symm.trans

[Patrick Massot]

Kevin, there is no class here, only structures extending each other and definitions.

[Patrick Massot]

But I can define shortcuts of course.

[Yaël Dillies]

Yeah sure, but adding spaces applies to Patrick's case, right?

[Kevin Buzzard]

Patrick Massot said:

Kevin, there is no class here, only structures extending each other and definitions.

Yes exactly, like there is no predicate class [is_ring_hom] any more, only structures like ring_hom extending monoid_hom etc. For morphisms we now seem convinced that this is the right way. I am suggesting that perhaps for these predicates on filter bases at 0 -- "I interact well with the group structure", "I interact well with the ring structure" could be predicate classes and the code might look cleaner.