\documentclass{article}
\usepackage[instructions]{hw}
\newcommand{\hw}{{\lang} Type System Specification}
\newcommand{\topic}{Cornell University}
\usepackage{import}
\subimport{../hw/}{hw-header}

\usepackage{mathpazo}
\usepackage{amssymb}

\usepackage{xr}
\externaldocument[:language:]{language}

\newcommand\hmul{\texttt{*\char62\char62}}

\newcommand{\kw}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\st}{\ensuremath{\leq}}
\newcommand{\pr}{\ensuremath{^{\prime}}}
\newcommand{\dpr}{\ensuremath{^{\prime\prime}}}
\newcommand\unit{\kw{unit}}
\newcommand\Grho{Γ(ρ)}
\newcommand\Gbeta{Γ(β)}

\newcommand{\PC}{\ensuremath{Γ ⊢}}
\newcommand{\PCs}[1]{\ensuremath{Γ#1\rho\beta ⊢_s}}
\newcommand{\PCloop}{\ensuremath{Γ\rho~\kw{true} ⊢_s}}

\newcommand\typeof{\mathit{typeof}}
\newcommand\varsof{\mathit{varsof}}

\newcommand\fd{\mathit{fd}}

\allowdisplaybreaks

\begin{document}
\headerBase{\\Version of \today}

\section{Changes}
\begin{itemize}
\item 3/3: Corrected typing rules that involves adding a new binding to the
typing context.  Headers such as "var" were missing in the new binding.
\item 2/27: Fixed \textsc{If} and \textsc{While} typing rules. A
little more clarifying text added about unit vs. void.
\item 2/26: Clarified rules for "use" declarations.
%\item None yet; watch this space.  % Do not delete this line; comment instead.
\end{itemize}

\section{Types}
The {\lang} type system uses a somewhat bigger set of types than can
be expressed explicitly in the source language:
\[
\begin{aligned}[t]
τ &::= \kw{int} \\
& \bnf  \kw{bool} \\
& \bnf \arrayof{τ}
\end{aligned}
\qquad\qquad
\begin{aligned}[t]
T &::= τ \\
& \bnf \unit \\
& \bnf (τ_1,τ_2,\ldots,τ_n) ~~ ^{n≥2}
\end{aligned}
\qquad\qquad
\begin{aligned}[t]
R &::= \kw{unit} \\
& \bnf \kw{void}
\end{aligned}
\qquad\qquad
\begin{aligned}[t]
\sigma & ::= "var"~τ \\
& \bnf "ret"~T \\
& \bnf "fn"~T \to T' 
\end{aligned}
\]
%
Ordinary types expressible in the language are denoted by the metavariable $τ$,
which can be \kw{int}, \kw{bool}, or an array type.

The metavariable $T$ denotes an expanded notion of type that represents 
possible types in procedures, functions, and multiple assignments.
It may be an ordinary type, \unit, or a tuple type.

The type {\unit} does not appear explicitly in the source language.
This type is given to an element on the left-hand side of
multiple assignments that uses the "_" placeholder, allowing their
handling be integrated directly into the type system. The {\unit} type
is also used to represent the result type of procedures.

Tuple types represent the parameter types of procedures and functions that take
multiple arguments, or the return types of functions that return multiple
results.

The metavariable $R$ represents the outcome of evaluating a statement,
which can be either \kw{unit} or \kw{void}.
The \kw{unit} type is the
the type of statements that _might_ complete normally and permit the
following statement to execute.  The type \kw{void} is the
type of statements such as \kw{return} that _never_ pass control to the following
statement. The \kw{void} type should not be confused with the C/Java type \kw{void}, which
is actually closer to \kw{unit}.

The set $\sigma$ is used to represent typing-environment entries,
which can either be normal variables (bound to $"var"~τ$ for some type $τ$),
return types (bound to $"ret"~T$),
functions (bound to $"fn"~T\to T'$ where $T'≠\unit$),
or procedures (bound to $"fn"~T\to\unit$),
where the ``result type'' $\unit$ indicates that the procedure
result contains no information other than that the procedure call
terminated.

\section{Subtyping}
The subtyping relation on $T$ is the least partial order consistent with
this rule:
\[
  \infer{τ \st \unit}{} 
\]
For now, however, there is no subsumption rule, so subtyping matters only
where it appears explicitly.

\section{Type-checking expressions}
To type-check expressions, we need to know what bound variables and functions
are in scope; this is represented by the typing context $Γ$,
which maps names $x$ to types $\sigma$.

The judgment $Γ ⊢ e:T$ is the rule for the type of an expression;
it states that with bindings $Γ$ we can conclude that $e$ has the type $T$.

We use the metavariable symbols $x$ or $f$ to represent arbitrary
identifiers, $\nm{n}$ to represent an integer literal constant,
$\nm{string}$ to represent a string literal constant, and
$\nm{char}$ to represent a character literal constant.
Using these conventions, the expression typing rules are:
\begin{gather*}
  \infer{Γ ⊢ \nm{n}: \kw{int}}{} \qquad
  \infer{Γ ⊢ \kw{true}: \kw{bool}}{} \qquad
  \infer{Γ ⊢ \kw{false}: \kw{bool}}{} \qquad
  \infer{Γ ⊢ \nm{string}: \arrayof{\kw{int}}}{} \qquad
  \infer{Γ ⊢ \nm{char}: \kw{int}}{}\\ \\
  \infer{Γ ⊢ x: τ}{Γ(x) = "var"~τ} \qquad
  \infer{Γ ⊢ e_1 \oplus e_2: \kw{int}}
            {Γ ⊢ e_1: \kw{int} & Γ ⊢ e_2: \kw{int} &
                    \oplus \in \set{"+","-","*",\hmul,"/","\%" }} \\ \\
  \infer{Γ ⊢ "-$e$":\kw{int}}{Γ ⊢ e: \kw{int}} \qquad
  \infer{Γ ⊢ e_1 \ominus e_2: \kw{bool}}
            {Γ ⊢ e_1: \kw{int} & Γ ⊢ e_2: \kw{int} &
                    \ominus \in \{"==","!=","<","<=",">",">="\}} \\ \\
% boolean ops.
  \infer{Γ ⊢ "!$e$":\kw{bool}}{Γ ⊢ e: \kw{bool}} \qquad
  \infer{Γ ⊢ e_1 \ominus e_2: \kw{bool}}
            {Γ ⊢ e_1: \kw{bool} & Γ ⊢ e_2: \kw{bool} &
                    \ominus \in \{"==","!=","\&","|"\}} \\ \\
% array ops.
  \infer{Γ⊢ "\kw{length}($e$)":\kw{int}}{Γ ⊢ e:\arrayof{τ}} \qquad
  \infer{Γ ⊢ e_1 \ominus e_2: \kw{bool}}
            {Γ ⊢ e_1: \arrayof{τ} &
                    Γ ⊢ e_2: \arrayof{τ} & \ominus \in \{"==","!="\}} \\ \\
  \infer{Γ⊢"\{$e_1$,$\ldots$,$e_n$\}": \arrayof{τ}}
            {Γ⊢  e_1:τ & \ldots & Γ⊢  e_n:τ & n ≥ 0} \qquad
  \infer{Γ⊢ "$e_1$[$e_2$]":τ}{Γ ⊢ e_1:\arrayof{τ} & Γ ⊢ e_2:\kw{int}} \qquad
  \infer{Γ⊢ "$e_1$ + $e_2$":\arrayof{τ}}{Γ ⊢ e_1:\arrayof{τ} & Γ ⊢ e_2:\arrayof{τ}} \\ \\
  \infer{Γ⊢"$f$()":T'}
            {Γ(f) = \kw{fn}~\unit\to T' & T'\neq\unit} \qquad
  \infer{Γ⊢"$f$($e$)":T'}
            {Γ(f) = \kw{fn}~τ\to T' & T'\neq\unit & Γ⊢ e:τ} \\ \\
  \infer{Γ⊢"$f$($e_1$,$\ldots$,$e_n$)":T'}
            {Γ(f) = \kw{fn}~(τ_1,\ldots,τ_n)\to T' & T'\neq\unit & Γ⊢ e_i:τ_i ~~ ^{(∀i∈1..n)} & n ≥ 2}
\end{gather*}

\section{Type-checking statements}

To type-check statements, we need all the information used to type-check
expressions, plus the types of procedures, which are included in $Γ$.
In addition, we extend the domain of
$Γ$ a little to include a special symbol $ρ$.
To check the $\kw{return}$ statement we need to know what the return type of the
current function is or if it is a procedure.
Let this be denoted by $\Grho="ret"~T$,
where $T≠\unit$ if the statement is part of a function, 
or $T=\unit$ if the statement is part of a procedure.  Since
statements include declarations, they can also produce new variable bindings,
resulting in an updated typing context which we will denote as $Γ'$.
To update typing contexts, we write $Γ[x\mapsto "var"~τ]$,
which is an environment exactly like $Γ$ except that it maps $x$ to $"var"~τ$.
We use the metavariable $s$ to denote a statement, so
the main typing judgment for statements has the form
$Γ⊢s:R,Γ'$.

Most of the statements are fairly straightforward and do not change $Γ$:
\begin{gather*}
  \infer[\rnm{Seq}]
            {\PC "\{$s_1$ $s_2$ $\ldots$ $s_n$\}" : R,Γ}
            {\PC s_1 : \kw{unit},Γ_1 & Γ_1⊢s_2:\kw{unit},Γ_2 &\ldots& Γ_{n-1}⊢ s_n : R,Γ_{n}} \\ \\
  \infer[\rnm{If}]{\PC "\kw{if} ($e$) $s$" : \kw{unit},Γ}{Γ ⊢ e:\kw{bool} & \PC s : R,Γ'} \qquad
  \infer[\rnm{IfElse}]
            {\PC "\kw{if} ($e$) $s_1$ \kw{else} $s_2$" : \nm{lub}(R_1,R_2),Γ}
            {Γ ⊢ e:\kw{bool} & \PC s_1 : R_1,Γ' & \PC s_2 : R_2,Γ''} \\ \\
  \infer[\rnm{While}]{\PC "\kw{while} ($e$) $s$" : \kw{unit},Γ}
            {Γ ⊢ e:\kw{bool} & Γ⊢ s : R,Γ'} \\ \\
  \infer[\rnm{PrCallUnit}]{\PC "$f$()" : \kw{unit},Γ}{Γ(f) = \kw{fn}~\unit\to\unit} \qquad
  \infer[\rnm{PrCall}]{\PC "$f$($e$)" : \kw{unit},Γ}{Γ(f) = \kw{fn}~τ\to\unit & Γ ⊢ e:τ} \\ \\
  \infer[\rnm{PrCallMulti}]{\PC "$f$($e_1$,$\ldots$,$e_n$)" : \kw{unit},Γ}
        {Γ(f) = \kw{fn}~(τ_1,\ldots,τ_n)\to\unit & Γ⊢ e_i:τ_i ~~ ^{(∀i∈1..n)} & n ≥ 2} \\ \\
  \infer[\rnm{Return}]{\PC \kw{return} : \kw{void},Γ}{\Grho = "ret"~\unit} \qquad
  \infer[\rnm{RetVal}]
        {\PC "\kw{return} $e$" : \kw{void},Γ}
        {\Grho = "ret"~τ & Γ ⊢ e:τ} \\ \\
  \infer[\rnm{RetMulti}]
        {\PC "\kw{return} $e_1$, $e_2$, $\ldots$, $e_n$" : \kw{void},Γ}
        {\Grho = "ret"~(τ_1,τ_2,\ldots,τ_n) & Γ⊢ e_i:τ_i ~~ ^{(∀i∈1..n)} & n ≥ 2}
\end{gather*}
The function \nm{lub} is defined as follows:
\[
\nm{lub}(R,R)=R \qquad
\nm{lub}(\kw{unit},R)=\nm{lub}(R,\kw{unit})=\kw{unit}
\]
Therefore, the type of an "if" is \kw{void} only if
all branches have that type.

Assignments require checking the left-hand side to make sure it
is assignable:
\begin{gather*}
  \infer[\rnm{Assign}]{Γ⊢"$x$ = $e$" : \kw{unit},Γ}{Γ(x) = "var"~τ & Γ⊢ e:τ} \qquad
  \infer[\rnm{ArrAssign}]{Γ⊢"$e_1$[$e_2$] = $e_3$" : \kw{unit},Γ}
            {Γ⊢ e_1 : \arrayof{τ} & Γ ⊢ e_2:\kw{int} & Γ ⊢ e_3 : τ}
\end{gather*}

Declarations are the source of new bindings. Three kinds of declarations
can appear in the source language: variable declarations,
multiple assignments, and function/procedure declarations. We are only
concerned with the first two kinds within a function body. To handle
multiple assignments, we define a declaration $d$ that can appear within
a multiple assignment:
%
\[ d ::= "$x$:$τ$" \bnf "_" \]
%
and define functions $\typeof(d)$ and $\varsof(d)$
as follows:
\[
\begin{array}{ll}
\typeof("$x$:$τ$") = τ & \typeof("_") = \unit \\
\varsof("$x$:$τ$") = \set{x} & \varsof("_") = ∅
\end{array}
\]
Using these
notations, we have the following rules:

\begin{gather*}
  \infer[\rnm{VarDecl}]{Γ⊢"$x$:$τ$" : \kw{unit},Γ[x \mapsto "var"~τ]}{x∉\dom{Γ}} \qquad
  \infer[\rnm{VarInit}]{Γ⊢"$x$:$τ$ = $e$" : \kw{unit},Γ[x \mapsto "var"~τ]}{x∉\dom{Γ} & Γ⊢ e: τ} \\ \\
  \infer[\rnm{ArrayDecl}]
        {Γ⊢"$x$:$τ$[$e_1$]$\ldots$[$e_n$]$\underbrace{"[]"\ldots"[]"}_{m}$" : 
            \kw{unit},Γ[x \mapsto "var"~τ\underbrace{"[]"\ldots"[]"}_{n+m}]}
        {x∉\dom{Γ} & Γ⊢ e_i:\kw{int} ~~ ^{(∀i∈1..n)} & n ≥ 1 & m ≥ 0} \\ \\
  \infer[\rnm{MultiAssign}]
        {Γ⊢"$d_1$,$\ldots$,$d_n$ = $e$" :
            \kw{unit},Γ[x_i↦"var"~\typeof(d_i) ~~ ^{(\forall i\in 1..n\forall x_i.\varsof(d_i)=\set{x_i})}]}
    {
      \begin{gathered}
        Γ⊢e : (τ_1,\ldots,τ_n) \quad
        τ_i ≤ \typeof(d_i) ~~ ^{(∀i∈1..n)} \\
        \dom{Γ}∩\varsof(d_i) = ∅ ~~ ^{(∀i∈1..n)} \quad
        \varsof(d_i)∩\varsof(d_j) = ∅ ~~ ^{(∀i,j∈1..n.j≠i)}
      \end{gathered}
    }
\end{gather*}
%
The final premise in rule {\sc MultiAssign} prevents shadowing by
ensuring that $\dom{Γ}$ and all of the $\varsof(d_i)$'s
are disjoint from each other.

\section{Checking top-level declarations}
\label{sec:top-decl}

At the top level of the program, we need to figure out the types of
procedures and functions, and make sure their bodies are well-typed. Since
mutual recursion is supported, this needs to be done in two passes. First, we
use the judgment $Γ ⊢ \fd : Γ'$ to state that the function or
procedure declaration $\fd$ extends top-level bindings $Γ$ to $Γ'$:
\begin{gather*}
  \infer{Γ ⊢ "$f$() $s$" : Γ[f\mapsto\kw{fn}~\unit\to \unit]}
        { f∉ \dom{Γ}} \qquad
  \infer{Γ ⊢ "$f$($x$:$τ$) $s$" : Γ[f\mapsto\kw{fn}~τ\to \unit]}
        { f∉ \dom{Γ}} \\ \\
  \infer{Γ ⊢ "$f$($x_1$:$τ_1$,$\ldots$,$x_n$:$τ_n$) $s$" : Γ'}
        { f∉ \dom{Γ} & Γ' = Γ[f\mapsto\kw{fn}~(τ_1,\ldots,τ_n)\to \unit] & n ≥ 2} \\ \\
  \infer{Γ ⊢ "$f$():$τ'$ $s$" : Γ[f\mapsto\kw{fn}~\unit\to τ']}
        { f∉ \dom{Γ}} \qquad
  \infer{Γ ⊢ "$f$($x$:$τ$):$τ'$ $s$" : Γ[f\mapsto\kw{fn}~τ\to τ']}
        { f∉ \dom{Γ}} \\ \\
  \infer{Γ ⊢ "$f$($x_1$:$τ_1$,$\ldots$,$x_n$:$τ_n$):$τ'$ $s$" : Γ'}
        { f∉ \dom{Γ} & Γ' = Γ[f\mapsto\kw{fn}~(τ_1,\ldots,τ_n)\to τ'] & n ≥ 2} \\ \\
  \infer{Γ ⊢ "$f$():$τ'_1$,$\ldots$,$τ'_m$ $s$" : Γ'}
        { f∉ \dom{Γ} & Γ' = Γ[f\mapsto\kw{fn}~\unit\to (τ'_1,\ldots,τ'_m)] & m ≥ 2} \\ \\
  \infer{Γ ⊢ "$f$($x$:$τ$):$τ'_1$,$\ldots$,$τ'_m$ $s$" : Γ'}
        { f∉ \dom{Γ} & Γ' = Γ[f\mapsto\kw{fn}~τ\to (τ'_1,\ldots,τ'_m)] & m ≥ 2} \\ \\
  \infer{Γ ⊢ "$f$($x_1$:$τ_1$,$\ldots$,$x_n$:$τ_n$):$τ'_1$,$\ldots$,$τ'_m$ $s$" : Γ'}
        { f∉ \dom{Γ} & Γ' = Γ[f\mapsto\kw{fn}~(τ_1,\ldots,τ_n)\to (τ'_1,\ldots,τ'_m)] & n ≥ 2 & m ≥ 2} \\ \\
\end{gather*}

The second pass over the program is captured by the judgment $Γ ⊢
\fd~~"def"$, which defines how to check well-formedness of each
function definition against a top-level environment $Γ$, ensuring that
parameters do not shadow anything and that the body is well-typed.
We treat procedures just like functions that return the {\unit} type.
The body of a procedure definition may have any type, but
the body of a function definition must have type \kw{void}, which ensures
that the function body does not fall off the end without returning.
\begin{gather*}
  \infer{Γ⊢ "$f$() $s$"~~"def"}
        {Γ[ρ↦"ret"~\unit] ⊢ s : R,Γ'} \qquad
  \infer{Γ⊢ "$f$($x$:$τ$) $s$"~~"def"}
        {x ∉ \dom{Γ} & Γ[x↦"var"~τ, ρ↦"ret"~\unit] ⊢ s : R,Γ'} \\ \\
  \infer{Γ⊢ "$f$($x_1$:$τ_1$,$\ldots$,$x_n$:$τ_n$) $s$"~~"def"}
    {
      \begin{gathered}
        |\dom{Γ} ∪ \{x_1,\dots,x_n\}| = |\dom{Γ}| + n \quad n ≥ 2\\
        Γ[x_1↦"var"~τ_1, \dots, x_n↦"var"~τ_n, ρ↦"ret"~\unit] ⊢  s : R,Γ'
      \end{gathered}
    } \\ \\
  \infer{Γ⊢ "$f$():$τ'$ $s$"~~"def"}
        {Γ[ρ↦"ret"~τ'] ⊢ s : \kw{void},Γ'} \qquad
  \infer{Γ⊢ "$f$($x$:$τ$):$τ'$ $s$"~~"def"}
        {x ∉ \dom{Γ} & Γ[x↦"var"~τ, ρ↦"ret"~τ'] ⊢ s : \kw{void},Γ'} \\ \\
  \infer{Γ⊢  "$f$($x_1$:$τ_1$,$\ldots$,$x_n$:$τ_n$):$τ'$ $s$"~~"def"}
    {
      \begin{gathered}
        |\dom{Γ} ∪ \{x_1,\dots,x_n\}| = |\dom{Γ}| + n \quad n ≥ 2 \\
        Γ[x_1↦"var"~τ_1, \dots, x_n↦"var"~τ_n, ρ↦"ret"~τ'] ⊢  s : \kw{void},Γ'
      \end{gathered}
    } \\ \\
  \infer{Γ⊢ "$f$():$τ'_1$,$\ldots$,$τ'_m$ $s$"~~"def"}
        {Γ[ρ↦"ret"~(τ'_1,\ldots,τ'_m)] ⊢ s : \kw{void},Γ' & m ≥ 2} \\ \\
  \infer{Γ⊢ "$f$($x$:$τ$):$τ'_1$,$\ldots$,$τ'_m$ $s$"~~"def"}
        {x ∉ \dom{Γ} & Γ[x↦"var"~τ, ρ↦"ret"~(τ'_1,\ldots,τ'_m)] ⊢ s : \kw{void},Γ' & m ≥ 2} \\ \\
  \infer{Γ⊢  "$f$($x_1$:$τ_1$,$\ldots$,$x_n$:$τ_n$):$τ'_1$,$\ldots$,$τ'_m$ $s$"~~"def"}
    {
      \begin{gathered}
        |\dom{Γ} ∪ \{x_1,\dots,x_n\}| = |\dom{Γ}| + n \quad n ≥ 2 \quad m ≥ 2\\
        Γ[x_1↦"var"~τ_1, \dots, x_n↦"var"~τ_n, ρ↦"ret"~(τ'_1,\ldots,τ'_m)] ⊢  s : \kw{void},Γ'
      \end{gathered}
    }
\end{gather*}

\section{Checking a program}

Using the previous judgments, we can define when an entire program
$\fd_1~\fd_2~\ldots~\fd_n$ that does not contain a "use" declaration
is well-formed, written $⊢ \fd_1~\fd_2~\ldots~\fd_n~~"prog"$:

\[
\infer{⊢ \fd_1~\fd_2~\ldots~\fd_n~~"prog"}
{
     ∅ ⊢ \fd_1 : Γ_1 &
     Γ_1 ⊢\fd_2 : Γ_2 &
     \ldots &
     Γ_{n-1} ⊢ \fd_n : Γ &
     Γ ⊢ \fd_i~~"def" ~~ ^{(∀i∈1..n)}
}
\]

For brevity, the rules for adding declarations appearing in interfaces are
omitted.  These rules are slightly different from those of the form
$Γ ⊢ \fd : Γ'$ in Section~\ref{sec:top-decl}, where $f∉ \dom{Γ}$ is replaced
with appropriate conditions.
Once added, these declarations also permits declarations in the source file
of identical signature.  See Section~\extref{:language:sec:interfaces} of
the {\lang} Language Specification.
\end{document}
