## Stream: general

#### Tomas Skrivan (Oct 01 2020 at 22:17):

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)


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]


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

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

#### 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

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

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

#### Reid Barton (Oct 01 2020 at 22:55):

Is this [ ] notation also overloaded?

#### 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


#### 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


#### Reid Barton (Oct 01 2020 at 23:16):

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

#### Eric Wieser (Oct 01 2020 at 23:18):

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

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

#### Eric Wieser (Oct 01 2020 at 23:37):

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

#### 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

#### 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