Namespace-based overloading does not find exports

Stream: lean4

[Alex Keizer]

I've exported a function hd in the namespace Vec, but when I try to call v.hd with v : Vec ..., it fails.

/-- A `Vec` is just a `List α` of statically known size -/
def Vec (α : Type _) (n : Nat) : Type _
  := Fin n → α


abbrev TypeVec : Nat → Type _
  := Vec (Type _)


/-- A dependent vector is a heterogenous list of statically known size -/
def DVec {n : Nat} (αs : TypeVec n) : Type _
  := (i : Fin n) → (αs i)


/-- A vector that repeats a single element `a` -/
def Vec.const {α : Type _} (a : α) (n : Nat) : Vec α n
  := fun _ => a


/- `Vec` is defeq to a `DVec` with constant type -/
unif_hint (α : Type _) (n : Nat) where
  |- Vec α n =?= DVec (Vec.const α n)



namespace DVec
  def hd {n : Nat} {αs : TypeVec (n+1)} (v : DVec αs) : (αs 0)
    := v 0
end DVec

namespace Vec
  export DVec (hd)
end Vec


-- works
example (v : Vec Nat 1) : Nat
  := DVec.hd v

-- Vec.hd exists
#check Vec.hd

/- Yet, this fails with:
    invalid field 'hd', the environment does not contain 'Vec.hd'
      v
    has type
      Vec Nat 1
-/
example (v : Vec Nat 1) : Nat
  := v.hd

More generally, is there a way to have all DVec functions available to be called with the field/dot on Vecs?
So far, I've only found

abbrev Vec.hd := DVec.hd

to work, but I'd rather avoid having to create a new alias for every function on DVecs

[Sebastian Ullrich]

No, this is not currently possible. Have you considered defining Vec as an abbrev in terms of DVec instead?

[Alex Keizer]

The problem there is that DVec takes a Vec as argument, so it would become a mutually inductive definition, which feels like an entirely different can of worms that I'd hoped to avoid

[Sebastian Ullrich]

Ah, I missed that

[Kyle Miller]

There's an experimental feature I've been working on in Lean 3 where you can add additional sources for dot notation. With it, if you do

attribute [elab_field_alternatives DVec] Vec

then when you use v.hd, if hd can't be resolved in any of the usual ways, it looks for DVec.hd. Then it uses the simpler procedure of doing DVec.hd v rather than the usual one of inserting it as the first explicit argument of a particular type.

The way I have it set up is that elab_field_alternatives is a list of names that is searched in a non-recursive manner (that way the elaborator can't get stuck in an infinite loop). It's meant to be similar to Python's __mro__, where the class hierarchy is resolved into a particular list of classes to search.

[Kyle Miller]

The motivation here is that while structures can extend others to receive additional "methods" due to the way dot notation resolves, there's not really a way to add additional "methods" that are consequences to a type implementing additional traits. This feature lets you have a sort of statically resolved OO-style mixin system.

[Sebastian Ullrich]

Yes, by "not currently possible" I meant that we have considered it before and would like to use it ourselves :) . I believe the most relevant prior work here is https://doc.rust-lang.org/std/ops/trait.Deref.html#more-on-deref-coercion. But an attribute may be at least as appropriate as a type class in the case of Lean, yes.

[Kyle Miller]

For mathlib, this feature would be helpful to be able to use dot notation for modeling certain families of mathematical objects. For example, graphs have an adjacency relation, and it's nice being able to write G.adj v w to say that "G considers v and w to be adjacent," however there are many different kinds of graphs (simple graphs, multigraphs, reflexive graphs, graphs defined using a function V -> V -> Type, graphs defined using functions s t : E -> V, etc.) and trying to model them as a hierarchy of structures that extend one another requires tradeoffs that would be nice not to have to make.

A simple example that would be more convincing if there were another type of graph to justify not just naming the field adj:

class has_adj (G : α) (V : out_param $ Type v) :=
(adj : V → V → Prop)

structure simple_graph (V : Type u) :=
(adj' : V → V → Prop)
(symm' : symmetric adj')
(irrefl' : irreflexive adj')

attribute [elab_field_alternatives has_adj] simple_graph

instance : has_adj G V := ⟨G.adj'⟩

Then G.adj v w would resolve as has_adj.adj G v w.

[Sebastian Ullrich]

A related proposal, again somewhat inspired by Rust, was that x.f should be allowed in general if f is a declaration in the current scope. With that, your code would work out of the box after open has_adj.

[Sebastian Ullrich]

In particular, x.toString would finally work for any ToString

[Kyle Miller]

Just to add in another graph type:

structure multi_digraph (V : Type*) :=
(E : Type*)
(s t : E → V)

instance : has_adj (multi_digraph V) := ⟨λ G v w, ∃ (e : G.E), s e = v ∧ t e = w⟩

attribute [elab_field_alternatives has_adj] multi_digraph

[Kyle Miller]

While open has_adj would work, ideally graphs that implement has_adj could permanently have G.adj available. I'd also like to avoid some namespace pollution -- part of the point of this feature isn't just to add additional fields, but to add additional dot-notation-accessible lemmas that are generally true for graphs of different types.

[Leonardo de Moura]

@Alex Keizer Your example above works without any additional annotation. The dot notation now has basic support for following aliases.
https://github.com/leanprover/lean4/commit/f4e083d5072bf299b159d10e6727ea0fa22776b6

[Henrik Böving]

Leonardo de Moura said:

Alex Keizer Your example above works without any additional annotation. The dot notation now has basic support for following aliases.
https://github.com/leanprover/lean4/commit/f4e083d5072bf299b159d10e6727ea0fa22776b6

Just a quick question because I dont see it covered in the test, does this respect protected? So if the old decl was protected is the one in the name space it was reexported to as well?

[Leonardo de Moura]

@Henrik Böving I am assuming this is an orthogonal concern, correct? protected annotations do not affect the dot notation. When we use export, we do not create a new declaration, but an alias to the original one.
When the name-resolution procedure process aliases, it does not check whether the target name is `protected or not. Example:

protected def Foo.bla (x : Nat) := 2*x

namespace Boo
export Foo (bla) -- Add alias Boo.bla for Foo.bla
end Boo

open Boo
#check bla -- Name resolution used the Alias `Boo.bla => Foo.bla` here.

[Henrik Böving]

(deleted)

[Henrik Böving]

Do we have something like a "protected export" then? For some reexported declarations it seems desirable to have this protected behaviour right?

[Leonardo de Moura]

I never felt the need for creating "protected exports". It would be great to have a consensus among users on what to do here. We are also open to change the behavior of aliases during name resolution and make sure Boo.bla is treated as protected in the example above.

[Henrik Böving]

I think it would mostly be consistent, if a previous namespace decided to declare something protected it was probably because it is a commonly used name that they dont wanted to just fly around out of namespaces so why should this behaviour be differet when it is re-exported

But that's just my 5-cents

[Leonardo de Moura]

@Henrik Böving It is a small change, and does not affect the main repo. We can easily remove it if others are unhappy about this change.

[Leonardo de Moura]

https://github.com/leanprover/lean4/commit/5901fef43abe90a3ce659f028cf905e7a2b100ff