320Caml Specification

<int>    ::= ; see OCaml docs ;
<float>  ::= ; see OCaml docs ;
<bool>   ::= true | false

<expr>   ::= <int> | <float> | <bool>
<ty>     ::= int | float | bool

Every literal is a well-formed expression by fiat.

In the case of Boolean values, we can make the syntax explicit: there are two literals, \(\codel{true}\) and \(\codel{false}\). For the other literals, we're going to have to use our intuition for now; we know what integer literals look like.¹

We additionally state that \(\codel{int}\), \(\codel{float}\), and \(\codel{bool}\) are well-formed types.

Example: Since \(\codel{2}\) an integer number literal, it is a well-formed expression. The literal \(\codel{true}\) is a well-formed expression.

Note: The rules for literals (and variables) are axioms, i.e., they have no premises. When building a derivation you will always have these rules at the leaves of the derivation tree.

Note: Several of the rules below have side conditions as premises. These are conditions which are not typing judgments, but are required in order to apply the rule. Side conditions do not appear in derivations (see the examples below). We are careful to write all side conditions in \(\side{\text{green}}\).

\[ \uniinf {\side{\texttt{n} \text{ is an integer literal}}} {\tyj{\Gamma}{\texttt{n}}{\int}} {intLit} \]

Every integer number literal is of type \(\codel{int}\) in any context.

\[ \uniinf {\side{\texttt{n} \text{ is an float literal}}} {\tyj{\Gamma}{\texttt{n}}{\float}} {floatLit} \]

Every floating-point number literal is of type \(\codel{float}\) in any context.

\[ \uniinf {} {\tyj{\Gamma}{\true}{\bool}} {trueLit} \qquad \uniinf {} {\tyj{\Gamma}{\false}{\bool}} {falseLit} \]

The literals \(\codel{true}\) and \(\codel{false}\) are of type \(\codel{bool}\) in any context.

Example: Since \(\codel{35}\) is a integer literal, the literal \(\codel{35}\) is of type \(\int\) in the empty context, i.e., the following is a valid derivation.

\[ \uniinf {} { \tyj \emptyCtxt {\codel{35}} \int } {stringLit} \]

\[ \uniinf {\side{\texttt{n} \text{ is an integer literal}}} {\evj{\texttt{n}}{n}} {intLitEval} \]

The integer number literal \(\texttt{n}\) evaluates to the number \(n\) that it denotes.

\[ \uniinf {\side{\texttt{n} \text{ is an float literal}}} {\evj{\texttt{n}}{n}} {floatLitEval} \]

The floating-point number literal \(\texttt{n}\) evaluates to the number \(n\) that it denotes.

\[ \uniinf {} {\evj{\true}{\top}} {trueLitEval} \qquad \uniinf {} {\evj{\false}{\bot}} {falseLitEval} \]

The literal \(\true\) evaluates to the Boolean value \(\top\). The literal \(\false\) evaluates to the Boolean value \(\bot\).

Example: Since \(\codel{3.14}\) is floating-point number literal, the literal \(\codel{3.14}\) evaluates to the number \(3.14\), i.e., the following is a valid derivation.

\[ \uniinf {} {\evj{\codel{3.14}}{3.14}} {evalLitEval} \]

<var>  ::= ; see OCaml docs ;
<expr> ::= <var>

Every variable is a well-formed expression. As with number literals, we will not make the syntax of a variable explicit, but will take a variable to be alphanumeric with underscores and single-quotes, not starting with a capital letter (as in OCaml).

\[ \uniinf {\side{(x : \tau) \in \Gamma}} {\tyj{\Gamma}{x}{\tau}} {var} \]

If the variable \(x\) is declared to be of type \(\tau\) in \(\Gamma\) (i.e., the declaration \((x : \tau)\) appears in \(\Gamma\)), then \(x\) is of type \(\tau\) in the context \(\Gamma\).

Example: Since \((\codel{x} : \codel{int})\) appears in the context \(\{\codel{x} : \int, \codel{y} : \bool\}\), we have that \(x\) is of type \(\int\) in this context, i.e. the following is a valid derivation.

\[ \uniinf {} {\tyj{\{ \codel{x} : \int, \codel{y} : \int \}}{\codel x}{\int}} {var} \]

There are no semantic rules for variables. If at any point you need to evaluate a variable, it's because the original expression was not well-scoped.

<op>   ::= + | - | * | / | mod
         | +. | -. | *. | /.
         | && | ∣∣
         | = | <> | < | <= | > | >=
<expr> ::= <expr> <op> <expr>

The symbol \(\codel{+}\), \(\codel-\), \(\codel *\), \(\codel/\), \(\codel{mod}\), etc. are well-formed operators.

If \(\square\) is a well-formed operator and \(e_1\) and \(e_2\) are well-formed expressions, then \(e_1 \ \square \ e_2\) is a well-formed expression.

\[ \bininf {\tyj \Gamma {e_1} {\int}} {\tyj \Gamma {e_2} {\int}} {\tyj \Gamma {e_1 \plus e_2}{\int}} {addInt} \qquad \bininf {\tyj \Gamma {e_1} {\int}} {\tyj \Gamma {e_2} {\int}} {\tyj \Gamma {e_1 \times e_2}{\int}} {mulInt} \] \[ \bininf {\tyj \Gamma {e_1} {\int}} {\tyj \Gamma {e_2} {\int}} {\tyj \Gamma {e_1 \minus e_2}{\int}} {subInt} \qquad \bininf {\tyj \Gamma {e_1} {\int}} {\tyj \Gamma {e_2} {\int}} {\tyj \Gamma {e_1 \divby e_2}{\int}} {divInt} \] \[ \bininf {\tyj \Gamma {e_1} {\int}} {\tyj \Gamma {e_2} {\int}} {\tyj \Gamma {e_1 \modby e_2}{\int}} {modInt} \]

\[ \bininf {\tyj \Gamma {e_1} {\float}} {\tyj \Gamma {e_2} {\float}} {\tyj \Gamma {e_1 \plusd e_2}{\float}} {addFloat} \qquad \bininf {\tyj \Gamma {e_1} {\float}} {\tyj \Gamma {e_2} {\float}} {\tyj \Gamma {e_1 \timesd e_2}{\float}} {mulFloat} \] \[ \bininf {\tyj \Gamma {e_1} {\float}} {\tyj \Gamma {e_2} {\float}} {\tyj \Gamma {e_1 \minusd e_2}{\float}} {subFloat} \qquad \bininf {\tyj \Gamma {e_1} {\float}} {\tyj \Gamma {e_2} {\float}} {\tyj \Gamma {e_1 \divbyd e_2}{\float}} {divFloat} \] \[ \bininf {\tyj \Gamma {e_1} {\bool}} {\tyj \Gamma {e_2} {\bool}} {\tyj \Gamma {e_1 \andb e_2} {\bool}} {and} \qquad \bininf {\tyj \Gamma {e_1} {\bool}} {\tyj \Gamma {e_2} {\bool}} {\tyj \Gamma {e_1 \orb e_2} {\bool}} {or} \] \[ \bininf {\tyj{\Gamma}{e_1}{\tau}} {\tyj{\Gamma}{e_2}{\tau}} {\tyj{\Gamma}{e_1 \eqc e_2}{\bool}} {eq} \qquad \bininf {\tyj{\Gamma}{e_1}{\tau}} {\tyj{\Gamma}{e_2}{\tau}} {\tyj{\Gamma}{e_1 \neqc e_2}{\bool}} {neq} \] \[ \bininf {\tyj{\Gamma}{e_1}{\tau}} {\tyj{\Gamma}{e_2}{\tau}} {\tyj{\Gamma}{e_1 \ltc e_2}{\bool}} {lt} \qquad \bininf {\tyj{\Gamma}{e_1}{\tau}} {\tyj{\Gamma}{e_2}{\tau}} {\tyj{\Gamma}{e_1 \ltec e_2}{\bool}} {lte} \] \[ \bininf {\tyj{\Gamma}{e_1}{\tau}} {\tyj{\Gamma}{e_2}{\tau}} {\tyj{\Gamma}{e_1 \gtc e_2}{\bool}} {gt} \qquad \bininf {\tyj{\Gamma}{e_1}{\tau}} {\tyj{\Gamma}{e_2}{\tau}} {\tyj{\Gamma}{e_1 \gtec e_2}{\bool}} {gte} \]

There are quite a few rules here, but in essence, they all say: if \(e_1\) and \(e_2\) are some type in a given context then \(e_1 \ \square \ e_2\) is some type in the same context.

Example: \(\codel 2 \plus \codel 3\) is an \(\int\) in the empty context since \(\codel 2\) is an \(\int\) in the empty context and \(\codel 3\) is an \(\int\) in the empty context. Since \(\codel 4\) is an \(\int\) in the empty context, we also have that \(\codel 2 \plus \codel 3 \neqc \codel 4\) is a \(\bool\) in the empty context. In other words, the following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{intLit}$} \UnaryInfC{$\tyj{\emptyCtxt}{\codel 2}{\int}$} \AxiomC{} \RightLabel{$\inflab{intLit}$} \UnaryInfC{$\tyj{\emptyCtxt}{\codel 3}{\int}$} \RightLabel{$\inflab{addInt}$} \BinaryInfC{$\tyj{\emptyCtxt}{\codel 2 \plus \codel 3}{\int}$} \AxiomC{} \RightLabel{$\inflab{intLit}$} \UnaryInfC{$\tyj{\emptyCtxt}{\codel 4}{\int}$} \RightLabel{$\inflab{neq}$} \BinaryInfC{$\tyj{\emptyCtxt}{\codel 2 \plus \codel 3 \neqc \codel 4}{\bool}$} \end{prooftree}

\[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 + v_2 = v}} {\evj{e_1 \plus e_2}{v}} {addIntEval} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 v_2 = v}} {\evj{e_1 \times e_2}{v}} {mulIntEval} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 - v_2 = v}} {\evj{e_1 \minus e_2}{v}} {subIntEval} \] \[ \quainf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_2 \neq 0}} {\side{v_1 / v_2 = v}} {\evj{e_1 \divby e_2}{v}} {divIntEval} \] \[ \quainf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_2 \neq 0}} {\side{v_1 \pmod {v_2} = v}} {\evj{e_1 \modby e_2}{v}} {modIntEval} \]

\[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 + v_2 = v}} {\evj{e_1 \plusd e_2}{v}} {addFloatEval} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 v_2 = v}} {\evj{e_1 \timesd e_2}{v}} {mulFloatEval} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 - v_2 = v}} {\evj{e_1 \minusd e_2}{v}} {subFloatEval} \] \[ \quainf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_2 \neq 0}} {\side{v_1 / v_2 = v}} {\evj{e_1 \divbyd e_2}{v}} {divIntEval} \] \[ \uniinf {\evj{e_1}{\top}} {\evj{e_1 \orb e_2}{\top}} {orEvalTrue} \qquad \bininf {\evj{e_1}{\bot}} {\evj{e_2}{v}} {\evj{e_1 \orb e_2}{v}} {orEvalFalse} \] \[ \uniinf {\evj{e_1}{\bot}} {\evj{e_1 \andb e_2}{\bot}} {andEvalFalse} \qquad \bininf {\evj{e_1}{\top}} {\evj{e_2}{v}} {\evj{e_1 \andb e_2}{v}} {andEvalTrue} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 = v_2}} {\evj{e_1 \eqc e_2}{\top}} {eqEvalTrue} \quad \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 \neq v_2}} {\evj{e_1 \eqc e_2}{\bot}} {eqEvalFalse} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 \neq v_2}} {\evj{e_1 \neqc e_2}{\top}} {neqEvalTrue} \quad \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 = v_2}} {\evj{e_1 \neqc e_2}{\bot}} {neqEvalFalse} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 < v_2}} {\evj{e_1 \ltc e_2}{\top}} {ltEvalTrue} \quad \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 \geq v_2}} {\evj{e_1 \eqc e_2}{\bot}} {ltEvalFalse} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 \leq v_2}} {\evj{e_1 \ltec e_2}{\top}} {lteEvalTrue} \quad \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 \gt v_2}} {\evj{e_1 \ltec e_2}{\bot}} {lteEvalFalse} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 > v_2}} {\evj{e_1 \gtc e_2}{\top}} {gtEvalTrue} \quad \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 \leq v_2}} {\evj{e_1 \gtc e_2}{\bot}} {gtEvalFalse} \] \[ \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 \geq v_2}} {\evj{e_1 \gtec e_2}{\top}} {gteEvalTrue} \quad \triinf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\side{v_1 < v_2}} {\evj{e_1 \gtec e_2}{\bot}} {gteEvalFalse} \]

Again, there are a lot of rules here, but they all in essence say that if \(e_1\) and \(e_2\) evaluate to particular values, then \(e_1 \ \square \ e_2\) evaluates to the expected value.

One case of note is Boolean operators. Note how the rules enforce short-circuiting.

Example: \(\codel 2 \plus \codel 3\) evaluates to \(5\) and \(\codel 4\) evaluates to \(4\). So, since \(5 \neq 4\), we have that \(\codel 2 \plus \codel 3 \neqc \codel 4\) evaluates to \(\top\). In other words, the following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{intLitEval}$} \UnaryInfC{$\evj{\codel 2}{2}$} \AxiomC{} \RightLabel{$\inflab{intLitEval}$} \UnaryInfC{$\evj{\codel 3}{3}$} \RightLabel{$\inflab{intAddEval}$} \BinaryInfC{$\evj{\codel 2 \plus \codel 3}{5}$} \AxiomC{} \RightLabel{$\inflab{intLitEval}$} \UnaryInfC{$\evj{\codel 4}{4}$} \RightLabel{$\inflab{intAddEval}$} \BinaryInfC{$\evj{\codel 2 \plus \codel 3 \neqc \codel 4}{\top}$} \end{prooftree}

<expr> ::= if <expr> then <expr> else <expr>

If \(e_1\) is a well-formed expression and \(e_2\) is a well-formed expression and \(e_3\) is a well-formed expression, then \(\ite{e_1}{e_2}{e_3}\) is a well-formed expression.

Example: Since \(\codel{2}\) is a well-formed expression, then \(\ite{\codel 2}{\codel 2}{\codel 2}\) is a well-formed expression, i.e., the following is a valid parse tree.

<expr>
├──┬──────┬────┬──────┬────┐
│  <expr> │    <expr> │    <expr>
│  │      │    │      │    │
│  <int>  │    <int>  │    <int>
│  │      │    │      │    │
if 2      then 2      else 2

\[ \triinf {\tyj{\Gamma}{e_1}{\bool}} {\tyj{\Gamma}{e_2}{\tau}} {\tyj{\Gamma}{e_3}{\tau}} {\tyj{\Gamma}{\ite{e_1}{e_2}{e_3}}{\tau}} {if} \]

If \(e_1\) is of type \(\bool\) in the context \(\Gamma\) and \(e_2\) is of type \(\tau\) in the context \(\Gamma\) and \(e_3\) is also of type \(\tau\) in the context \(\Gamma\), then \(\ite{e_1}{e_2}{e_3}\) is of type \(\tau\) in the context \(\Gamma\).

Note: The type of the then-case must be the same as the type of the else-case, and the entire if-expression is of this type.

Example: Since \(\true\) is of type \(\bool\) in the empty context by the \(\mathsf{trueLit}\) rule, and \(\codel 2\) is of type \(\int\) in the empty context by the \(\mathsf{intLit}\) rule, it follows by the \(\mathsf{if}\) rule that \(\ite{\true}{\codel 2}{\codel 2}\) is of type \(\int\) in the empty context, i.e. the following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\ (\mathsf{trueLit})$} \UnaryInfC{$\tyj{\emptyCtxt}{\true}{\bool}$} \AxiomC{} \RightLabel{$\ (\mathsf{intLit})$} \UnaryInfC{$\tyj{\emptyCtxt}{\codel 2}{\int}$} \RightLabel{$\ (\mathsf{if})$} \BinaryInfC{$\tyj{\emptyCtxt}{\ite{\true}{\codel 2}{\codel 2}}{\int}$} \end{prooftree}

\[ \bininf {\evj{e_1}{\top}} {\evj{e_2}{v_2}} {\evj{\ite{e_1}{e_2}{e_3}}{v_2}} {ifEvalTrue} \qquad \bininf {\evj{e_1}{\bot}} {\evj{e_3}{v_3}} {\evj{\ite{e_1}{e_2}{e_3}}{v_3}} {ifEvalFalse} \]

If \(e_1\) evaluates to \(\true\) and \(e_2\) evaluates to \(v_2\), then \(\ite{e_1}{e_2}{e_3}\) evaluates to \(v_2\).

Example: Since \(\evj \true \top\) by the \(\mathsf{trueEval}\) rule and \(\evj{\codel 2}{2}\) by the \(\mathsf{intLitEval}\) rule then \(\evj{\ite{\true}{\codel 2}{\codel 3}}{2}\) by the \(\mathsf{ifEvalTrue}\) rule, i.e. the following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{trueEval}$} \UnaryInfC{$\evj{\true}{\top}$} \AxiomC{} \RightLabel{$\inflab{intEval}$} \UnaryInfC{$\evj{\codel 2}{2}$} \RightLabel{$\inflab{ifEval}$} \BinaryInfC{$\evj{\ite{\true}{\codel 2}{\codel 3}}{2}$} \end{prooftree}

<expr> ::= let <var> = <expr> in <expr>

If \(x\) is a variable and \(e_1\) is a well-formed expression and \(e_2\) is a well-formed expression, then \(\let{x}{e_1}{e_2}\) is a well-formed expression.

Example: Since \(\codel{var_name}\) is a well-formed variable name and \(\codel 2\) is a well-formed expression then \(\let{\codel{var_name}}{\codel 2}{\codel{var_name}}\) is a well-formed expression, i.e., the following is a valid parse tree.

<expr>
├───┬────────┬─┬──────┬──┐
│   <var>    │ <expr> │  <expr>
│   │        │ │      │  │
│   │        │ <int>  │  <var>
│   │        │ │      │  │
let var_name = 2      in var_name

\[ \bininf {\tyj{\Gamma}{e_1}{\tau_1}} {\tyj{\Gamma, x : \tau_1}{e_2}{\tau_2}} {\tyj{\Gamma}{\let{x}{e_1}{e_2}}{\tau_2}} {let} \]

If \(e_1\) is of type \(\tau_1\) in the context \(\Gamma\), and \(e_2\) is of type \(\tau_2\) in the context \(\Gamma\) with the variable declaration \((x : \tau_1)\) added to it, then \(\let{x}{e_1}{e_2}\) is of type \(\tau_2\) in the context \(\Gamma\).

Example: The following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{intLit}$} \UnaryInfC{$\tyj{\emptyCtxt}{\codel 2}{\int}$} \AxiomC{} \RightLabel{$\inflab{var}$} \UnaryInfC{$\tyj{\{\codel y : \int\}}{\codel y}{\int}$} \AxiomC{} \RightLabel{$\inflab{var}$} \UnaryInfC{$\tyj{\{\codel y : \int\}}{\codel y}{\int}$} \RightLabel{$\inflab{intAdd}$} \BinaryInfC{$\tyj{\{\codel y : \int\}}{\codel y \plus \codel y}{\int}$} \RightLabel{$\inflab{let}$} \BinaryInfC{$\tyj{\emptyCtxt}{\let{\codel y}{\codel 2}{\codel y \plus \codel y}}{\int}$} \end{prooftree}

\[ \triinf {\evj{e_1}{v_1}} {\side{\subst{v_1}{x}{e_2} = e'}} {\evj{e'}{v}} {\evj{\let{x}{e_1}{e_2}}{v}} {letEval} \]

If \(e_1\) evaluates to \(v_1\) and \(e_2\) with \(v_1\) substituted for \(x\) evaluates to \(v\), then \(\let{x}{e_1}{e_2}\) evaluates to \(v\).

Example: Since \(\evj{\codel 2}{2}\) by the \(\mathsf{intLitEval}\) rule and \(\codel y \plus \codel y\) is \(\codel 2 \plus \codel 2\) after substituting \(\codel 2\) for \(\codel y\) and \(\codel 2 \plus \codel 2\) evaluates to \(4\) by the \(\mathsf{intAddEval}\) rule, it follows that \(\let{\codel y}{\codel 2}{\codel y \plus \codel y}\) evaluates to \(4\), i.e. the following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{intLitEval}$} \UnaryInfC{$\evj{\codel 2}{2}$} \AxiomC{} \RightLabel{$\inflab{intLitEval}$} \UnaryInfC{$\evj{\codel 2}{2}$} \AxiomC{} \RightLabel{$\inflab{intLitEval}$} \UnaryInfC{$\evj{\codel 2}{2}$} \RightLabel{$\inflab{intAddEval}$} \BinaryInfC{$\evj{\codel 2 \plus \codel 2}{4}$} \RightLabel{$\inflab{letEval}$} \BinaryInfC{$\evj{\let{\codel y}{\codel 2}{\codel y \plus \codel y}}{4}$} \end{prooftree}

<expr> ::= fun <var> -> <expr>

If \(x\) is a well-formed variable and \(e\) is a well-formed expression, then \(\fun{x}{e}\) is a well-formed expression.

Example: Since \(\codel{name}\) is a valid variable name and \(\codel{name} \plus \codel{3}\) is a well-formed expression, it follows that \(\fun{\codel{name}}{\codel{name}\plus \codel{3}}\) is a well-formed expression, i.e., the following is a valid parse tree

<expr>
├───┬─────┬───┐
│   <var> │   <expr>
│   │     │   ├──────┬─┐
│   │     │   <expr> │ <expr>
│   │     │   │      │ │
│   │     │   <var>  │ <int>
│   │     │   │      │ │
fun name  ->  name   + 3

\[ \uniinf {\tyj{\Gamma, x : \tau_1}{e}{\tau_2}} {\tyj{\Gamma}{\fun{x}{e}}{\funty{\tau_1}{\tau_2}}} {fun} \]

If \(e\) is of type \(\tau_2\) in the context \(\Gamma\) together with the variable declaration \((x : \tau_1)\) added to it, then \(\fun{x}{e}\) is of type \(\funty{\tau_1}{\tau_2}\).

Example: The following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{intLit}$} \UnaryInfC{$\tyj{\{ \codel z : \float \}}{\codel 2}{\int}$} \RightLabel{$\inflab{fun}$} \UnaryInfC{$\tyj{\emptyCtxt}{\fun{\codel z}{\codel 2}}{\funty{\float}\int}$} \end{prooftree}

\[ \uniinf {} {\evj{\fun{x}{e}}{\funval x e}} {funEval} \qquad \]

A function evaluates to a function value.

Example: The following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{funEval}$} \UnaryInfC{$\evj{\fun{\codel x}{\codel x \plus \codel x}}{\funval {\codel x}{\codel x \plus \codel x}}$} \end{prooftree}

<expr> ::= <expr> <expr>

If \(e_1\) is a well-formed expression and \(e_2\) is a well-formed expression, then \(e_1 \ e_2\) is a well-formed expression.

\[ \bininf {\tyj{\Gamma}{e_1}{\funty {\tau_2} {\tau}}} {\tyj{\Gamma}{e_2}{\tau_2}} {\tyj{\Gamma}{e_1 \ e_2}{\tau}} {app} \]

If \(e_1\) is of type \(\funty {\tau_2} {\tau}\) and \(e_2\) is of type \(\tau_2\), then \(e_1 \ e_2\) is of type \(\tau\).

Example: The following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{int}$} \UnaryInfC{$\tyj{\{ \codel z : \float \}}{\codel 2}{\int}$} \RightLabel{$\inflab{fun}$} \UnaryInfC{$\tyj{\emptyCtxt}{\fun{\codel z}{\codel 2}}{\funty{\float}\int}$} \AxiomC{} \RightLabel{$\inflab{floatLit}$} \UnaryInfC{$\tyj{\emptyCtxt}{\codel{2.0}}{\float}$} \RightLabel{$\inflab{app}$} \BinaryInfC{$\tyj{\emptyCtxt}{(\fun{\codel z}{\codel 2}) \ \codel{2.0}}{\int}$} \end{prooftree}

\[ \quainf {\evj{e_1}{\funval{x}{e}}} {\evj{e_2}{v_2}} {\side{\subst{v_2}{x}{e} = e'}} {\evj{e'}{v}} {\evj{e_1 \ e_2}{v}} {appEval} \]

If \(e_1\) evaluates to the function value \(\funval x e\) and \(e_2\) evaluates to \(v_2\) and \(e\) with \(v_2\) substituted for \(x\) evaluates to \(v\), then \(e_1 \ e_2\) evaluates to \(v\).

Note: Despite the fact that we make a distinction between values and expressions, it is always possible to convert a value to an expression. We do this implictly when we substitute a value into and expression

Example: The following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{funEval}$} \UnaryInfC{$\evj{\fun{\codel x}{\codel x \plus \codel x}}{\funval {\codel x}{\codel x \plus \codel x}}$} \AxiomC{} \RightLabel{$\inflab{iLE}$} \UnaryInfC{$\evj{\codel 2}{2}$} \AxiomC{} \RightLabel{$\inflab{iLE}$} \UnaryInfC{$\evj{\codel 2}{2}$} \AxiomC{} \RightLabel{$\inflab{iLE}$} \UnaryInfC{$\evj{\codel 2}{2}$} \RightLabel{$\inflab{iAE}$} \BinaryInfC{$\evj{\codel 2 \plus \codel 2}{4}$} \RightLabel{$\inflab{app}$} \TrinaryInfC{$\evj{(\fun{\codel x}{\codel x \plus \codel x}) \ \codel 2}{4}$} \end{prooftree}

<expr> ::= <expr> , <expr>
<ty>   ::= <ty> * <ty>

If \(e_1\) is a well-formed expression and \(e_2\) is a well-formed expression, then \(e_1 \ \codel, \ e_2\) is a well-formed expression.

\[ \bininf {\tyj{\Gamma}{e_1}{\tau_1}} {\tyj{\Gamma}{e_2}{\tau_2}} {\tyj{\Gamma}{e_1 \pairc e_2}{\tau_1 \times \tau_2}} {tuple} \]

If \(e_1\) is of type \(\tau_1\) in the context \(\Gamma\) and \(e_2\) is of type \(\tau_2\) in the context \(\Gamma\), then \(e_1 \pairc e_2\) is of type \(\tau_1 \times \tau_2\) in the context \(\Gamma\).

\[ \bininf {\evj{e_1}{v_1}} {\evj{e_2}{v_2}} {\evj{e_1 \pairc e_2}{(v_1, v_2)}} {tupleEval} \]

If \(e_1\) evaluates to \(v_1\) and \(e_2\) evaluates to \(v_2\), then \(e_1 \pairc e_2\) evaluates to a tuple value \((v_1, v_2)\) (as usual, note the distinction between tuple expressions and tuple values).

<expr> ::= []
         | <expr> :: <expr>
<ty>   ::= <ty> list

\(\nil\) is a well-formed expression.

If \(e_1\) is a well-formed expression and \(e_2\) is a well-formed expression, then \(e_1 \cons e_2\) is a well-formed expression.

Example: Since \(\codel 2 \plus \codel 2\) is a well-formed expression, and \(\codel{"word"}\) is a well-formed expression, it follows that \(\codel( \codel{2} \plus \codel {2} \codel) \cons \codel{"word"} \cons \nil\) is a well-formed expression, i.e., the following is a valid parse tree

<expr>
├──────────────────────────┬──┐
<expr>                     │  <expr>
├──────┬─────────────────┐ │  ├────────┬──┐
│      <expr>            │ │  <expr>   │  <expr>
│      ├──────┬────┐     │ │  │        │  │
│      <int>  <op> <int> │ │  <string> │  │
│      │      │    │     │ │  │        │  │
(      2      +    2     ) :: "word"   :: []

\[ \uniinf {} {\tyj{\Gamma}{\nil}{\listty \tau}} {nil} \qquad \bininf {\tyj{\Gamma}{e_1}{\tau}} {\tyj{\Gamma}{e_2}{\listty \tau}} {\tyj{\Gamma}{e_1 \cons e_2}{\listty \tau}} {cons} \]

The empty list \(\nil\) of type \(\listty \tau\) in any context \(\Gamma\) (and for any type \(\tau\)).

If \(e_1\) is of type \(\tau\) in the context \(\Gamma\) and \(e_2\) is of type \(\listty \tau\) in the context \(\Gamma\), then \(e_1 \cons e_2\) is of type \(\listty \tau\) in the context \(\Gamma\).

Example: The following is a valid derivation.

\begin{prooftree} \AxiomC{} \RightLabel{$\inflab{var}$} \UnaryInfC{$\tyj{\{\codel x : \int\}}{\codel x}{\int}$} \AxiomC{} \RightLabel{$\inflab{iL}$} \UnaryInfC{$\tyj{\{\codel x : \int\}}{\codel 1}{\int}$} \RightLabel{$\inflab{iA}$} \BinaryInfC{$\tyj{\{\codel x : \int\}}{\codel x \plus \codel 1}{\int}$} \AxiomC{} \RightLabel{$\inflab{nil}$} \UnaryInfC{$\tyj{\{\codel x : \int\}}{\nil}{\listty \int}$} \RightLabel{$\inflab{cons}$} \BinaryInfC{$\tyj{\{\codel x : \int\}}{\codel( \codel x \plus \codel 1 \codel) \cons \nil}{\listty \int}$} \end{prooftree}

\[ \uniinf {} {\evj{\nil}{\nilv}} {nilEval} \qquad \bininf {\evj{e_2}{[v_2, \dots, v_k]}} {\evj{e_1}{v_1}} {\evj{e_1 \cons e_2}{[v_1, v_2, \dots, v_k]}} {consEval} \]

The empty list \(\nil\) evaluates to the empty list (as a value).

If \(e_2\) evaluates to the list value \([v_2, \dots, v_k]\) and \(e_1\) evaluates to the value \(v_1\), then \(e_1 \cons e_2\) evaluates to the list value \([v_1, v_2, \dots, v_k]\)

<expr> ::= match <expr> with ∣ <var> , <var> -> <expr>

If \(e\) and \(e'\) are a well-formed expressions and \(x\) and \(y\) are valid variable names, then \(\match e \with \case{x \pairc y}{e'}\) is a well-formed expression.

\[ \bininf {\tyj{\Gamma}{e}{\tau_1 \times \tau_2}} {\tyj{\Gamma, x : \tau_1, y : \tau_2}{e'}{\tau}} {\tyj{\Gamma}{\match e \with \case{x \pairc y}{e'}}{\tau}} {tupleMatch} \]

If \(e\) is of type \(\tau_1 \times \tau_2\) in the context \(\Gamma\) and \(e'\) is of type \(\tau\) in the context \(\Gamma\) in addition to the declarations \((x : \tau_1)\) and \((y : \tau_2)\), then \(\match e \with \case{x \pairc y}{e'}\) is of type \(\tau\).

\[ \triinf {\evj{e}{(v_1, v_2)}} {\side{\subst{v_2}{y}{\subst{v_1}{x}{e'}} = e''}} {\evj{e''}{v}} {\evj{\match e \with \case{x \pairc y}{e'}}{v}} {tupleMatchEval} \]

If \(e\) evaluates to a tuple value \((v_1, v_2)\) and \(e'\) with \(v_1\) substituted in for \(x\) and \(v_2\) substituted in for \(y\) evaluates to \(v\), then \(\match e \with \case{x \pairc y}{e'}\) evaluates to \(v\).

<expr> ::= match <expr> with
           ∣ [] -> <expr>
           ∣ <var> :: <var> -> <expr>

If \(e\), \(e_1\) and \(e_2\) are well-formed expressions and \(x\) and \(y\) are valid variable names then \(\match e \with \case{\nil}{e_1} \case{x \cons y}{e_2}\) is a well-formed expression.

\[ \triinf {\tyj{\Gamma}{e}{\listty {\tau'}}} {\tyj{\Gamma}{e_1}{\tau}} {\tyj{\Gamma, x : \tau', y : \listty {\tau'}}{e_2}{\tau}} {\tyj{\Gamma}{\match e \with \case{\nil}{e_1} \case{x \cons y}{e_2}}{\tau}} {matchList} \]

If all of the following hold:

• \(e\) is of type \(\listty {\tau'}\) in the context \(\Gamma\)
• \(e_1\) is of type \(\tau\) in the context \(\Gamma\)
• \(e_2\) is of type \(\tau\) in the context \(\Gamma\) in addition to the declarations \((x : \tau')\) and \((y : \listty {\tau'})\)

then \(\match e \with \case{\nil}{e_1} \case{x \cons y}{e_2}\) is of type \(\tau\).

\[ \bininf {\evj{e}{\nilv}} {\evj{e_1}{v}} {\evj{\match e \with \case{\nil}{e_1} \case{x \cons y}{e_2}}{v}} {matchListEvalNil} \]

\[ \triinf {\evj{e}{h \consv t}} {\side{e_2' = [t / y][h / x]e_2}} {\evj{e_2'}{v}} {\evj{\match e \with \case{\nil}{e_1} \case{x \cons y}{e_2}}{v}} {matchListEvalCons} \]

If \(e\) evaluates to the empty list \(\nilv\) and \(e_1\) evaluates to \(v\), then \(\match e \with \case{\nil}{e_1} \case{x \cons y}{e_2}\) evaluates to \(v\).

If \(e\) evaluates to the list value \(h \consv t\) and \(e_2\) with \(h\) substituted for \(x\) and \(t\) substituted for \(y\) evaluates to \(v\), then \(\match e \with \case{\nil}{e_1} \case{x \cons y}{e_2}\) evaluates to \(v\).

<expr> ::= ( <expr> )

Expressions may be surrounded in parentheses.

More to come…