Simple type-directed macro/elaborator?

Stream: lean4

[Joey Eremondi]

I'm wondering if anyone has examples of a simple type directed macro.

I'm basically trying to have t⦃s⦄ elaborate to f t s when t : T1, to g t s when t : T2, and to error otherwise. I've tried copying some of the code from the "Beyond Notations" paper but it doesn't seem to work, and it's also doing something much more complicated than what I have in mind.

Are there good examples for this kind of type-directed overloading?

I know I could make this work for type classes, but that seems like overkill for a case where I know that it will be one of two given types.

[Eric Wieser]

The big advantage of type classes here is you can then write def foo [HasMySyntax T] (t : T)(s : S) := t⦃s⦄ + t⦃s⦄ and this one function will work for T1 and T2

[Jannis Limperg]

Can macros be type-directed at all? I thought they were purely syntax-to-syntax transformations, with no type information present.

[Henrik Böving]

When you overload the same syntax with different macros lean will try to elaborate all versions and iff only a single one succeeds it will take that and be happy so I guess that can be viewed as a very rudimentary version of that. But in general using type classes is much preferred over this and alternatively an elaborator directly. Trying to elaborate all of the variants to expand the syntax can be slow.

[Kyle Miller]

mathlib4#5133 has an experimental type-directed elaborator for adjoining elements or sets to a field. It supports F⟮S⟯ and F⟮α⟯, which elaborate to adjoin F S for the set S and adjoin F {α} for the non-set α. Here, the non-set version is taken to be the default, which part of the reason why there is the complexity of a custom elaborator instead of just using notation overloading or typeclasses.

[Kyle Miller]

Like what Henrik said, you can use the fact that notations/macros will all be elaborated if there is an ambiguity, so this works as a simple-type-directed macro:

structure T1 where
  x : Nat → Nat

structure T2 where
  y : Nat → Nat

notation t "⦃" s "⦄" => T1.x t s
notation t "⦃" s "⦄" => T2.y t s

def a : T1 := ⟨id⟩
def b : T2 := ⟨id⟩

#check a⦃2⦄
#check b⦃2⦄

It's got the downside that Eric mentioned, where you can't make theorems or definitions that are polymorphic in the interpretation of the notation.