Core C++

7.1. Overloading🔗

Definition7.1.1
Group: Overloading, polymorphism, subtyping and inference. (8)
Group member previews
Preview
Definition 7.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 5.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

A name denotes an overload set, the functions of the program with that name, or the methods of that name along the chain of a class, one per signature. A method of a derived class replaces the one of a base with the same signature, and a different signature is another overload, so the subset has no name hiding. Two declarations of one name live together only when they differ.

\dfrac{\text{arities differ, or } \exists i.\ p_i \neq q_i \text{ and neither } p_i \text{ nor } q_i \text{ is convertible}}{\text{the two declarations are overloads}}\;\textsf{(Distinguishable)}

A type is convertible when the library marks it so, as std::function of Definition 8.2.2. The restriction is the check 5 of the design. It keeps a lambda argument from deciding a call, which would ask for the type of the lambda before the candidate that gives it is known.

Lean code for Definition7.1.1●4 definitions
  • defdefined in CoreCpp/Syntax.lean
    complete
    def CoreCpp.sigOf (ps : List CoreCpp.Param) : List CoreCpp.Ty
    def CoreCpp.sigOf (ps : List CoreCpp.Param) :
  List CoreCpp.Ty
    The signature of a list of parameters, the types alone, which names one
member of an overload set.
  • defdefined in CoreCpp/Syntax.lean
    complete
    def CoreCpp.Program.funsNamed (p : CoreCpp.Program) (f : String) :
  List CoreCpp.Fun
    def CoreCpp.Program.funsNamed
  (p : CoreCpp.Program) (f : String) :
  List CoreCpp.Fun
    The overload set of the functions named f.
  • defdefined in CoreCpp/Syntax.lean
    complete
    def CoreCpp.Program.findMethods (p : CoreCpp.Program) (c m : String) :
  List (CoreCpp.Method × String)
    def CoreCpp.Program.findMethods
  (p : CoreCpp.Program) (c m : String) :
  List (CoreCpp.Method × String)
    The overload set of the method m as seen from class c, one method per
signature, the nearest in the chain of c, each with the class that declares
it. A method of a derived class replaces the one of a base with the same
signature, and a different signature is another overload, without the name
hiding of C++.
  • defdefined in CoreCpp/Typing.lean
    complete
    def CoreCpp.Typing.distinguishable (ps qs : List CoreCpp.Param) : Bool
    def CoreCpp.Typing.distinguishable
  (ps qs : List CoreCpp.Param) : Bool
    Two overloads of one name are declared together only when they differ in
arity or in a parameter of a type other than `std::function`, the check 5 of
the design. The restriction keeps a lambda argument from deciding a call,
which would ask for the type of the lambda before the candidate is known.

```
arities differ, or ∃ i. pᵢ ≠ qᵢ and neither pᵢ nor qᵢ is std::function
──────────────────────────────────────────────────────────────────── (Distinguishable)
the two declarations are overloads
```
Definition7.1.2
Group: Overloading, polymorphism, subtyping and inference. (8)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 5.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Definition 7.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A call collects the candidates of its arity that accept the arguments, each argument by value acceptable at the type of its parameter and each argument of a reference parameter denoting a location of that type. The choice is the exact candidate when several accept.

\dfrac{\begin{array}{c} A = \text{the candidates of } \mathrm{cand}(f, k) \text{ that accept } e_1, \ldots, e_k \\ A \text{ has one element whose parameters are} \\ \text{exactly the types of the arguments, or } A \text{ is a singleton} \end{array}}{\text{the call of } f \text{ selects that candidate}}\;\textsf{(T-Overload)}

With A empty the error is the one of the single candidate of that arity, when there is one, and no overload otherwise. With two or more in A and no exact one the call is ambiguous. Core C++ does not rank conversion sequences as C++ does, so the rule fits in one line on the board and the error is predictable.

The implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.

Lean code for Definition7.1.2●3 definitions
  • opaquedefined in CoreCpp/Typing.lean
    complete
    opaque CoreCpp.Typing.pickOverload (p : CoreCpp.Program) (Γ : CoreCpp.TEnv)
  (who : String) (cands : List (List CoreCpp.Param))
  (es : List CoreCpp.Expr) : CoreCpp.T Nat
    opaque CoreCpp.Typing.pickOverload
  (p : CoreCpp.Program) (Γ : CoreCpp.TEnv)
  (who : String)
  (cands : List (List CoreCpp.Param))
  (es : List CoreCpp.Expr) : CoreCpp.T Nat
    The candidate of an overload set that a call selects, by its index. The
candidates that accept the arguments are collected, and the choice is the
exact one when several accept.

```
A = the candidates of cand(f, k) that accept e₁, …, eₖ
A has one element whose parameters are exactly the types of the arguments, or A is a singleton
─────────────────────────────────────────────────────────────────────────────── (T-Overload)
the call of f selects that candidate
```

With A empty the error is the one of the single candidate of that arity,
when there is one, and `no overload` otherwise. With two or more in A and
no exact one the call is ambiguous. Core C++ does not rank conversion
sequences, so the rule fits in one line on the board.
  • opaquedefined in CoreCpp/Typing.lean
    complete
    opaque CoreCpp.Typing.resolveFun (p : CoreCpp.Program) (Γ : CoreCpp.TEnv)
  (f : String) (es : List CoreCpp.Expr) : CoreCpp.T CoreCpp.Fun
    opaque CoreCpp.Typing.resolveFun
  (p : CoreCpp.Program) (Γ : CoreCpp.TEnv)
  (f : String) (es : List CoreCpp.Expr) :
  CoreCpp.T CoreCpp.Fun
    The function a call selects out of the overload set of its name.
  • opaquedefined in CoreCpp/Typing.lean
    complete
    opaque CoreCpp.Typing.resolveMethod (p : CoreCpp.Program) (Γ : CoreCpp.TEnv)
  (recv : CoreCpp.Expr) (arrow : Bool) (m : String)
  (es : List CoreCpp.Expr) : CoreCpp.T (CoreCpp.Method × String)
    opaque CoreCpp.Typing.resolveMethod
  (p : CoreCpp.Program) (Γ : CoreCpp.TEnv)
  (recv : CoreCpp.Expr) (arrow : Bool)
  (m : String) (es : List CoreCpp.Expr) :
  CoreCpp.T (CoreCpp.Method × String)
    The method a call selects, with the class that declares it, the rules
T-Method and T-MethodArrow with the overload set of the name.
Definition7.1.3
Group: Overloading, polymorphism, subtyping and inference. (8)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 2.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Overloading adds no evaluation rule. The type checker writes the signature of the chosen candidate into the tree, the field sig of a call, and the evaluator looks a function or a method up by name and signature instead of by name alone. A program that was not annotated, which the checker rejects first, runs with the first candidate of the name.

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.

Lean code for Definition7.1.3●3 definitions
  • defdefined in CoreCpp/Semantics.lean
    complete
    def CoreCpp.FunEnv.lookupSig (fs : CoreCpp.FunEnv) (f : String)
  (sig : Option (List CoreCpp.Ty)) : Option CoreCpp.Fun
    def CoreCpp.FunEnv.lookupSig
  (fs : CoreCpp.FunEnv) (f : String)
  (sig : Option (List CoreCpp.Ty)) :
  Option CoreCpp.Fun
    The function named f with the signature the type checker chose, or the
first one of the name when the program was not annotated.
  • defdefined in CoreCpp/Eval.lean
    complete
    def CoreCpp.Eval.resolve (fs : CoreCpp.FunEnv) (s t m : String)
  (sig : Option (List CoreCpp.Ty)) : CoreCpp.M (CoreCpp.Method × String)
    def CoreCpp.Eval.resolve (fs : CoreCpp.FunEnv)
  (s t m : String)
  (sig : Option (List CoreCpp.Ty)) :
  CoreCpp.M (CoreCpp.Method × String)
    The method m of class s with the signature the type checker chose, the
nearest in the chain of s, dispatched by the tag t when that method is
virtual. The signature picks one member of an overload set, and without it,
in an unannotated program, the first of the name serves.
  • defdefined in CoreCpp/Typing.lean
    complete
    def CoreCpp.Typing.annotate (p₀ : CoreCpp.Program) :
  CoreCpp.T CoreCpp.Program
    def CoreCpp.Typing.annotate
  (p₀ : CoreCpp.Program) :
  CoreCpp.T CoreCpp.Program
    The program with the static classes, the chosen overloads and the
reference returns filled in. Fails only on an ill typed program, which
`check` rejects first.