Surprising namespaces in elaboration of type of function

Stream: lean4

[Kyle Miller]

In the following example, I wasn't expecting Foo in the type of Foo.f to elaborate in the Foo namespace.

inductive Foo
  | Foo (n : Nat)

def Foo.f : Foo → Nat
  | .Foo n => n + 1

This has the error on line 4, "type expected, got (Foo : Nat → _root_.Foo)", suggesting it's seeing Foo.Foo rather than Foo.

Changing Foo to _root_.Foo is a workaround, but I would have expected elaboration to respect whichever namespace I happened to explicitly be in.

(I was using the Lean.Data.Xml.Basic module, and it has inductive types whose constructors have the same names.)

[Sebastian Ullrich]

Kyle Miller said:

(I was using the Lean.Data.Xml.Basic module, and it has inductive types whose constructors have the same names.)

Ok, this is just wrong

[Kyle Miller]

I meant the constructors have the same names as their corresponding types, which seems fine -- many Haskell data types do that for example.

[Sebastian Ullrich]

Yes, to be clear I meant we should definitely change this. Lean is not Haskell.

[Sebastian Ullrich]

Coming back to your original post, def Foo.f now behaves like namespace Foo def f, yes.

[Jireh Loreaux]

I have to say, when I first learned Haskell I found it super confusing that types and their constructors had the same names. So I'm especially glad we're not adopting this.

[Sebastian Ullrich]

It only really makes sense if you have separate name spaces for types and terms anyway, which we don't (and now Dependent Haskell doesn't either!)

[Kyle Miller]

Sebastian Ullrich said:

Coming back to your original post, def Foo.f now behaves like namespace Foo def f, yes.

I'm just reporting this as being surprising. I have an idea of why it's convenient for it to work like this, but I'm not sure I like it applies to the arguments and type of a declaration -- it'd be less surprising if it just applied to the body of a declaration.

One thing I don't like about it is that if you're adding a declaration that's meant to be used for generalized field notation, then if that object's namespace has a name that shadows another name it becomes more convoluted to refer to that one. There's a pattern we've used in mathlib where there's some predicate, say is_foo, and another predicate, say is_bar, and if is_foo implies is_bar we might have is_bar.is_foo so that if h : is_bar x one can write h.is_foo. Another pattern is that if is_foo (foo x) is true when is_foo x is true, then we define is_foo.foo : is_foo x -> is_foo (foo x). Here's an example of the latter for set.finite.prod : set.finite s -> set.finite t -> set.finite (set.prod s t) docs#set.finite.prod

[Kyle Miller]

I'd be happier if there were a construct like

with namespace foo
def bar ...

to temporarily change the namespace for a command explicitly. This implicit behavior for def foo.bar means you have to notice small lexical details of the name being defined to make sense of the type of a definition.

Anyway, it's not a big deal, but I thought I'd mention my experience. It seems like the kind of feature I'm going to be occasionally re-surprised by.

[Sebastian Ullrich]

Oh, I do get surprised by it as well