Custom identifiers?

Stream: lean4

[Mac]

When trying to define Haskell-like operator identifiers I encountered the following error:

syntax "(~)" : ident
-- unknown category 'ident'

Is there some reason why ident is not a proper syntax category? I would like to able to do something akin the following:

syntax "(~)" : ident
infix:50 " ~ " => $(Lean.mkIdent `(~))
def trans (A : Sort _) ((~) : A -> A -> Prop) (a b c : A) := a ~ b -> b ~ c -> a ~ c

[Sebastian Ullrich]

An intriguing idea. What I don't quite like about it is that you need an unhygienic macro for it, and you need to do it for each operator separately. I'd rather like to have a general mechanism a la

(infix "~" : A -> A -> Prop)

[Mario Carneiro]

Oh no we're turning into agda

[Sebastian Ullrich]

Actually it's not clear to me whether Agda allows local mixfix notations (@Jakob von Raumer ?)

A type name, function name, or constructor name can comprise one or more name parts if we separate them with underscore characters _, and the resulting name can be used as an operator.

[Jakob von Raumer]

What do you mean by "local"?

[Sebastian Ullrich]

For a let- or lambda-bound function as above

[Jannis Limperg]

Yeah, no problem.

data ⊤ : Set where
  tt : ⊤

stuff : ⊤
stuff =
  let _//_ : ⊤ → ⊤ → ⊤
      x // y = tt
  in (tt ~ tt + tt) // tt
  where
    _~_+_ : ⊤ → ⊤ → ⊤ → ⊤
    x ~ y + z = tt

Works with lambda binders as well.

[Jakob von Raumer]

foo : (X : Set)(x : X) → Set
foo X x = let _~_ = λ (x y : X) → X in
        x ~ x

[Sebastian Ullrich]

Nice. I would have been surprised if it didn't work, but the docs quoted above seemed relatively specific.

[Jakob von Raumer]

Agda has the same rules for every sort of identifier, be it constructor, definition, ...

[Sebastian Ullrich]

I guess it's still a "function name"

[Jakob von Raumer]

I mean, the Lean community seems pretty dismissive about mixfix as theorem names, which I get, but mixfix variable seem to have some good use cases too

[Mario Carneiro]

I just don't think that notations should be the actual canonical names of things

[Mario Carneiro]

I think local notations (like literally local to an expression) are a fine way to address this use case

[Jakob von Raumer]

But isn't the reasoning behind that the same as the reasoning why a "thing" shouldn't be just named with a single letter and we do that all the time locally?

[Mario Carneiro]

For that, I think a macro expansion to name the identifier something inaccessible and let you supply the mixfix notation would be ideal

[Mario Carneiro]

but the grammar of identifiers shouldn't need to change to support this

[Mac]

Sebastian Ullrich said:

An intriguing idea. What I don't quite like about it is that you need an unhygienic macro for it, and you need to do it for each operator separately. I'd rather like to have a general mechanism a la

(infix "~" : A -> A -> Prop)

I fully support this idea! However, this does could restrict the kinds of notation you can locally bind. For example, this would likely not allow for local binding of lambda-like macros (akin to forall/exists/sigma, etc.).

[Mac]

Mario Carneiro said:

I just don't think that notations should be the actual canonical names of things

Mario Carneiro said:

For that, I think a macro expansion to name the identifier something inaccessible and let you supply the mixfix notation would be ideal

You can already do both of these. For the unlikely to access approach:

infix:50 " ~ " => $(Lean.mkIdent `«~»)
def trans (A : Sort _) («~» : A -> A -> Prop) (a b c : A) := a ~ b -> b ~ c -> a ~ c

For the standard naming approach:

infix:50 " < " => $(Lean.mkIdent `lt)
def trans (A : Sort _) (lt : A -> A -> Prop) (a b c : A) := a < b -> b < c -> a < c

I don't like the former because it requires too much usage of French double quotes, and I don't like the latter because the connection between the notation and the identifier is not immediately clear (its unhygienic). I even dislike my original suggestion somewhat because of the unhygienic macro usage that destroys pretty printing.

[Mario Carneiro]

The second example isn't quite what I meant. I mean a hygienic macro that both declares a new binder like (lt : $type) and also the notation for it, infix $notation => lt. That way the name lt becomes bound in the macro so you can't refer to it, and the surface syntax becomes somewhat similar to agda where you just use the notation directly in the binder

[Sebastian Ullrich]

Mac said:

I fully support this idea! However, this does could restrict the kinds of notation you can locally bind. For example, this would likely not allow for local binding of lambda-like macros (akin to forall/exists/sigma, etc.).

Yes, it will need cooperation from each macro's parser at least. But if we can do it for built-in syntax, it will also be possible for any user-defined one.