Core C++

7.4. Subtyping and inference🔗

Theorem7.4.1
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 6.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N

Subsumption is the typing rule of subtyping, and it is the only conversion between class types.

\dfrac{\Gamma \vdash e : D* \qquad D \text{ derives from } B}{\Gamma \vdash e : B*}\;\textsf{(T-Sub)}

It holds in declarations, assignments, arguments, results, comparisons and in the branches of ?:.

Subtype polymorphism and parametric polymorphism do not compose in the subset. Two instantiations of one template have no subtype relation, so Stack<D*> is not a subtype of Stack<B*>, and the reason is that a Stack<B*> accepts an push of any B*, which a Stack<D*> does not. Variance is left out of the subset.

Definition7.4.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.
uses 1used by 0✓L∃∀N

Type inference in Core C++ is local. The rule of auto is the one of the earlier units, and it already reaches pointers and instantiations, because a pointer has values and an instantiation is a class.

\dfrac{\Gamma \vdash e : \tau \qquad \tau \text{ has values} \qquad \tau \neq \mathtt{nullptr\_t}}{\Gamma \vdash \mathtt{auto}\ x = e \dashv \Gamma[x \mapsto \tau]}\;\textsf{(T-Auto)}

A lambda has no type of its own, so it never initialises an auto, which the grammar already guarantees. Inference over a whole program, as Hindley and Milner give it for Haskell, has no rule here, and it is shown as a contrast.

Lean code for Definition7.4.2●1 definition
  • inductive(11 constructors)defined in CoreCpp/Syntax.lean
    complete
    inductive CoreCpp.Cmd : Type
    inductive CoreCpp.Cmd : Type
    Commands. A block is a list of commands. `exprStmt` is the statement that
evaluates an expression and discards its value. `declRef` is the local
reference `τ& x = e`, a second name for the location `e` denotes. `delete e
static` is `delete e;`, with `static` the class of the pointer as the type
checker sees it, filled by `Typing.annotate`.

    Constructors

    CoreCpp.Cmd.block (cs : List CoreCpp.Cmd) : CoreCpp.Cmd
    CoreCpp.Cmd.ite (c : CoreCpp.Expr)
  (t e : List CoreCpp.Cmd) : CoreCpp.Cmd
    CoreCpp.Cmd.while (c : CoreCpp.Expr)
  (body : List CoreCpp.Cmd) : CoreCpp.Cmd
    CoreCpp.Cmd.for (init : CoreCpp.Cmd) (c : CoreCpp.Expr)
  (step : CoreCpp.Cmd) (body : List CoreCpp.Cmd) :
  CoreCpp.Cmd
    CoreCpp.Cmd.ret (e : Option CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.decl (ty : CoreCpp.Ty) (x : String)
  (init : CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.declRef (ty : CoreCpp.Ty) (x : String)
  (init : CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.declAuto (x : String) (init : CoreCpp.Expr) :
  CoreCpp.Cmd
    CoreCpp.Cmd.assign (lhs rhs : CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.exprStmt (e : CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.delete (e : CoreCpp.Expr)
  (static : Option String) : CoreCpp.Cmd