Suggestion: how about `&` for overloaded method type separator, instead of `|`?

[vain0x]

Current syntax of overloaded method type looks like a union of function types. However, type of overloaded method behaves like an intersection of function types in typical type system.

I suggest to change the separator from | to & for consistency.

---

For example, there is a method f that is overloaded like this:

def f: (Integer) -> void
     | (String) -> void

If f has an intersection of function types, type check of f 42 passes like this:

f: ((Integer) -> void) & ((String) -> void)
-------------------------------------------
f: (Integer) -> void                         42: Integer
--------------------------------------------------------
f 42: void

f "hello" is also okay.

If union, it doesn't. It's unsure whether f can take an integer. This is an example written in lambda calculus with subtyping:

# g: (String) -> void
let g = \s: String. use_string s in

# Upcast to union type. This is OK since (T | U) is subtype of T.
let f: ((Integer) -> void | (String) -> void) = g in

f 42  # This shouldn't pass type check since `g 42` is type error.

[Ryan1729]

Here's an example of this in Typescript

type FType = ((a: number) => void) | ((a: string) => void)
const f: FType = (a: number | string) => {}

f(42)

type GType = ((a: number) => void) & ((a: string) => void)
const g: GType = (a: number | string) => {}

g(42)

The f(42) line causes a compile error, but the g(42) line does not.

[vain0x]

Closing this issue because it seems this issue was too late to change syntax.

[soutaro]

I'm sorry that I didn't notice this issue. Yes, I think it's too late and I won't change the syntax to & even though it would be more suitable to the semantics...

I don't remember why I made | the operator for overloading. Seems like there is no good reason for it.

[ParadoxV5]

Sorry for the necropost.
I came upon this suggestion while checking for #1875 and decided that this chunk of text fits here better.

---

The choice for | was probably because it was more natural for beginners, as in how Integer|String is narrowable while Integer&String is impossible to intersect (at runtime).

However, on deeper contemplation, & is more accurate, especially with a Lisp-1 (e.g., TypeScript) mindset (Ruby is Lisp-2):

• ^(Integer) -> void | ^(String) -> void means it might be one or the other, so only Integer & String args are safe to pass (if they exist).
• ^(Integer) -> void & ^(String) -> void means both Integer and String are fine for the intersection, therefore it’s practically ^(Integer | String) -> void

This is the same science as how in type args are contravariant.