Why is dot-notation not working here?

Stream: new members

[Dan Abramov]

def n : Nat := 42
def s : String := "The answer is " ++ toString n

def s' : String := "The answer is " ++ n.toString
/- invalid field 'toString', the environment does not contain 'Nat.toString' -/

Why doesn't this work? Is there a way to add Nat.toString to the environment? I'm mostly curious about the error itself, not necessarily "how to embed numbers into strings".

[Yakov Pechersky]

toString comes from a class, and thus toString n works because toString is able to synthesize an instance of ToString Nat. Dot notation, however, looks (to first principle) by namespaces. And there is no toString in the Nat namespace.

[Dan Abramov]

Is looking by namespace more restrictive? Does the difference exist intentionally so one is stricter than the other, or is it due to some other design reason?

[Yakov Pechersky]

Namespace lookup is very syntactic, in my understanding. Either the declaration exists in the environment by that explicit name, or it doesn't. On the other hand, application of a function that has a typeclass instance argument relies on a typeclass search, that might be computationally intensive or not. It relies on more than just available declaration _names_, but also values: instances.

So I wouldn't call one stricter than the other. The dot notation is syntactic sugar for namespaced declarations, with some special support for situations where the underlying type is a subtype of some other type (so it can look in both namespaces).

[Yakov Pechersky]

Said otherwise, if Nat.toString existed and then was renamed (typo) to Natt.toString, then n.toString for n : Nat would stop working outright with the same error as you saw above. On the other hand, if somehow you didn't have an instance of ToString Nat in your environment, and you invoked toString n, you'd see a instance can't be synthesized error.

[Yakov Pechersky]

Oh, one more thing. Something to notice here is that docs#toString is actually docs#ToString.toString

[Yakov Pechersky]

That is, it is (actually) in the ToString namespace. There happens to also be a global open ToString which basically makes toString invokable globally without having to refer to the ToString namespace.

[Yakov Pechersky]

Imagine that there was some other function Foo.toString. And I opened that namespace as well. When the syntax of toString n gets elaborated, both are tried, and if both functions can be invoked with a Nat argument, you get an error about conflicting names. But (iirc) if only one of them works for Nat, then you get the one you meant to use. And there's no clash.

[Kyle Miller]

There's another important factor: dot notation looks for a parameter of the value's type. If n.toString could resolve to the global toString, there's no Nat parameter.

[Kyle Miller]

It's possible to create an alias to ToString.toString in the Nat namespace, which gets dot notation to resolve, but you can see the error:

def n : Nat := 42

namespace Nat
export ToString (toString)
end Nat

def s' : String := "The answer is " ++ n.toString
/-
Invalid field notation: Function `toString` does not have
a usable parameter of type `Nat` for which to substitute `n`

Note: Such a parameter must be explicit, or implicit with
a unique name, to be used by field notation
-/

[Matt Diamond]

btw the dot-notation feature you're attempting to use in s' is referred to in the manual as "Generalized Field Notation"... there's a section that lays out exactly how it gets parsed, if you need any more clarification:

https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#generalized-field-notation

[Robin Arnez]

I'll just add that you might be looking for docs#Nat.repr for which dot notation does work