Deriving dot notation from class instances

Stream: Is there code for X?

[Fabrizio Montesi]

I'd like an attribute (or something similar) for instances that generates appropriate abbreviations for dot notation. For example:

structure Str where
  n : Nat

@[dotify Str]
instance : ToString Str where
  toString str := ToString.toString str.n

-- The use of dotify above generates:
-- def Str.toString : Str → String := ToString.toString

#eval { n := 3 : Str }.toString -- This works because of the generated abbrev. Otherwise, it'd throw an error as usual.

Does this exist already perhaps? It look feasible but nontrivial, as identifying the definitions that should be abbreviated requires some care. I guess one could also provide a parameter to force the inclusion/exclusion of some definitions.

We could really use this in CSLib, to avoid a proliferation of manually-written abbreviations.

[Aaron Liu]

how do you generate the name? Does it only do one-field classes

[Fabrizio Montesi]

You mean Str? I passed it as an argument to the annotation.

[Aaron Liu]

Fabrizio Montesi said:

Does this exist already perhaps? It look feasible but nontrivial, as identifying the definitions that should be abbreviated requires some care. I guess one could also provide a parameter to force the inclusion/exclusion of some definitions.

This probably doesn't exist but probably isn't too hard to make

[Aaron Liu]

Fabrizio Montesi said:

You mean Str? I passed it as an argument to the annotation.

I mean the name Str.toString

[Fabrizio Montesi]

Here's a first informal idea:

Say I use @[dotify T].
This looks for all names under the class namespace (this would find toString), filters to get only those whose signature starts by taking an explicit parameter of type T, and then produces an abbreviation for each under T's namespace.

[Aaron Liu]

ok

[Aaron Liu]

that's an algorithm I can follow

[Robin Arnez]

Something like this?

import Mathlib

open Lean Meta

partial def dotify (inst : Name) (target : Name) : MetaM Unit := do
  let val ← getConstVal inst
  let doCompile := !isNoncomputable (← getEnv) inst
  forallTelescopeReducing val.type (whnfType := true) fun xs body => do
    let instApp := mkAppN (.const inst (val.levelParams.map Level.param)) xs
    let rec traverse (instApp : Expr) (ty : Expr) : MetaM Unit := do
      ty.withApp fun fn args => do
      let .const nm us := fn | throwError "not a class: {body}"
      unless isClass (← getEnv) nm do throwError "not a class: {body}"
      let info := getStructureInfo (← getEnv) nm
      for field in info.fieldInfo do
        let projApp : Expr := .app (mkAppN (.const field.projFn us) args) instApp
        let projType ← inferType projApp
        if field.subobject?.isSome then
          traverse projApp (← whnf projType)
          continue
        let name := target ++ field.fieldName
        if (← getEnv).contains name then
          continue
        let type ← mkForallFVars xs projType
        let value ← mkLambdaFVars xs projApp
        if ← isProp projType then
          addDecl <| .thmDecl {
            name, type, value
            levelParams := val.levelParams
          }
        else
          let decl : Declaration := .defnDecl {
            name, type, value
            levelParams := val.levelParams
            hints := .abbrev
            safety := .safe
          }
          addDecl decl
          if doCompile then
            compileDecl decl
    traverse instApp body

structure Str where
  n : Nat

instance instToStringStr : ToString Str where
  toString str := ToString.toString str.n

#eval! dotify ``instToStringStr `Str

#print Str.toString

def RealClone := Real

noncomputable instance : ConditionallyCompleteLinearOrderedField RealClone := inferInstanceAs (ConditionallyCompleteLinearOrderedField Real)

#eval! dotify ``instConditionallyCompleteLinearOrderedFieldRealClone `RealClone

#print RealClone.one_mul

... although I didn't do the "filters ..." part

[Fabrizio Montesi]

I need to read up some more about macro development to fully understand it, but the effect looks pretty good, thanks!

I've found a few discussions with desiderata that could be (at least partially) addressed by such an annotation:

https://leanprover-community.github.io/archive/stream/270676-lean4/topic/class.20dot.20notation.html
#new members > Why Dot notation doesn't work for instance methods?
#new members > Why is dot-notation not working here?

Hence the question: where should this (or some version of this) go? I'd like to be able to use it in CSLib, but maybe it could be good to put it in batteries? I don't know if there are plans to include a feature like this in Lean.

[Ching-Tsun Chou]

Suppose the dot-notation discussed above works, in the sense that one can use it in an expression and the expression compiles. But will all the theorems reachable via the dot-notation also be available to tactics like grind and simp? In the particular application that motivates this thread, we have a class like Acceptor below. Will the instances of language and mem_language be also be available to grind because of their grind annotations? If I still have to make instances of them and put the grind annotation on them, what exactly does the dot-notation buy me?

/-- An `Acceptor` is a machine that recognises strings (lists of symbols in an alphabet). -/
class Acceptor (α : Type _) (Symbol : outParam (Type _)) where
  /-- Predicate that establishes whether a string `xs` is accepted. -/
  Accepts (a : α) (xs : List Symbol) : Prop

namespace Acceptor
variable {Symbol : Type _}

/-- The language of an `Acceptor` is the set of strings it `Accepts`. -/
@[scoped grind .]
def language [Acceptor α Symbol] (a : α) : Language Symbol :=
  { xs | Accepts a xs }

/-- A string is in the language of an acceptor iff the acceptor accepts it. -/
@[scoped grind =]
theorem mem_language [Acceptor α Symbol] (a : α) (xs : List Symbol) :
  xs ∈ language a ↔ Accepts a xs := Iff.rfl

[Fabrizio Montesi]

They might, I tried with manually-written abbrevs and it worked once (that's why I wanted abbrevs). But it needs further testing. If it doesn't work out of the box, we might need to replicate the grind annotations.

[Ching-Tsun Chou]

If I need to replicate the grind annotation for each instance of Acceptor, then what does Acceptor buy me?

[Robin Arnez]

grind eagerly unfolds all reducible declarations so abbrevs don't need new grind annotations

[Fabrizio Montesi]

For the sake of the argument: If we can't get grind to work I wouldn't use abbreviations for Acceptor at all then, or it'd kill the point of code deduplication. It'd become a choice between code deduplication (Acceptor) or having dot notation (copy defs for all instances).

But there's a good chance it'll work, we should check.

[Fabrizio Montesi]

Robin Arnez said:

grind eagerly unfolds all reducible declarations so abbrevs don't need new grind annotations

Precisely this.

[Ching-Tsun Chou]

@Robin Arnez Just to be clear: Are you saying that if language above is declared using abbrev instead of def, then for every instance of Acceptor, grind will find the corresponding instances of language and mem_language? Note that the latter two are only in the namespace of Acceptor, not in the class declaration proper.

[Fabrizio Montesi]

No, the proxy def should be an abbrev (for example, DA.FinAcc.language in our current case in cslib).

[Fabrizio Montesi]

(and the macro we're discussing produces these proxy defs automatically)

[Ching-Tsun Chou]

So you are saying that I still have to make a abbrev definition for DA.FinAcc.language but I don't have to repeat the mem_language theorem for that instance? If so, is the saving (which is 4 lines of code) worth the introduction of an "acceptor" concept and the need for extending Lean? Note that the introduction of a new concept is not free either. It's one additional of indirection for a human reader of the code to comprehend and one additional file for Lean to load.

[Fabrizio Montesi]

No, you wouldn't need language either. You would just need the instance as we have now (annotated with @[dotify] or whatever we end up calling it).

[Ching-Tsun Chou]

OK, we saved another 4 lines of code. But it still seems to me that the concepts being abstracted into Acceptor are so meager that the saving from code deduplication does not justify the additional level of indirection and the need for extending Lean.

[Chris Henson]

Maybe let's discuss further the particular application to CSlib in that channel as to not get too off-topic for this thread.

[Tomas Skrivan]

Recently I wanted something similar. One field structures are used to do function overloading so I decided to streamline the notation for it and it supports dot notation too.

You first declare the function

declfun foo {α} (a : α) : α

then define it for some types

defun foo (x : Float) := 2*x
defun foo (x : Nat) := 10*x

or for structures

structure Vector2 where
  (x y : Float)
deriving Repr

namespace Vector2
defun foo (x : Vector2) : Vector2 := ⟨foo x.1, foo x.2⟩
end Vector2

Now you can call

-- 100
#eval foo 10
-- 20
#eval foo 10.0
-- { x := 2.000000, y := 4.000000 }
#eval (Vector2.mk 1.0 2.0).foo

For structures either foo (Vector2.mk 1.0 2.0) or (Vector2.mk 1.0 2.0).foo works. The later is exactly the problem in question here.

code

import Lean
open Lean

namespace HouLean.Meta

/--
Declare an overloadable function by creating a single-method typeclass.

## Example
```lean
declfun sin {α} (x : α) : α
```

This creates a typeclass `Sin` with a single method `sin`. You can then define
overloads using `defun`:

```lean
defun sin (x : Float) := x.sin
defun sin (x : Float32) := x.sin
defun Vector2.sin (u : Vector2) : Vector2 := ⟨u.x.sin, u.y.sin⟩
```

## Implementation Details
Internally, `declfun` creates a typeclass and exports its method. For example,
`declfun sin {α} (x : α) : α` generates:
```lean
class Sin (α : Type) where
  sin (x : α) : α
export Sin (sin)
```
-/
syntax (docComment)? "declfun" declId bracketedBinder* ":" term : command

/--
Define an overload for a function declared with `declfun`.

## Example
```lean
-- Simple overload
defun sin (x : Float) := x.sin

-- Member function (automatically creates both the function and the overload instance)
defun Vector2.sin (u : Vector2) : Vector2 := ⟨u.x.sin, u.y.sin⟩
```

## Behavior
- For simple names like `sin`, `defun` creates an instance of the corresponding typeclass
- For qualified names like `Vector2.sin`, it defines the member function and creates an instance

## Implementation Details
`defun` generates typeclass instances. For example, `defun sin (x : Float) := x.sin`
creates:
```lean
instance : Sin Float where
  sin x := x.sin
```
-/
syntax (docComment)? "defun" declId bracketedBinder* (":" term)? ":=" term : command

open Lean.Parser.Term in
/-- Extract leading implicit and instance implicit binders from a binder array. -/
def extractImplicitBinders (binders : TSyntaxArray ``bracketedBinder) :
    Array (TSyntax ``bracketedBinder) × Array (TSyntax ``bracketedBinder) :=
  let implicit := binders.takeWhile fun b : TSyntax ``bracketedBinder =>
    match b with
    | `(bracketedBinder| { $_ }) => true
    | `(bracketedBinder| [ $_ ]) => true
    | _ => false
  (implicit, binders[implicit.size:])

open Lean.Parser.Term in
/-- Convert implicit binders `{x}` to explicit binders `(x)`. -/
def implicitBindersToExplicit (binders : TSyntaxArray ``bracketedBinder) :
    MacroM (TSyntaxArray ``bracketedBinder) :=
  binders.mapM fun b : TSyntax ``bracketedBinder =>
    match b with
    | `(bracketedBinder| { $x }) => `(bracketedBinder| ( $x ))
    | b => pure b

open Lean Elab Command in
elab_rules : command
| `($[$doc:docComment]? declfun $id:ident $bs:bracketedBinder* : $ty:term) => do
  let className := mkIdent <| id.getId.capitalize
  let (classBinders, funBinders) := extractImplicitBinders bs
  let classBinders ← liftMacroM <| implicitBindersToExplicit classBinders

  elabCommand (← `(class $className:ident $classBinders* where
      $[$doc:docComment]?
      $id:ident $funBinders:bracketedBinder* : $ty))

  elabCommand (← `(export $className ($id)))

open Meta Elab Command Term in
elab_rules : command
| `($[$doc:docComment]? defun $id:ident $bs:bracketedBinder* $[: $ty:term]? := $body) => do
  liftTermElabM do
    unless id.getId.isStr do
      throwError "invalid function name {id}"

    let funName := id.getId.getString!
    let className := funName.capitalize
    let funId ← resolveGlobalConstNoOverload (mkIdent <| Name.mkSimple className |>.append (.mkSimple funName))
    let classId ← resolveGlobalConstNoOverload (mkIdent <| Name.mkSimple className)

    -- Elaborate function definition
    let f ← Term.elabBinders bs fun xs => do
      let t? ← ty.mapM (elabTerm · none)
      let b ← elabTermAndSynthesize body t?
      mkLambdaFVars xs b
    let F ← inferType f >>= instantiateMVars

    if F.hasLevelMVar then
      throwError "Universe polymorphic functions are not supported yet!"

    -- Prepare function declaration with mvars
    let funExpr ← mkConstWithFreshMVarLevels funId
    let classExpr ← mkConstWithFreshMVarLevels classId
    let (ys, _, _) ← forallMetaTelescope (← inferType classExpr)
    let classExpr := classExpr.beta ys
    let inst ← mkFreshExprMVar classExpr
    let funExpr := funExpr.beta (ys.push inst)
    let funType ← inferType funExpr

    -- Overload should have the same type, which fills type mvars
    if ← isDefEq funType F then
      let classExpr ← instantiateMVars classExpr
      let mut inst ← mkAppM (classId.append `mk) #[f] >>= instantiateMVars

      let ns ← getCurrNamespace
      let strName :=
        if id.getId.getNumParts > 1 then
          id.getId.getPrefix
        else
          ns

      -- Handle member function case
      if (← getEnv).contains strName then
        -- Resolve namespace properly
        let funName := id.getId.getString!
        let strId ← resolveGlobalConstNoOverload (mkIdent strName)
        let declId := strId.append (.mkSimple funName)
        let hints := ReducibilityHints.regular (getMaxHeight (← getEnv) f + 1)
        let decl ← Lean.mkDefinitionValInferringUnsafe declId [] F f hints
        addDeclarationRangesFromSyntax declId id


        -- Add documentation if provided
        match doc with
        | some doc =>
          addDecl (Declaration.defnDecl decl)
          addDocString declId (mkNullNode bs) doc
          compileDecl (Declaration.defnDecl decl)
        | none =>
          addAndCompile (Declaration.defnDecl decl)

        inst ← mkAppM (classId.append `mk) #[(.const declId [])]

      -- Generate and add instance
      let instName := (← getCurrNamespace) ++ (← NameGen.mkBaseNameWithSuffix "inst" classExpr)
      if (←getEnv).contains instName then
        throwError "Enviroment already contains {instName}"
      let hints := ReducibilityHints.regular (getMaxHeight (← getEnv) inst + 1)
      let decl ← Lean.mkDefinitionValInferringUnsafe instName [] classExpr inst hints
      addAndCompile (Declaration.defnDecl decl)
      addInstance instName AttributeKind.global (eval_prio default)
      addDeclarationRangesFromSyntax instName id
    else
      throwError m!"Invalid function type {F}, expected {funType}!"


end HouLean.Meta



declfun foo {α} (a : α) : α

defun foo (x : Float) := 2*x
defun foo (x : Nat) := 10*x

structure Vector2 where
  (x y : Float)
deriving Repr

namespace Vector2
defun foo (x : Vector2) : Vector2 := ⟨foo x.1, foo x.2⟩
end Vector2

-- 100
#eval foo 10
-- 20
#eval foo 10.0
-- { x := 2.000000, y := 4.000000 }
#eval foo (Vector2.mk 1.0 2.0)