Zulip Chat Archive

Stream: lean4

Topic: Custom identifiers?


view this post on Zulip Mac (Apr 13 2021 at 22:03):

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

view this post on Zulip Sebastian Ullrich (Apr 14 2021 at 07:06):

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)

view this post on Zulip Mario Carneiro (Apr 14 2021 at 08:03):

Oh no we're turning into agda

view this post on Zulip Sebastian Ullrich (Apr 14 2021 at 08:53):

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.

view this post on Zulip Jakob von Raumer (Apr 14 2021 at 08:54):

What do you mean by "local"?

view this post on Zulip Sebastian Ullrich (Apr 14 2021 at 08:55):

For a let- or lambda-bound function as above

view this post on Zulip Jannis Limperg (Apr 14 2021 at 08:58):

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.

view this post on Zulip Jakob von Raumer (Apr 14 2021 at 08:58):

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

view this post on Zulip Sebastian Ullrich (Apr 14 2021 at 08:59):

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

view this post on Zulip Jakob von Raumer (Apr 14 2021 at 08:59):

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

view this post on Zulip Sebastian Ullrich (Apr 14 2021 at 09:00):

I guess it's still a "function name"

view this post on Zulip Jakob von Raumer (Apr 14 2021 at 09:02):

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

view this post on Zulip Mario Carneiro (Apr 14 2021 at 09:03):

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

view this post on Zulip Mario Carneiro (Apr 14 2021 at 09:04):

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

view this post on Zulip Jakob von Raumer (Apr 14 2021 at 09:05):

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?

view this post on Zulip Mario Carneiro (Apr 14 2021 at 09:06):

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

view this post on Zulip Mario Carneiro (Apr 14 2021 at 09:07):

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

view this post on Zulip Mac (Apr 14 2021 at 23:43):

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.).

view this post on Zulip Mac (Apr 14 2021 at 23:53):

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.

view this post on Zulip Mario Carneiro (Apr 15 2021 at 01:24):

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

view this post on Zulip Sebastian Ullrich (Apr 15 2021 at 07:20):

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.


Last updated: May 07 2021 at 12:15 UTC