Zulip Chat Archive

Stream: general

Topic: Problems with notation overloading


view this post on Zulip Tomas Skrivan (Oct 01 2020 at 22:17):

I'm having problems with overloading a notation.

Everything works fine without overloading

notation x | y := pair[x][y]
variables {X Y Z : type} {x : X} {y : Y} {z : Z}
#check (x|y)
| pair[x][y] : Expr (X × Y)

However, adding an overload for the notation produces:

notation x | y := pair[x][y]
notation x | y := pair[x][y]
variables {X Y Z : type} {x : X} {y : Y} {z : Z}
#check (x|y)
| (λ (x_1 : Expr X), pair[x_1].app) x y : Expr (X × Y)

Why do I get (λ (x_1 : Expr X), pair[x_1].app) x y : Expr (X × Y) instead of pair[x][y] ?

This actually causes a failure of overload resolution for (x|y)|x with an error:

error for λ (x_1 : _), [choice Expr.app' Expr.app] ([choice Expr.app' Expr.app] (quotient.mk pair) x_1)
type mismatch at application
  (λ (x_1 : quotient ?m_1.setoid), Expr.app' pair[x_1]) ((λ (x_1 : Expr X), pair[x_1].app) x y)
term
  (λ (x_1 : Expr X), pair[x_1].app) x y
has type
  Expr (X × Y)
but is expected to have type
  quotient ?m_1.setoid

error for λ (x_1 : _), [choice Expr.app' Expr.app] ([choice Expr.app' Expr.app] pair x_1)
type mismatch at application
  (λ (x_1 : Expr (X × Y)), pair[x_1].app) ((λ (x_1 : Expr X), pair[x_1].app) x y) x
term
  x
has type
  X
but is expected to have type
  Expr ?m_1[(λ (x_1 : Expr X), pair[x_1].app) x y]

view this post on Zulip Reid Barton (Oct 01 2020 at 22:32):

I wouldn't recommend overloading notation, except possibly in cases where it's really obvious to Lean which variant is needed.

view this post on Zulip Tomas Skrivan (Oct 01 2020 at 22:41):

Not sure what is 'really obvious' but in my case those overloads either act on a type or on its quotient.

view this post on Zulip Reid Barton (Oct 01 2020 at 22:43):

Well, for example, since I don't know what pair[x] means, I couldn't tell which variant is expected in your #check example, except from context

view this post on Zulip Reid Barton (Oct 01 2020 at 22:46):

We don't really use overloaded notation, instead we use type classes. If you want to "overload function application" then you can create an instance of has_coe_to_fun.

view this post on Zulip Tomas Skrivan (Oct 01 2020 at 22:53):

I will have look at has_coe_to_fun.

Anyway, #check pair[x] gives pair[x] : Expr (?M_1 ⟶ X × ?M_1), it pairs with x.

view this post on Zulip Reid Barton (Oct 01 2020 at 22:55):

Is this [ ] notation also overloaded?

view this post on Zulip Tomas Skrivan (Oct 01 2020 at 22:57):

Yes it is. I'm working with a type representing expressions

inductive Expr : type  Type
| sym (T : type) (name : string) : Expr T
| app {X Y : type} : Expr (X  Y)  Expr X  Expr Y

notation f [ x ] := Expr.app f x

view this post on Zulip Tomas Skrivan (Oct 01 2020 at 22:59):

And it is also defined on the quotient

def Expr.app' {X Y : type} := quotient.lift₂ (λ f  x, f[x])
notation f [ x ] := Expr.app' f x

view this post on Zulip Reid Barton (Oct 01 2020 at 23:16):

Yeah, so in this situation I would not trust Lean to pick the correct overload variants.

view this post on Zulip Eric Wieser (Oct 01 2020 at 23:18):

So lean actually does support overloading without the usual approach of typeclasses? Is this documented anywhere?

view this post on Zulip Reid Barton (Oct 01 2020 at 23:32):

I'm pretty sure Lean makes some nonzero effort to select the right notation based on the available type information--it definitely does this for disambiguating the same name in several different open namespaces, which is a feature used mainly without being aware of it.

view this post on Zulip Eric Wieser (Oct 01 2020 at 23:37):

So functions can be overloaded by declaring them in different namespaces then opening both?

view this post on Zulip Reid Barton (Oct 01 2020 at 23:41):

Yes, or more commonly when a function in an opened namespace has the same name as one in the root namespace

view this post on Zulip Sebastian Ullrich (Oct 02 2020 at 08:32):

Overloaded names and notations are simply tried in turn, after which the unique successful interpretation is taken if any


Last updated: May 08 2021 at 19:11 UTC