More reliable "methods"?

Stream: lean4

[David Thrane Christiansen]

I really like the way that "method call" syntax works in Lean, with the type of the argument before the dot supplying a namespaces in which to find the function.

However, there are three difficulties that arise from the fact that the user isn't saying that this is precisely what they're intending:

1. Moving a type to a new namespace will break use sites, rather than definition sites, of these "methods"
2. A typo in a definition's namespace will make it silently uncallable, again affecting use sites rather than definition sites
3. To add a "method" while working in some other namespace, one must either write a fully-qualified name with _root_ at the beginning or end the namespace and restart it. While this may be an advantage in that it reduces confusing file structures, it can get in the way of intense code binges :)

I think the following metaprogram that I put together this morning addresses all of these:

import Std.Tactic.GuardMsgs
import Lean

namespace Where.Does.This.Go

open Lean Parser Elab Command

def method := leading_parser
  declModifiers false >> "defmethod " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix

/-- Like 'def', except the namespace is resolved to an existing unique
name, and the resulting name is defined in that namespace.

In particular, `defmethod A.B.f ...` first resolves `A.B`. If there is
a unique resolution, say `Lib.More.A.B`, then it is equivalent to
`def Lib.More.A.B.f ...`. If there is no unique resolution, it is an
error.
-/
syntax (name := methodDecl) method : command

def _root_.Lean.Syntax.args : Syntax → Array Syntax
  | .node _ _ args => args
  | _ => #[]

@[command_elab methodDecl]
def elabMethodDecl : CommandElab := fun stx => do
  let ident := stx[0][2][0]
  let .ident origInfo origSubstr x _ := ident
    | throwErrorAt ident "Expected identifier"
  let .str ns@(.str ..) y := x
    | throwErrorAt ident "Expected definable identifier with namespace"
  let options ← (resolveGlobalName ns : CommandElabM _)
  match options with
  | [] => throwErrorAt ident "'{ns}' not found"
  | found@(_ :: _ :: _) =>
    let exprs ← liftTermElabM <| found.mapM fun (i, _) => do
      let i' := mkCIdent i
      Term.elabTerm (← `(term| $i' )) none
    let names : MessageData := .group <| .joinSep (exprs.map (.ofFormat .line ++ toMessageData ·)) ","
    throwErrorAt ident "'{ns}' is ambiguous - found:{names}\n\nPlease write a more specific namespace."
  | [(resolved, _)] =>
    let withNewName := stx.modifyArg 0 (·.modifyArg 2 (·.modifyArg 0 (fun _ => .ident origInfo origSubstr (unambiguous resolved y) [])))
    let decl ← withNewName.replaceM fun
      | .atom info "defmethod" => pure (some (.atom info "def"))
      | .node info ``method args => pure (some (.node info ``Parser.Command.declaration args))
      | _ => pure none
    let decl' := open Parser.Command in
      Syntax.node .none ``declaration #[decl[0][0], .node .none ``«def» decl[0].args[1:7]]
    elabCommand decl'
where
  inRoot : Name → Name
    | .anonymous => .str .anonymous "_root_"
    | .str ns n => .str (inRoot ns) n
    | .num ns n => .num (inRoot ns) n
  unambiguous (ns : Name) (y : String) : Name :=
    .str (inRoot ns) y
  replaceIdent (n : Name) : Syntax → CommandElabM Syntax
    | .ident info str _ preres => pure <| .ident info str n preres
    | other => throwErrorAt other "Not an identifier: {other}"


namespace A.B.C
  structure D where
    field : Nat
  deriving Repr

  structure List (α : Type u) where
    notReallyList : α
end A.B.C

namespace Other

open A.B.C


defmethod D.double : D → D
  | ⟨n⟩ => ⟨n*2⟩

/--
error: 'List' is ambiguous - found: A.B.C.List, _root_.List

Please write a more specific namespace.
-/
#guard_msgs in
defmethod List.wat (xs : List Nat) : Nat := 3

end Other

/-- info: { field := 6 } -/
#guard_msgs in
#eval (A.B.C.D.mk 3).double

What do you think?

[Mario Carneiro]

I like it, although the keyword name could use some work. I might also more clearly separate the namespace from the method name to make it clear that they are being parsed separately

[Mario Carneiro]

how about

def(in List) wat (xs : List Nat) : Nat := 3

[Mario Carneiro]

that also makes it easier to generalize to theorem, opaque etc

[David Thrane Christiansen]

I think I like my bike shed color a bit better than this one, but I appreciate the point about generalizability. Perhaps another solution would be a modifier, rather than a new declaration form.

[Scott Morrison]

I think keyword proliferation is worth avoiding. People already have trouble with def/theorem (and what on earth is lemma? :-), and we've coped flak for our cornucopia of brackets () {} [] {{}} ‹› «».

[David Thrane Christiansen]

If the set of definition modifiers were extensible then this would fit in nicely, now that I think about it more

[Kyle Miller]

Could this be implemented with a command? You'd have in_namespace ident command to evaluate command within the namespace specified by ident.

in_namespace List
def wat (xs : List Nat) : Nat := 3

[Kyle Miller]

That way you don't have to touch the def command, and it generalizes to all defining commands.

[David Thrane Christiansen]

That could work too, I suppose :-)

[David Thrane Christiansen]

maybe something like namespace for List that checks that List is an inductive type, and then gets into its namespace?

[Mario Carneiro]

that checks that List is an inductive type

Why would you check for this? You can use dot notation on any type.

[Eric Wieser]

I think having in_namespace Foo do magic name resolution but namespace Foo in not do so will be very confusing

[Eric Wieser]

A more radical fix here would be "namespace Foo must be predeclared before using def Foo.bar", where predeclared means you used either namespace Foo or a declaration Foo is in the environment.

[Eric Wieser]

Or maybe even just the second condition, replacing the first with a new_namespace command to really avoid any accidents

[Mario Carneiro]

Namespace declarations would be great, that would solve the problem of where to make go to def on namespace/open commands go, add hover docs, as well as avoiding misspelling problems

[Mario Carneiro]

but it would be a somewhat disruptive breaking change to require

[Mario Carneiro]

On the other hand, I'm not sure I would want namespace Foo to do regular name resolution for Foo, because this would make it more difficult to determine what namespace is being selected, which makes it harder to understand where definitions in the namespace went, which affects downstream open declarations, etc. That is, you would have to unravel quite a bit to do name resolution "by hand", which impacts readability of lean code outside the editor (and even in it, when using the sticky header feature for determining the current file namespace)

[Kyle Miller]

@David Thrane Christiansen I hacked together an in_namespace_for command, and in your example in_namespace_for D def double : D → D | ⟨n⟩ => ⟨n*2⟩ defines a function A.B.C.D.double. Your point number 1 in your first message I think is important (make it so moving D is likely to break definition sites).

import Std.Tactic.GuardMsgs
import Lean

namespace Lean.Elab.Command

/-- Resolves the given name and runs the command within that resolved name's namespace. -/
elab "in_namespace_for " n:ident cmd:command : command => do
  let ns ← resolveGlobalConstNoOverloadWithInfo n
  let nscopes := (← getScopes).length
  modify fun s => { s with
    env := s.env.registerNamespace ns,
    scopes := { s.scopes.head! with header := "", currNamespace := ns} :: s.scopes
  }
  pushScope
  activateScoped ns
  try
    elabCommand cmd
  finally
    unless (← getScopes).length == nscopes + 1 do
      throwError "Command should not alter scopes"
    modify fun s => { s with scopes := s.scopes.drop 1 }
    popScope

end Lean.Elab.Command

universe u

namespace A.B.C
  structure D where
    field : Nat
  deriving Repr

  structure List (α : Type u) where
    notReallyList : α
end A.B.C

namespace Other

open A.B.C

in_namespace_for D def double : D → D
  | ⟨n⟩ => ⟨n*2⟩

/-- error: ambiguous identifier '`List', possible interpretations: [A.B.C.List, List] -/
#guard_msgs in
in_namespace_for List def wat (xs : List Nat) : Nat := 3

end Other

/-- info: { field := 6 } -/
#guard_msgs in
#eval (A.B.C.D.mk 3).double

[Kyle Miller]

@David Thrane Christiansen It turns out mathlib has a command for running another command within a namespace. With it, there's a quick implementation of this (with slightly different characteristics as my other one):

import Mathlib.Util.WithWeakNamespace

namespace Lean.Elab.Command

/-- `in_namespace_for ident cmd` resolves the identifier and runs the command
within that resolved identifier's namespace. -/
elab "in_namespace_for " n:ident cmd:command : command => do
  let ns := rootNamespace ++ (← resolveGlobalConstNoOverloadWithInfo n)
  elabCommand <| ← `(command| with_weak_namespace $(mkIdent ns) $cmd)

end Lean.Elab.Command

code with examples

import Std.Tactic.GuardMsgs
import Mathlib.Util.WithWeakNamespace

namespace Lean.Elab.Command

/-- `in_namespace_for ident cmd` resolves the identifier and runs the command
within that resolved identifier's namespace. -/
elab "in_namespace_for " n:ident cmd:command : command => do
  let ns := rootNamespace ++ (← resolveGlobalConstNoOverloadWithInfo n)
  elabCommand <| ← `(command| with_weak_namespace $(mkIdent ns) $cmd)

end Lean.Elab.Command

universe u

namespace A.B.C
  structure D where
    field : Nat
  deriving Repr

  structure List (α : Type u) where
    notReallyList : α
end A.B.C

namespace Other

open A.B.C

in_namespace_for D def double : D → D
  | ⟨n⟩ => ⟨n*2⟩

/-- error: ambiguous identifier '`List', possible interpretations: [A.B.C.List, List] -/
#guard_msgs in
in_namespace_for List def wat (xs : List Nat) : Nat := 3

end Other

/-- info: { field := 6 } -/
#guard_msgs in
#eval (A.B.C.D.mk 3).double

[David Thrane Christiansen]

This is indeed a nice way to do it!