Catch errors that are not caught by parsing (because many constructs are not context-free).

<p>Examples (C):
<ol>
	<li>All identifiers are declared
	<li>Types
	<li>...
</ol>
The set of legal programs is a subset of the parse-able programs.

<h3>Scope</h3>
<ul>
	<li>Match identifier declarations with uses
	<ul>
		<li>Important static analysis step
	</ul>
	Example 1:
	<pre>
	void foo (int n) {
	  int a = 0, i;
    printf("a = %d\n", a);
		for (i = 0; i &lt; n; i++) {
      int a = 1;
      printf("a + j = %d\n", a + j); //a's value is 1. where is j. error?
		}
    printf("a = %d\n", a);
  }
	</pre>
	<li>The <em>scope</em> of an identifier is the porition of the program in which that identifier is accessible
	<li> The same identifier may refer to different things in different parts of the program
	<ul>
		<li>Different scopes for same name don't overlap
	</ul>
	<li>An identifier may have restricted scope
	<li> Most languages have <em>static</em> scope
	<ul>
		<li> Scope depends only on the program text, not run-time behaviour. e.g., C
	</ul>
	<li>A few languages are <em>dynamically</em> scoped
	<ul>
		<li>Lisp (earlier versions, now moved to static scoping), SNOBOL
		<li>Scope depends on execution behaviour of a program
	</ul>
	<li> A dynamically-scoped variable refers to the closest enclosing binding in the execution of the program
	<ul>
		<li>Example:
		<pre>
void foo(int x)
{
  int a = 4;
  bar(3);
}
void bar(int y)
{
  printf("a = %d\n", a); //refers to a in the closest enclosing binding in the execution of the program
}
		</pre>
	</ul>
	<li>We will talk about dynamic scope later ...
	<li>In C, identifier bindings are introduced by:
	<ul>
		<li> Function definitions (introduces method names; only allowed at top-level)
		<li> Struct definitions (introduces type names aka class names)
		<li> Variable declarations (introduces objects of certain types; objects represent regions of memory)
		<li> Structure field definitions (introduces objects)
		<li> Function argument declarations (introduces objects of certain types)
		<li> Typedefs (introduces type names)
	</ul>
	<li>Not all identifiers follow the most-closely nested rule
	<ul>
		<li>Function definitions in C cannot be nested
		<li>Forward declarations are allowed for functions and variables (extern keyword). Thus a variable can be used before it is defined.
		<li>In C++, you can use member functions for the type-variables even if they have never been declared/defined (type-variables are the arguments to the template keyword)
		<li>In C++ class declaration, you can use a member variable in a method before it is defined.
		<li>Some languages allow identifiers to be overridden within the same scope, others don't. Some languages allow identifiers to be overridden in different nested scopes, others may not. 
	</ul>
</ul>

<h3>Symbol Tables</h3>
<ul>
	<li>Much of semantic analysis can be expressed as a recursive descent of an AST
	<ul>
		<li> <em>Before</em>: Process an AST node <code>n</code>
		<li> <em>Recurse</em>: Process the children of <code>n</code>
		<li> <em>After</em>: Finish processing the AST node <code>n</code>
	</ul>
	<li>When performing semantic analysis on a portion of the AST, we need
	to know which identifiers are defined
	<li>A <em>symbol table</em> is a data structure that tracks the current bindings of the identifiers
	<li>Example: the scope of a variable declaration is one subtree of the AST
	<pre>
   { //new scope
     int x = 4;  //declarations
     f(x);
   }
   Tree:
   NewScope --&gt;(left child) declarations x = 4
   NewScope --&gt;(right child) statements
	</pre>
	On entry to the new scope, the new declarations will be added to the symbol table before recursing down right child (statements). On returning from the new scope, the new declarations will be removed and the old declarations of x (if any) will be restored in the symbol table.
	<li> For implementing a symbol table, we can use a stack of scopes (assuming C89)
	<ul>
		<li> <code>enter_scope()</code>: start a new nested scope
		<li> <code>find_symbol(x)</code>: search stack starting from top, for the first scope that contains <code>x</code>. Return first <code>x</code> found or NULL if none found
		<li> <code>add_symbol(x)</code>: add a symbol to the current scope (top scope)
		<li> <code>check_scope(x)</code>: true if <code>x</code> defined in the current scope (top scope). allows to check for double definitions.
		<li> <code>exit_scope()</code>: exit current scope
	</ul>
	<li>For implementing forward declarations, or C++ style use-before-define styles, one may have to make multiple passes over the AST. First pass: gather all member names. Second pass: Do the checking. In general, semantic analysis requires multiple passes (often more than two). Easier to break the analysis into simpler passes, as opposed to one big complicated pass.
</ul>

<h3>Types</h3>
<ul>
	<li>What is a type
	<ul>
		<li>The notion varies from language to language
		<li>Typically
		<ul>
			<li>A set of values
			<li>A set of operations on those values
		</ul>
		<li>Classes are one instantiation of the modern notion of type
	</ul>
	<li>Consider the assembly language fragment:
	<pre>
  add $r1,$r2,$r3
	</pre>
	What are the types of $r1, $r2, $r3? Can't say. For all you know, r1 may represent a bit-pattern that represents a string. The only thing we can say is that these have the base-type <em>bitvector</em>.
	<li>Types restrict the set of legal programs further
	<ul>
		<li>e.g., addition on a string seems quite unlikely
		<li>Tradeoff: catch common mistakes (e.g., addition to string is quite unlikely), but may eliminate some more-optimized programs (we can still specify all programming functionality, just that the remaining set of programs may not be as optimized as the original set of programs).
		<li>Different programming languages take different tradeoff points, e.g., OCaml has immutable variables (i.e., values are written only at time of creation) while C has mutable variables (values can be written at any time).
		<li>Well-typed programs (or well-defined programs) are a subset of parseable programs that have all symbol uses matched with its corresponding definition.
		<ul>
			<li>A type checking logic can execute either at compile time or at runtime to disambiguate well-typed programs from not-well-typed programs
			<li><em>or</em> this checking responsibility can be left to the programmer (undefined behaviour)
		</ul>
	</ul>
	<li>Certain operations are legal for values of each type
	<ul>
		<li>It doesn't make sense to add a function pointer and an integer in C.
		<li>It does make sense to add two integers
		<li>But both have the same assembly language implementation!
	</ul>
	<li>A language's type system specifies which operations are valid for which types
	<li>The goal of type checking is to ensure that operations are used with correct types
	<ul>
		<li>Enforces intended interpretation of values, because nothing else will!
	</ul>
	<li>Three kind of languages
	<ul>
		<li>Statically typed: All or almost all checking of types is done as part of compilation (C, Java)
		<li>Dynamically typed: Almost all checking of types is done as part of program execution (Scheme, Lisp, Python, Perl)
		<li>Type unchecked: No type checking. All strings in the language (e.g., CFG) are valid strings. e.g., machine code, or some parts of C, e.g., integer overflow.
	</ul>
	<li>Another variation of typing: undefined behaviour. Accessing word beyond the length of an array is not type-checked in C. But if this happens at runtime, the program is not well-defined (or well-typed). The type-system is in programmer's head, but nobody will check it for you!
	<li>Competing views on static vs. dynamic typing
	<ul>
		<li>Long-standing debate which is better
	</ul>
	<li>Static typing proponents say:
	<ul>
		<li>Static checking catches many programming errors at compile time
		<li>Avoids overhead of runtime checks
	</ul>
	<li>Dynamic typing proponents say:
	<ul>
		<li>Static type systems are restrictive. Restricts the programs that you can write (even though they may be well-typed at runtime)
		<ul>
			<li>Array de-reference quite hard to verify statically. Restricting programs to only those programs that can be verified statically is a non-starter. Java decides to use runtime checks (dynamic type-checking).
		</ul>
		<li>Rapid prototyping difficult within a static type system
	</ul>
	<li>Some strange things about typing
	<ul>
		<li>A lot of code is written in statically typed languages with an "escape" mechanism
		<ul>
			<li>Unsafe casts in C, Java
			<li>Philosophy: if the programmer knows what she is doing, let her do whatever she wants. e.g., addition on strings. If the programmer is making a mistake, the program will behave badly, but the language does not provide any guarantees (after all you took the matter in your hands)
		</ul>
		<li>People retrofit static typing to dynamically typed languages
		<ul>
			<li>Avoid runtime costs
			<li>Debugging
			<li>This can only be best-effort, no guarantees. Some dynamic checks may remain
		</ul>
	</ul>
	<li>In C
	<ul>
		<li>The user declares types for identifiers
		<li>The compiler infers types for expressions
	</ul>
	<li><em>Type checking</em> is the process of verifying fully typed programs. Types are already available. We just check if the type rules are obeyed.
	<li><em>Type inference</em> is the process of filling in missing type information.
  <li> Both type-checking and type-inference rely on the same set of <em>typing rules</em>.  Type-checking and type-interference are different terms, but people often use them interchangeably for this reason.
</ul>

<h3>Type checking formalism</h3>
<ul>
	<li>Inference rules have the form
	<ul>
		<li>If Hypothesis is true, then Conclusion is true
	</ul>
  <li>The hypothesis and conclusion can be written in arbitrary logic, e.g., propositional logic where the atomic propositions are formed using relational operators over values drawn
from a set.  Another example is first-order logic.
	<li>Rules of inference are a compact notation for "If-Then" statements
	<li>The notation is easy to read with practice
	<li>We will start with a simplified system and gradually add features
	<li>Type checking computes via reasoning
	<ul>
		<li>If E1 and E2 have certain types, then E3 has a certain type
	</ul>
	<li>Building blocks
	<ul>
		<li>Symbol ^ is "and"
		<li>Symbol =&gt; is "if-then"
		<li>x:T is "x has type T"
	</ul>
	<li>If <code>e1</code> has type <code>Int</code> and <code>e2</code> has type <code>Int</code>, then <code>e1+e2</code> has type Int
	<li><code>(e1:Int ^ e2:Int) =&gt; e1+e2:Int</code>
	<li><code>(e1:Int ^ e2:Int) =&gt; e1+e2:Int</code> is a special case of <code>Hypothesis1 ^ Hypothesis2 ... ^ HypothesisN =&gt; Conclusion</code></li>
		<ul>
			This is an inference rule
		</ul>
	<li>By tradition inference rules are written
	<pre>
|- Hypothesis ... |- Hypothesis
-------------------------------
     |- Conclusion
	</pre>
	<li>e.g., C types have hypotheses and conclusions of the form
	<pre>
|- e:T
	</pre>
	<li> <code>|-</code> means "it is provable that ..."
</ul>

<h4>Some rules</h4>
<pre>
i is an integer literal (constant)
----------------------------------  [Int]
     |- i:int
</pre>
<pre>
|-e1:int    |-e2:int
----------------------------------  [Add]
     |-e1+e2:int
</pre>

<ul>
<li>These rules give templates describing how to type integers and + expressions
<li>By filling in the templates, we can produce complete typings for expressions
<pre>
1 is an int literal
-------------------
  |- 1:int

2 is an int literal
-------------------
  |- 2:int

|-1:int   |-2:int
-----------------
   |-1+2:int
</pre>
</ul>

<h4>Type Checking</h4>
<ul>
	<li>Type checking proves facts <code>e:T</code>
	<ul>
		<li>Proof is on the structure of the AST
		<li>Proof has the shape of the AST
		<li>One type rule is used for each AST node
	</ul>
	<li>In the type rule used for a node <code>e</code>:
	<ul>
		<li>Hypotheses are the proofs of types of <code>e</code>'s subexpressions
		<li>Conclusion is a type of <code>e</code>
	</ul>
	<li>Types are computed in a bottom-up pass over the AST
</ul>

<h4>Subtyping relation between types</h4>
  <ul>
    <li><code>S &lt;: T</code> is read "S is a subtype of T" or "T is a supertype of S".
    <li><code>S</code> is a subtype of <code>T</code> if any term of type <code>S</code> can be safely used in a context where a term of type <code>T</code> was expected.
    <li>The precise semantics of subtyping here crucially depends on the particulars of how "safely be used" and "any context" are defined by a given type formalism or programming language. The type system of a programming language essentially defines its own subtyping relation.</li>
    <li>Consider two types <code>int</code> and <code>bool</code>.  Let's hypothetically say that every operator that is defined for a term of type <code>bool</code> is also defined for a term of type <code>int</code>, e.g., <code>1 &amp;&amp; 3</code> evaluates to say <code>4</code> (for some strange definition of the semantics of <code>&amp;&amp;</code> on integers. But that does not necessarily mean that <code>int</code> is a subtype of <code>bool</code>.
    </li>
    <li>Due to the subtyping relation, a term may belong to more than one type. Subtyping is therefore a form of type polymorphism.</li>
    <li>Subtype is the same as "derived" type in an OO language
    <li>Supertype is the same as "base" type in an OO language
    <li>Example: the following code is type-correct
    <pre>
class A { ... };
class B : A { ... };
A a = B();
    </pre>
    </li>
    <li>Subtyping relation is reflexive, transitive, and anti-symmetric:
    <ul>
      <li> Reflexive: <code>S &lt;: S</code>
      <li> Transitive: <code>S &lt;: T</code> and <code>T &lt;: U</code> implies <code>S &lt;: U</code>.
      <li> Antisymmetric: <code>S &lt;: T</code> and <code>T &lt;: S</code> implies <code>S=T</code>.
    </ul>
    </li>
    <li>In C/C++:
    <ul>
      <li> <code>char</code> is <em>not</em> a subtype of <code>int</code>.  Similarly, <code>int</code> is <em>not</em> a subtype of <code>float</code>.
      <ul>
        <li>Consider a function declaration of type <code>void foo(int i) { ... }</code>.  Strictly speaking, it is not legal to call <code>foo('c')</code> (where <code>'c'</code> is of <code>char</code> type. Similar is the case for <code>float</code> and <code>int</code>.</li>
        <li>It is a different matter that compilers implement <em>implicit type conversion</em>, also called <em>implicity type casting</em> where they implicitly cast <code>char c</code> to <code>int</code>.  This casting could also have been done explicitly by the programmer, to make the program legal.  Recall that <em>type casting</em> is a backdoor provided in C to allow type conversions for programmer convenience.
        <li>Why did the C designers choose not to make <code>char</code> a subtype of <code>int</code>?  Perhaps, because they wanted to allow the programmer to have (among other things) two versions of a function <code>foo</code>, one that accepts a value of type <code>char</code> as an argument, and another that accepts a value of type <code>int</code> as an argument, also called <em>function overloading</em>.
        <li>Why not allow function overloading but still keep <code>char</code> as a subtype of <code>int</code>, and choose the most precisely fitting function definition for <code>foo</code> in case there are multiple choices?  That is an interesting proposal, but then we also need to tackle the case where <code>foo</code> takes multiple arguments, and one definition is <code>foo(int, char)</code> and another is <code>foo(char, int)</code>.  It is quite unclear what to do in this case.
        <li>Implicit type casting is an optional feature in a compiler.
        <li>The rules for <em>implicit type casting</em> in a compiler can also be expressed using inference rules.  However, in practice, so far, both type checking and implicit type casting is done directly in imperative code, instead of through a DSL to express these inference rules.  Yet, it is much easier to learn about these rules as succinct and neat inference rules.</li>
        <li>There is a push towards specifying the language standards (e.g., C standard) through formal inference rules, they are currently specified using english text.</li>
      </ul>
    </ul>
    </li>
  </ul>

<h4>Soundness of a static typesystem</h4>
  <ul>
   <li>Let the <em>execution semantics</em> define that an <em>expression is evaluated to a value v</em>.  Further, let value <code>v</code> be of type <code>T</code>.</li>
   <li>Let the <em>static typing rules</em> define that an <em>expression is of type T</em>, i.e., <code>e:T</code>.</li>
   <li>A static typesystem is <em>sound</em>  with respect to an execution semantics if whenever <code>e:T</code>, then <code>e</code> evaluates to a value of subtype <code>S&lt;:T</code>.</li>
   <li>The soundness of a static typesystem can be ascertained by checking the soundness of eeach type rule.
   <li>We want only sound type rules, but some sound type rules are <em>better</em> (i.e., more precise) than others:
   <ul>
     <li>The following type rule is sound
     <pre>
|- 1 : int   |- 2 : int
-----------------------
    |- 1+2 : void
     </pre>
     </li>
     <li>The following type rule is also sound
     <pre>
|- 1 : int   |- 2 : int
-----------------------
    |- 1+2 : int
     </pre>
     </li>
    </ul>
    Even though both type rules are sound, the second type rule is <em>more precise</em> than the first one.
    In other words, the second type rule admits more desirable programs as type-correct than the first rule.
    For example (1+2)+3 will be type-incorrect with the first rule, but will be type-correct with the second rule.
    </li>
    <li> [Optional discussion] What does <em>completeness</em> mean here?  A static typesystem would be <em>complete</em>
    with respect to an execution semantics if whenever <code>e</code> evaluates to a value of type <code>T</code>,
    then <code>e:T</code> is provable. However, achieving completeness is not possible in the presence of loops. For example, completeness requires that all programs that can produce a value <code>v:T</code> should also statically evaluate to type <code>T</code>; however, in the presence of loops, a value may be computed only if the loop terminates. If the loop never terminates, the type-checker should assign a type that agrees with non-termination (e.g., <code>void</code> to indicate that this value can never be used, or a stronger type that indicates non-termination explicitly). This  would amount to statically identifying if the loop terminates, but that is the halting problem. There is more discussion on completeness later.</li>
  </ul>

<h4>Our programming language</h4>
Our programming language is a subset of C/C++ with the following exceptions/features:
  <ul>
    <li> Declarations appar only at the beginning of a scope.</li>
    <li> Even statements represent values and are thus associated with a type.  For this reason, we will just call a statement, an expression.</li>
    <li> Object-oriented features are supported with subtyping, i.e., the programmer can define custom types and subtypes.</li>
    <li> Primitive types include <code>bool</code> and <code>int</code>. <em>Important</em>: <code>void</code> is the supertype of all types.</li>
  </ul>

<h2>Type rules for our programming language</h2>
<pre>
------------------  [false]
  |- false : bool
</pre>
<pre>
------------------  [true]
  |- true : bool
</pre>

<pre>
 s is a character literal
------------------------- [char]
  |- s : char
</pre>
<pre>
 s is a string literal
----------------------- [string]
  |- s : char *
</pre>
<pre>
    |-b:bool
----------------------- [Not]
  |- !b : bool
</pre>
<pre>
  |-x:int  |-y:int
----------------------- [Relational]
  |- x&lt;y : bool
</pre>
Notice that <code>!i</code> where <code>i:int</code> is not well-typed in our language.
Similarly, <code>true&lt;false</code> is not well-typed in our language.

<p>Two expressions (or statements) may be sequenced using the semi-colon operator, such that the type of the compound expression is the same as the type of the second expression.
If a new scope is created with an expression in its body, then the type of that new scope is the same as the type of its body.
<pre>
|- e1:T1    |- e2:T2
-------------------- [Sequence]
  |- e1;e2 : T2
</pre>
<pre>
 |- e:T
---------- [Scope]
 |- {e}:T
</pre>
For, example, the expression <code>{ { 2 + 3; 4; }; 5 }</code> evaluates to 5.

<h4>Assignment expression</h4>
<p>Now let's consider an assignment expression (or statement).  Recall that an assignment expression evaluates to the value that has been assigned, and its type is the type of the assigned variable.
<pre>
 |-x:T0  |-y:T1 T1&lt;:T0
-------------------------- [Assignment]
  |- x := y : T1
</pre>
This rule seems to be giving a valid type to the following expression: <code>1 := 2</code>, but this would be incorrect in our language. To support
an assignment, we need to
distinguish between a <em>reference type</em> and a <em>value type</em>.

<p>
For a primitive type <code>T</code>, its corresponding reference type is written <code>T&amp;</code>.
A reference type represents an <em>object</em> (region of memory) holding the corresponding value type. 
By
definition, <code>T&amp;</code> is a
subtype of <code>T</code>, i.e., <code>T&amp; &lt;: T</code>.

<p>Example: the following subtyping relations can be present in our language: <code>U&lt;:T</code>, <code>T&amp;&lt;:T</code>,
<code>U&amp;&lt;:U</code>, <code>U&amp;&lt;:T&amp;</code> (to form a diamond structure).

<p>
Thus, the assignment rule now becomes:
<pre>
 |-e0:T0&amp;  |-e1:T1 T1&lt;:T0
------------------------------- [Assignment]
  |- e0 := e1 : val(T1)
</pre>
Here <code>val(T1)</code> returns the value type of <code>T1</code> if <code>T1</code> is a reference type; else it returns <code>T1</code> itself.
Notice that the conclusion assigns a value type to the assignment expression, which <em>rejects</em> <code>(x := y) := z</code> expressions, but accepts <code>x := (y := z)</code>.
If we want to admit <code>(x := y) := z</code>, we may want to change the inferred type in the conclusion to <code>T1&amp;</code> (the type of <code>x</code>), but that would be quite non-intuitive, as that would likely mean that we are assigning <code>z</code> to <code>y</code> in the execution semantics.

<p>
The assignment rule admits the following code to be well-typed:
<pre>
class A { ... };
class B : A { int y; ... };
A a = B();
</pre>
If we replace this rule with a less general version like the following, then the code above does not remain well-typed.
<pre>
 |-x:T&amp;  |-y:T
------------------- [Assignment]
  |- x := y : T
</pre>
This above rule is sound but not precise, in the sense it does not admit all the programs that we would like to admit. This is similar to how a previous imprecise rule did not admit <code>(1+2)+3</code>.  

Notice that the conclusion assigns the more specific type <code>T1</code>, which <em>admits</em> <code>(A a = B()).y</code> as type correct.

<h4>While loop</h4>
<pre>
 |-e:TB  |-x:T  TB&lt;:bool
---------------------------- [While]
  |- while (e) x : void
</pre>
This is a design decision. One could have said that the type of a while loop is the type of the last statement that executes. But then what if the statement didn't execute even once?  Hence a type 'void' means that the statement has a type which is not usable.

<h4>Address-of</h4>
<pre>
   |-s:T&amp;
----------------------- [address-of]
  |- &amp;s : T *
</pre>
Notice that the address-of operator is only well-typed when used on a reference type, e.g., it is illegal to say <code>&amp;1</code>.

<h4>If-then-else</h4>
<pre>
    |- e1 : TB
    |- e2 : T2
    |- e3 : T3
    TB &lt;: bool
--------------------------------  [if-then-else]
|- if e1 then e2 else e3 : void
</pre>
Notice that it is by design that <code>if-then-else</code> always returns type, even when <code>T2=T3</code>.

<h4>Ternary</h4>
<pre>
    |- e1 : TB
    |- e2 : T2
    |- e3 : T3
    TB &lt;: bool
--------------------------------  [if-then-else]
|- e1 ? e2 : e3 : val(lub(T2,T3))
</pre>
An <em>upper bound</em> <code>U(T2,T3)</code> of types <code>T2</code> and <code>T3</code>, is defined so that the following
hold: <code>T2&lt;:U</code> and <code>T3&lt;U</code>.  A <code>least upper bound</code> <code>lub(T2,T3)</code>
is defined so that <code>lub</code> is an upper-bound of <code>T2</code> and <code>T3</code>,
and the further, for any other upper bound <code>U(T2,T3)</code>, <code>lub &lt;: U</code> holds.

<p>The <code>lub</code> need not be unique for a partially ordered set (poset), even
in the presence of a <code>void</code> type.  However, for our language,
it turns out that <code>lub</code> is unique.  If <code>lub</code> is not unique, this rule
should be modified appropriately, e.g., to resolve this ambiguity.  One option is to have
a hypothesis that requires that there must exist a unique <code>lub</code> of <code>T2</code>
and <code>T3</code> for this expression to be well-typed.

<p>The <code>val</code> operator ensures that this cannot be now used in the LHS of an assignment.

<h4>Variable</h4>
<p>But what is the type of a variable reference?
<pre>
   x is a variable
  ----------------  [Var]
      |- x:?
</pre>
The local, structural rule does not carry enough information to give <code>x</code> a type.  We need more information in the rules.

<p>A <em>type environment</em> gives types for <em>free</em> variables
<ul>
	<li>A type environment is a function from ObjectIdentifiers to Types
	<li>A variable is free in an expression if it is not defined within the expression
	<ul>
		<li><code>x</code> is free in expression <code>x</code>
		<li><code>x</code> is free in expression <code>x+y</code>
		<li><code>x</code> is free in expression <code>{int y = ...; x+y;}</code>
		<li><code>y</code> is a <em>bound variable</em> in expression <code>{int y = ...; x+y;}</code>
	</ul>
</ul>

<p>The sentence <code>O |- e:T</code> is read
<ul>
	<li>Under the assumption that free variables have the types given by O, it is provable (|-) that expression <code>e</code> has the type <code>T</code>
</ul>
<pre>
i is an integer literal (constant)
----------------------------------  [Int]
    O |- i:int
</pre>
<pre>
 O |- e1:int    O |- e2:int
----------------------------------  [Add]
    O |- e1+e2:int
</pre>
Notice that the same assumptions are required in both the hypotheses and the conclusion.

<p>And we can write our first rule that uses type environment <code>O</code>
<pre>
O(x) = T
-------------  [Var]
O |- x:T&amp;
</pre>
Notice that we choose to keep the value type in <code>O</code>, and use it
to assign the reference type to <code>x</code> --- this is a succinct way
of saying that all variables must be of a reference type.

<p>We allow a declaration only at the beginning of a scope; moreover, there can be
at most one declaration at the beginning of a scope, and multiple declarations require
multiple nested scopes.
<pre>
  O[T0/x] |- e1:T1
   T0 != void
----------------------------    [Let-No-Init]
 O |- { T0 x; e1 } : T1
</pre>
O[T/x] represents one function, where
<pre>
O[T/x](x) = T
O[T/x](y) = O(y)
</pre>
Notice that we use <code>T0/X</code> instead of <code>T0&amp;/X</code> --- that's because the <code>Var</code>
rule only expects the value type of the variable in the type environment, and uses it to assign a
reference type to the variable.

<p>
When we enter the scope, we add a new assumption in our type environment.
When we leave the scope, we remove the assumption.

<p>This terminology reminds us of the symbol table. So the type-environment is
stored in the symbol table.
<ul>
	<li>The type environment gives types to the free identifiers in the current scope
	<li>The type environment is passed down the AST from the root towards the leaves
	<ul>
		<li>To check the type of a new scope, we will see which rules can be applied
		<li>The Let-Init/Let-No-Init rule will indicate that we should try type-checking the body of the new scope with an updated environment (top-down): O[T/x]
	</ul>
	<li>Types are computed up the AST from the leaves towards the root.
</ul>

Our language also allows the initialization of a newly-declared variable.
<pre>
      O[T0/x] |- e1:T1
         O |- e2:T0
         T0 != void
----------------------------    [Let-Init]
 O |- { T0 x = e2; e1 } : T1
</pre>
Notice that this rule says that the initializer <code>e2</code> should have the same type <code>T0</code> as <code>x</code>. This is imprecise, we should ideally allow such assignment as long as <code>e2</code> is of a subtype of <code>T0</code>.

<p>A better version of [Let-Init] using subtyping:
<pre>
      O[T/x] |- e1:T1
         O |- e2:T0
       T0 &lt;: T
        T != void
----------------------------    [Let-Init]
 O |- { T x = e2; e1 } : T1
</pre>
Notice that <code>T0</code> only needs to be a subtype of <code>T</code> and not a subtype of <code>T&amp;</code>.  This allows <code>int x = 3</code>.
Notice that we disallow the construction of a term of type <code>void&amp;</code>.  Consequently, we also disallow the construction
of a term of type <code>void*</code>.

<!--
<p>
Similarly, a better version of [Assignment] using subtyping is:
<pre>
 O|-x:T0&amp;  O|-e1:T1   T1&lt;:T0
~---------------------------------~ [Assignment]
       O |- x=e1 : T1
</pre>
Notice that the type of the assignment statement is value type <code>T1</code>, so it can participate in more operations than <code>T0</code>. Also notice that it is not a reference type.
-->

<h3>Typing Methods</h3>
C++ example
<pre>
        O |- e1:T1
        ...
        O |- en:Tn
------------------------------ [Dispatch]
   O |- f(e1,e2,...,en):?
</pre>
Also maintain a mapping for method signatures in O
<pre>
O(f) = (T1,...,Tn,T(n+1))
</pre>
means that there is a method f such that
<pre>
f(x1:T1,x2:T2,x3:T3,...,xn:Tn):T(n+1)
</pre>
Hence, our dispatch rule becomes:
<pre>
        O |- e1:T1
        ...
        O |- en:Tn
        O |- f:(T1',..,Tn',T(n+1)')
        T1&lt;=T1',...Tn&lt;=Tn'
---------------------------------------- [Dispatch]
   O |- f(e1,e2,...,en):T(n+1)
</pre>
Notice that this tackles both call-by-value and call-by reference. For example,
<code>T1'</code> could be a reference type.  Further, a reference-type can be used as an argument where a value-type was expected; but not vice-versa.

<p>
Object-oriented languages also implement encapsulation (e.g., some functions are only visible in certain classes, etc.). To handle them, one can
extend O to be a function from a tuple of class-name and the identifier-name, e.g., <code>C.f</code> instead of <code>f</code>.
<!--  We can maintain a stack of <em>current class</em>,
and whenever we enter the scope of a class <code>C</code>, we can push <code>C</code> to the stack, and pop it upon leaving the scope.-->

<p>Example:
The following shows an example syntax of a method declaration and dispatch.
<pre>
class C {
   ....
   ...foo(T1 a1, ..., Tn an) .... //method declaration.
};

C c;
c.foo(....);
</pre>

<p>The following shows an example syntax of a method declaration and dispatch with inheritance (subtyping) where <code>D&lt;:C</code>.
<pre>
class C {
   ....
   ...foo(T1 a1, ..., Tn an) .... //method declaration.
};

D c;
c.foo(x1,...,xn);
</pre>
In this case, we will use <em>scoping rules</em> to resolve "which <code>foo</code>?".  For example, in this case, the <code>foo</code>
is <code>C</code>'s foo.  Notice that the scoping rule will need to know the type of <code>c</code> and potentially
the types of <code>x1..xn</code> to be able to identify "which <code>foo</code>?",
and so scoping and typing work hand-in-hand.  Irrespective, once the question has been answered, we annotate each such
dispatch with the class name corresponding to the method being dispatched, e.g., the dispatch in the example above becomes:
<pre>
D c;
c@C.foo(....);
</pre>
This disambiguation is required
to determine the type of the return value, e.g., <code>C.foo</code> may have a different
return type than <code>B.foo</code>.

<p>
To express inheritance, we will use the subtype-relation for the
<code>this</code> object in the method dispatch.
<pre>
     O |- e0:T0&amp;
     O |- e1:T1
     ...
     O |- en:Tn
     O |- T.f : (T1',..,Tn',T(n+1))
     T0 &lt;: T
     T1&lt;:T1', ...,  Tn&lt;:Tn'
---------------------------------------- [Static-Dispatch]
   O |- e0@T.f(e1,e2,...,en):T(n+1)
</pre>
Notice that we require <code>e0</code> to be a reference type.  In other words,
<code>e0</code> should represent of a region of memory, also called an <em>object</em>.

<h4>Type polymorphism examples</h4>
The following definitions can co-exist.
<ol>
<li><pre>int foo(int)</pre>
<li><pre>long foo(long)</pre>
<li><pre>string foo(string)</pre>
</ol>
Notice that <code>string foo(int)</code> cannot co-exist with the first <code>foo</code>.

<p>Type resolution in this case is performed by looking at the types of the arguments, and those definitions
are enabled where the types of actual arguments are respective subtypes of the formal arguments.
If no
definitions are enabled, this is a type error.
If more than one definitions are enabled, that is usually a type-ambiguity error.
(Notice that using resolution rules here like, most closely matching type, etc., are unlikely to
be intuitive for the programmer when there are multiple arguments and one argument matches more
closely for one candidate while another argument matches more closely for another candidate).

<h4>this keyword</h4>
<p>
For object-oriented languages, to resolve the <code>this</code>
keyword, we also need to know the "current class" C in which the expression is sitting.
To support this, we change the form of a typing rule (also called a <em>sentence</em> in logic) to:
<pre>
O,C |- e:T
</pre>
We use C=null for a context which is free of any "current class".

<p>
For example,
<pre>
 O,C |- e1:int    O,C |- e2:int
----------------------------------  [Add]
    O,C |- e1+e2:int
</pre>
The rule for the <code>this</code> keyword would be the following:
<pre>
  C != null
---------------  [This]
O,C : this: C*
</pre>

<h4>Summary</h4>
<ul>
	<li>Type rules are defined on the structure of expressions (through structural induction)</li>
	<li>Types of variables are modeled by an environment</li>
</ul>
Warning: Type rules are very compact! A lot of information in compact rules and it takes time to interpret them.

<h3>Implementing Type Checking</h3>
<ul>
<li>C type checking can be implemented in a single traversal over the AST.  This is not true for some other languages like OCaml for example, where multiple passes may be required.
<li>Type environment is passed down the tree
<ul>
	<li>From parent to child
	<li>Other languages may require multiple passes to construct the type environment at each node
</ul>
<li>Types are passed up the tree
<ul>
	<li>From child to parent
</ul>
</ul>

Let's consider the following rule:
<pre>
 O,C |- e1:int    O,C |- e2:int
----------------------------------  [Add]
    O,C |- e1+e2:int
</pre>
This says that to type-check <code>e1+e2</code>, then we have to type-check
<code>e1</code> and <code>e2</code> separately in the same O,C environment.

<pre>
TypeCheck(Environment, e1+e2) = {
  T1 = TypeCheck(Environment, e1);
  Check T1 == int;
  T2 = TypeCheck(Environment, e2);
  Check T2 == int;
  return int;
}
</pre>

Let's consider a more complex example:
<pre>
         O |- e2:T0
      O[T&amp;/x] |- e1:T1
       T0 &lt;: T
        T != void
----------------------------    [Let-Init]
 O |- { T x = e2; e1 } : T1
</pre>
Let's look at the corresponding type-checking implementation:
<pre>
TypeCheck(Environment, { T x = e0; e1 }) = {
  T0 = TypeCheck(Environment, e0);
  T1 = TypeCheck(Environment.add(x:T&amp;), e1);
  Check subtype(T0,T1);
  Check T != void;
  return T1;
}
</pre>

<p>Recall that we claimed that type inference and type checking are similar, in that they use the same typing rules.
The typing rules can also be used to implement type inference.  We can modify the <code>TypeCheck</code> function,
so that along with the <code>Environment</code>, it also passes down the acceptable types for a sub-expression, or
more generally <em>type constraints</em>.  At the end, these constraints can be solved to identify the types of
the leaf nodes of the AST to implement type inference.  If the constraints have no solution, it is a type error.
If the constraints have more than one solution, either there is a type ambiguity error, or there is a rule
to resolve the ambiguity. For example, the most <em>general</em> type may be used when
all the candidate types are ordered by the subtyping relation, i.e., the type that is the supertype
of all other candidates, e.g., \alpha-list is more general than int-list.

<h3>Static vs. Dynamic Typing</h3>
Languages with static type checking also have a notion of dynamic types, just that they may or may not implement
the dynamic checks. The dynamic type of a term is determined through the <em>execution semantics</em>.

<ul>
	The dynamic type of an object is the class C that is used in the "<code>C c</code>" (object) or "<code>C()</code>" (value) expression that created it.
	<ul>
		<li>A run-time notion
		<li>Even languages that are not statically typed have the notion of dynamic type
	</ul>
	<li>The static type of an expression captures all dynamic types the expression could have
	<ul>
		<li>A compile-time notion
	</ul>
</ul>

<p>If a typesystem is sound, we do not need to implement dynamic checks for the properties
that have been checked statically. For example, we do not need to dynamically check during
execution of <code>1+2</code> that <code>1</code> and <code>2</code> are both of type <code>int</code>.

<p>Consider C++ program:
<pre>
class A { ... }
class B : public A { ... }
void foo() {
  A* foo = new A;
  B* bar = new B;
  ....
  foo =  bar;
}
</pre>
Static type of foo is "A*", but the dynamic type of foo is "A*" and "B*" at different program points.

<p>Formalizing the relationship, for a sound typesystem: for all expressions E, dynamic_type(E) &lt;: static_type(E)

<p>In all executions, E evaluates to values of the type inferred by the compiler. You have to actually run the program to get the dynamic_type. In the early days of programming languages, equality (instead of subtype relation) was proved for their type systems.

<!--<p>In other words, a static typechecker will not accept any program that would have failed
the dynamic typechecker <em>of equal precision</em>. In other words, all dynamically
type-incorrect programs (for the types being checked statically) would be rejected
by the static typechecker.-->

<p>Notice that rejecting all programs is sound.  That's why we also care about <em>precision</em>,
i.e., how many programs we can willingly accept.

<h4>Completeness</h4>

All dynamically type-correct programs are <em>accepted</em> by the static typechecker. Consider the
following program:
<pre>
C c;
D d; //where D is a subtype of C
....
D d2 = cond ? c : d;
</pre>
Let's say that at runtime <code>cond</code> can never be false, and so this program is dynamically type-correct.
However, statically figuring out that <code>cond</code> is never false is undecidable.

<p>Show a Venn diagram: statically-type-correct &lt; dynamically-type-correct &lt; parseable.
For soundness, <code>statically-type-correct &lt; dynamically-type-correct</code> should hold.
For completeness, <code>dynamically-type-correct &lt; statically-type-correct</code> should hold.

<p>All operations that can be used on an object of type C can also be used on an object of type C' &lt;= C.
<ul>
	<li>Such as fetching the value of an attribute
	<li>Or invoking a method on the object
</ul>
Subclasses <em>only add</em> attributes or methods (they never remove attributes/methods).

<p>The dynamic type is obtained through the execution semantics of the program, e.g., if we have an expression <code>x++</code>, and the current state of the program determines <code>x</code> to be of type <code>int&amp;</code>, there is a dynamic typing rule that says that the type of the new expression is also <code>int&amp;</code>. Consider the example <code>{ T x = e0; x; }</code> where <code>e0:T0 &lt;: T</code>; here the dynamic type of the expression is <code>T0</code> (not <code>T</code>!). Similarly, the dynamic
type of <code>if x then y:T1 else Y:T2</code> will be either <code>T1</code> or <code>T2</code> (not <code>lub(T1,T2)</code> or <code>void</code>).

<p>In other words, soundness states that the static type system will not accept any incorrect program (that will not pass the dynamic type check of equal power). A dynamic type check for array-bounds is not of equal power (it has more checks enabled); a sound static type check for array-bounds would reject all incorrect programs (but it will also reject a few more that will actually pass the dynamic type check).

<p>Soundness of static type system: all dynamically-type-incorrect programs will be rejected. Ensured by ensuring that static_type is a supertype of dynamic_type. A trivial static-type system that rejects all programs is sound (but not useful).

<p>Completeness: all dynamically-type-correct programs will be accepted. Not possible to ensure both soundness and completeness in general.

<h3>Example where static type system can be too restrictive</h3>
While a static type system may be sound, it may be too restrictive and
may disallow certain programs that may be dynamically well-typed.
<pre>
class Count {
  int i = 0; //default value = 0
  Count inc() { i := i + 1; return *this; }
};
</pre>
Now consider a subclass <code>Stock</code> of <code>Count</code>:
<pre>
class Stock : public Count {
  string name; //name of the item
};
</pre>
And the following use of <code>Stock</code>:
<pre>
Stock a;
Stock b = a.inc();
... b.name ...
</pre>
This code does not type-check because the return value of <code>inc</code>
is <code>Count</code> which is not a subtype of <code>Stock</code>.

<p>This seems like a major limitation as now the derived classes (subtypes) will be unable to use the <code>inc</code> method.

<p><code>a.inc()</code> has <em>dynamic type</em> <code>Stock</code>.

<p>So dynamically speaking, it is legitimate to write the following:
<code>
	Stock b := a.inc();
</code>
But this is not well-typed as
<li><code>a.inc()</code> has <em>static type</em> <code>Count</code>.

<p>Common workarounds to the incompleteness of a static type system:
<ul>
	<li>We can extend the type system. Different languages extend the type system in different directions
	<li>Option 1: Use <code>dynamic_cast</code>: returns nullptr at runtime if not-successful; else returns a pointer to the object of the new type. Allows bypassing the static type system. May entail runtime cost.
	<li>Option 2: C++ Template : pass subtype as argument to the supertype
		<pre>
template&lt;typename T&gt;
class Count&lt;T&gt; {
  int i = 0;
	T inc() { i &lt;-- i + 1; return *static_cast&lt;T *&gt;(this); } //static_cast gets checked at compile-time!
}

class Stock : public Count&lt;Stock&gt;
{
  ...
}
</pre>
The use of <code>static_cast</code> is only a convenience, as the compiler will check if it is guaranteed that
<code>this</code> can be type-casted to <code>T*</code> at compile-time (potentially using an analysis that is
external to the type-rules that we have discussed so far).  One could replace <code>static_cast</code> with
<code>dynamic_cast</code> with the same effect (except that the compiler will no longer check the cast at compile time).
</li>
</ul>

<h3>Error Recovery</h3>
<ul>
	<li> Detecting where errors occur is easier than in parsing
	<li> Introduce a new type <code>No_type</code> for use with ill-typed expressions
	<li>Define <code>No_type &lt;: C</code> for all types <code>C</code>. Avoids cascading type errors due to one type-error.
	<li>Thus, every operation is defined for <code>No_type</code>
	<ul>
		<li>With a <code>No_type</code> result
	</ul>
	<li>The type hierarchy is not a tree anymore, it is a DAG with <code>No_type</code> at the bottom.  A DAG may also occur due to multiple inheritance for example.</li>
</ul>