Skip to content

Instantly share code, notes, and snippets.

@HertzDevil
Created April 6, 2021 05:18
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save HertzDevil/b2150e2c1051fc29f191e5ac69644641 to your computer and use it in GitHub Desktop.
Save HertzDevil/b2150e2c1051fc29f191e5ac69644641 to your computer and use it in GitHub Desktop.
Overload order

Overload order

Definitions

A call is said to be in canonical position if positional parameters are matched with positional arguments, and named parameters are matched with named arguments. This means the names of positional parameters do not matter for overload ordering, but they must not be used by named arguments.

def foo(a, b = 0, *c, d, e = 0, **f); end

# These calls are in canonical position:
foo(1, d: 1)
foo(1, 2, d: 3, e: 4)
foo(1, 2, 3, 4, d: 5, e: 6, f: 7, g: 8)

# These calls are *not* in canonical position:
foo(a: 1, d: 2)
foo(1, d: 2, b: 3)

Given defs f and g, a parameter x of f and a parameter y of g are said to be a pair of corresponding parameters if there exists a call in canonical position such that a single argument of the call matches both x and y.

def foo(x0, x1, x2, *xs, n0, n1, n2); end
def bar(y0, y1, *ys, n2, n3, **ns); end

# The corresponding parameter pairs are:
# * `x0` <-> `y0`
# * `x1` <-> `y1`
# * `x2` <-> `ys`
# * `xs` <-> `ys`
# * `n0` <-> `ns`
# * `n1` <-> `ns`
# * `n2` <-> `n2`
# Note that `ys` and `ns` each have multiple corresponding parameters,
# whereas `n3` has none

Two defs are compatible if there exists a common call in canonical position where all arguments are matched to the respective parameters in each def.

A parameter x subsumes y if every valid argument for x is also a valid argument for y. As a special case, a parameter without a restriction never subsumes a parameter with a restriction applied. (This subsumption is defined parameter-wise at the moment, so cannot account for e.g. identical free variables in multiple parameters.)

A parameter x is more specific than y if, whenever x is matched by n arguments, y can also be matched by n arguments, but not vice-versa. Since

  • a required parameter is matched by 1 argument;
  • an optional parameter is matched by 0 or 1 argument;
  • a splat parameter is matched by 0 or more arguments; (TODO: this is not always true when a restriction is provided, especially for splat restrictions)

required parameters are more specific than optional parameters, which are more specific than splat parameters.

Computing strictness

To determine whether a def f should be ordered before g for overload resolution, we first check whether the two defs are compatible at all. Two defs can be incompatible if any of the following is true:

  • f has more required positional parameters than there are positional parameters (required or optional) in g, and g does not have a single splat parameter;
  • f has a required named parameter m, and g has neither that named parameter nor a double splat parameter;
  • f accepts a block and g does not.

Each of the following pairs of overloads are incompatible with each other:

# second overload requires 2 arguments, first accepts only 1
def foo(x0); end
def foo(y0, y1); end

# second overload requires 2+ arguments, first accepts only 0 or 1
def foo(x0 = 0); end
def foo(y0, y1, *ys); end

# second overload requires argument for `n0`, first doesn't accept it
def foo; end
def foo(*, n0); end

# second overload yields, first doesn't
def foo; end
def foo; yield; end

If neither def is stricter than the other, then their overload order is based on their definition order. If two defs are incompatible, an ordering might de defined between them nonetheless to make the strictness relation transitive. This applies only to the first rule above.

The next step is to compare all the corresponding parameter pairs between them by subsumption. If all parameters in f subsume their corresponding parameters in g (where they exist), but not vice-versa, then f is stricter than g. If both defs have parameters that are not subsumed by their corresponding parameters in the opposite def, then neither def is stricter. If all pairs of corresponding parameters subsume each other, we then check the specificity of all the parameters instead.

In the following examples, the first overload of each group is stricter than the second overload:

# Int32 < Int
def foo(x0 : Int32); end
def foo(y0 : Int); end

# having a restriction is always stricter than not having one
def foo(x0 : _); end
def foo(y0); end

# `xs` and `y0` are corresponding parameters, and `Int32 < Int`
def foo(*xs : Int32); end
def foo(y0 : Int); end

# `m0` and `ns` are corresponding parameters, and `Int32 < Int`
def foo(*, m0 : Int32); end
def foo(**ns : Int); end

In each group of the overloads below, neither def is stricter than the other:

# Int32 < String and String < Int32 are both false
def foo(x0 : Int32); end
def foo(y0 : String); end

# `y0` doesn't subsume `x0`, and `x1` doesn't subsume `y1`
def foo(x0 : Int32, x1 : Number); end
def foo(y0 : Int, y1 : Int); end

# `ys` doesn't subsume `x0`, and `x1` doesn't subsume `ys`
def foo(x0 : Int32, x1 : Number); end
def foo(*ys : Int); end

# `ys` doesn't subsume `x0`, and `ms` doesn't subsume `n0`
def foo(x0 : Int32, **ms : Number); end
def foo(*ys : Int, n0 : Int); end

Specificity checking is done by identifying method signatures that would result in certain parameters being less specific than their corresponding parameters in the other def. For positional parameters, this happens when:

  • f has fewer required parameters than g. Consider

    def f(x0, x1, ..., xm); end
    def g(y0, y1, ..., ym, ..., yn); end

    If there are no corresponding parameters in f for ..., yn, then the two defs are incompatible. Otherwise, the parameters that follow xm must be optional or splat parameters, and they are less specific than required parameters.

  • Neither def has a single splat parameter, and f can accept more parameters than g does. These extra parameters in f must all be optional.

    def f(x0, x1, x2 = 0, x3 = 0); end
    def g(y0, y1); end
  • f has a single splat parameter xs and g does not. Then g's parameters that correspond to xs must be required or optional.

    def f(x0, *xs); end
    def g(y0, y1, y2 = 0); end
  • Both defs have a single splat parameter, and f's splat parameter appears before g's splat parameter, so that the former corresponds to required or optional parameters in g.

    def f(*xs); end
    def g(y0, y1 = 0, *ys); end

The first rule has a higher priority, and wins over the remaining three rules. This helps resolve cases like the following:

def foo(x0, x1 = 0, x2 = 0, x3 = 0); end
def foo(y0, y1, y2 = 0); end

The second overload is more specific than the first one, despite the first accepting more arguments than the second, since for any compatible calls between the two overloads (i.e. 2 or 3 positional arguments), y1 is more specific than x1 = 0, and the parameters that appear after x2 do not matter.

The following defs:

def f(x0 = 0); end
def g(y0, y1, y2 = 0); end

are incompatible because f accepts at most 1 positional parameter and g requires at least 2. However, we state through the first rule that f is nonetheless less specific than g. Suppose a third def def h(z0, z1 = 0); end is added; then g is more specific than h, and h is more specific than f. Therefore, g must be more specific than f even though there are no common calls. Such a chain of intermediate defs always exist, unless neither f nor g uses optional positional parameters or single splats, but without loss of generality, even given:

def f(x0); end
def g(y0, y1); end

we assume g is more specific than f. The result is that a total order exists between all possible signatures of positional parameters, as follows:

...
def foo(x0, x1); end
def foo(x0, x1, x2 = 0); end
def foo(x0, x1, x2 = 0, x3 = 0); end
...
def foo(x0, x1, x2 = 0, x3 = 0, *xs); end
def foo(x0, x1, x2 = 0, *xs); end
def foo(x0, x1, *xs); end
def foo(x0); end
def foo(x0, x1 = 0); end
def foo(x0, x1 = 0, x2 = 0); end
...
def foo(x0, x1 = 0, x2 = 0, *xs); end
def foo(x0, x1 = 0, *xs); end
def foo(x0, *xs); end
def foo; end
def foo(x0 = 0); end
def foo(x0 = 0, x1 = 0); end
...
def foo(x0 = 0, x1 = 0, *xs); end
def foo(x0 = 0, *xs); end
def foo(*xs); end # least specific overload

For a given named parameter n, f has a less specific signature than g when:

  • n is a required parameter in g, but not a required parameter in f. This means either n's corresponding parameter in f is an optional or splat parameter, or the two defs are incompatible.

    def f; end
    def g(*, n); end
  • Neither def has a double splat parameter, and n is optional in f but not accepted in g.

    def f(*, n = 0); end
    def g; end
  • f has a double splat parameter and g does not. (This also applies when there are no named parameters at all other than the double splat.)

    def f(**ns); end
    def g(*, n); end
  • Both defs have a double splat parameter, and n is optional in g but not present in f.

    def f(**ns); end
    def g(*, n = 0, **ns); end

As with the positional case, the first rule wins over the rest of the rules. However, def f; end and def g(*, n); end are unordered, as no possible transitivity issues could occur here.

The combined specificity is derived from the signature for the positional parameters, plus the signature for each named parameter. If both defs have signatures that are less specific than the opposite def, then neither def is stricter; otherwise, the def with more specific signatures comes first. At this point, if none of the signatures are less specific, then the two defs must be equivalent, so the last def will be considered a redefinition of the first one.

The following are some cases where neither def is stricter than the other:

# `x` is more specific than `y = 0`, but
# `n` is more specific than `n = 0`
def foo(x, *, n = 0); end
def foo(y = 0, *, n); end

# no positional parameters is more specific than `*ys`, but
# no named parameters is more specific than `**ms`
def foo(**ms); end
def foo(*ys); end

# `x` is more specific than `*ys`, but
# `n` is more specific than `**ms`
def foo(x, **ms); end
def foo(*ys, n); end

# `m` is more specific than `m = 0`, but
# `n` is more specific than `n = 0`
def foo(*, m, n = 0); end
def foo(*, n, m = 0); end

Generic types

A single overload order exists across all instantiations of the same generic type. Any bound type variables appear as if they are unbound free variables during strictness evaluation, and by default they never subsume non-free restrictions. (This is the current behaviour already.)

class A; end
class B < A; end
class C < B; end

class Foo(T)
  # behaves as if `forall T` is present during strictness evaluation
  def foo(x : T)
    1
  end

  # always stricter than the overload above, even when T < B
  def foo(x : B)
    2
  end
end

Foo(A).new.foo(A.new) # => 1
Foo(A).new.foo(A.new) # => 2
Foo(A).new.foo(A.new) # => 2

Foo(B).new.foo(B.new) # => 2
Foo(B).new.foo(B.new) # => 2

Foo(C).new.foo(C.new) # => 2
Foo(C).new.foo(C.new) # => 2

If free variable unification is implemented, it should be done during the subsumption checks between the corresponding parameter pairs.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment