Inference Rules

This page includes the inference rules that we use for typing judgments and semantic judgments. We will typically try to update it on a per-abstraction basis.

Typing judgments

A typing judgment is of the form \Gamma \vdash e : \tau, where

It reads "in the context \Gamma, the expression e has type \tau."

A context is a set of typed variables written, for example, as

\{ \texttt{x} : \texttt{int}, \texttt{y} : \texttt{string}\}

which is a context which has a variable \texttt{x} of type \texttt{int} and a variable \texttt{y} of type \texttt{string}. It's a set in the sense that a variable can appear at most once, e.g.,

\{\texttt{x} : \texttt{int}, \texttt{x} : \texttt{string}\}

is not a valid context.

Variables

This rule says that if the variable x has type \tau in \Gamma then we can derive (without premises) that x has type \tau. The requirement that x : \tau appears in \Gamma is called a side condition, and is not included in a typing derivation (you can tell side-conditions by the fact that they are premises which are not typing judgments).

\frac
{x : \tau \in \Gamma}
{\Gamma \vdash x : \tau}
\ \textsf{(Var)}

Literals

These rules say that all literals (e.g., \texttt{2}, \texttt{3.234}, \texttt{"word"}) have the appropriate type in any context without premises.

\frac
{n \text{ is an integer literal}}
{\Gamma \vdash n : \texttt{int}}
\ \textsf{(IntLit)}
\qquad
\frac
{n \text{ is an integer literal}}
{\Gamma \vdash n : \texttt{float}}
\ \textsf{(FloatLit)}
\qquad
\frac
{s \text{ is an integer literal}}
{\Gamma \vdash s : \texttt{string}}
\ \textsf{(StrLit)}

\frac{}{\Gamma \vdash \texttt{true} : \texttt{bool}}
\ \textsf{(TrueLit)}
\qquad
\frac{}{\Gamma \vdash \texttt{false} : \texttt{bool}}
\ \textsf{(FalseLit)}

Integer arithmetic

These rules express that integer operations apply only to integers and return integers.

\frac
{\Gamma \vdash e_1 : \texttt{int}
 \qquad
 \Gamma \vdash e_2 : \texttt{int}
}
{\Gamma \vdash e_1 \ \texttt{+} \ e_2 : \texttt{int}}
\ \textsf{(IntAdd)}
\qquad
\frac
{\Gamma \vdash e_1 : \texttt{int}
 \qquad
 \Gamma \vdash e_2 : \texttt{int}
}
{\Gamma \vdash e_1 \ \texttt{-} \ e_2 : \texttt{int}}
\ \textsf{(IntSub)}

\frac
{\Gamma \vdash e_1 : \texttt{int}
 \qquad
 \Gamma \vdash e_2 : \texttt{int}
}
{\Gamma \vdash e_1 \ \texttt{*} \ e_2 : \texttt{int}}
\ \textsf{(IntMul)}
\qquad
\frac
{\Gamma \vdash e_1 : \texttt{int}
 \qquad
 \Gamma \vdash e_2 : \texttt{int}
}
{\Gamma \vdash e_1 \ \texttt{/} \ e_2 : \texttt{int}}
\ \textsf{(IntDiv)}

\frac
{\Gamma \vdash e_1 : \texttt{int}
 \qquad
 \Gamma \vdash e_2 : \texttt{int}
}
{\Gamma \vdash e_1 \ \texttt{mod} \ e_2 : \texttt{int}}
\ \textsf{(IntMod)}

Floating-point arithmetic

\frac
{\Gamma \vdash e_1 : \texttt{float}
 \qquad
 \Gamma \vdash e_2 : \texttt{float}
}
{\Gamma \vdash e_1 \ \texttt{+.} \ e_2 : \texttt{float}}
\ \textsf{(FloatAdd)}
\qquad
\frac
{\Gamma \vdash e_1 : \texttt{float}
 \qquad
 \Gamma \vdash e_2 : \texttt{float}
}
{\Gamma \vdash e_1 \ \texttt{-.} \ e_2 : \texttt{float}}
\ \textsf{(FloatSub)}

\frac
{\Gamma \vdash e_1 : \texttt{float}
 \qquad
 \Gamma \vdash e_2 : \texttt{float}
}
{\Gamma \vdash e_1 \ \texttt{*.} \ e_2 : \texttt{float}}
\ \textsf{(FloatMul)}
\qquad
\frac
{\Gamma \vdash e_1 : \texttt{float}
 \qquad
 \Gamma \vdash e_2 : \texttt{float}
}
{\Gamma \vdash e_1 \ \texttt{/.} \ e_2 : \texttt{float}}
\ \textsf{(FloatDiv)}

Boolean operators

\frac
{\Gamma \vdash e_1 : \texttt{bool}
 \qquad
 \Gamma \vdash e_2 : \texttt{bool}
}
{\Gamma \vdash e_1 \ \texttt{\&\&} \ e_2 : \texttt{bool}}
\ \textsf{(And)}
\qquad
\frac
{\Gamma \vdash e_1 : \texttt{bool}
 \qquad
 \Gamma \vdash e_2 : \texttt{bool}
}
{\Gamma \vdash e_1 \ \texttt{||} \ e_2 : \texttt{bool}}
\ \textsf{(Or)}

\frac
{\Gamma \vdash e : \texttt{bool}}
{\Gamma \vdash \texttt{not} \ e : \texttt{bool}}
\ \textsf{(Not)}

Comparison operators

Note that comparison operators are polymorphic, they can be apply to any type.

\frac
{\Gamma \vdash e_1 : \tau
 \qquad
 \Gamma \vdash e_2 : \tau
}
{\Gamma \vdash e_1 \ \texttt{=} \ e_2 : \texttt{bool}}
\ \textsf{(Equal)}
\qquad
\frac
{\Gamma \vdash e_1 : \tau
 \qquad
 \Gamma \vdash e_2 : \tau
}
{\Gamma \vdash e_1 \ \texttt{<>} \ e_2 : \texttt{bool}}
\ \textsf{(NotEqual)}

\frac
{\Gamma \vdash e_1 : \tau
 \qquad
 \Gamma \vdash e_2 : \tau
}
{\Gamma \vdash e_1 \ \texttt{<} \ e_2 : \texttt{bool}}
\ \textsf{(LessThan)}
\qquad
\frac
{\Gamma \vdash e_1 : \tau
 \qquad
 \Gamma \vdash e_2 : \tau
}
{\Gamma \vdash e_1 \ \texttt{<=} \ e_2 : \texttt{bool}}
\ \textsf{(LTE)}

\frac
{\Gamma \vdash e_1 : \tau
 \qquad
 \Gamma \vdash e_2 : \tau
}
{\Gamma \vdash e_1 \ \texttt{>} \ e_2 : \texttt{bool}}
\ \textsf{(GreaterThan)}
\qquad
\frac
{\Gamma \vdash e_1 : \tau
 \qquad
 \Gamma \vdash e_2 : \tau
}
{\Gamma \vdash e_1 \ \texttt{>=} \ e_2 : \texttt{bool}}
\ \textsf{(GTE)}

Let-expressions

The left rule reads

\frac
{\Gamma \vdash e_1 : \tau
 \qquad
 \Gamma, x : \tau \vdash e_2 : \tau'
}
{\Gamma \vdash \texttt{let} \ x \ \texttt{=} \ e_1 \ \texttt{in} \ e_2 : \tau'
}
\ \textsf{(Let)}
\qquad
\frac
{\Gamma, x : \tau \vdash e_1 : \tau_1
 \qquad
 \Gamma, f : \tau \ \texttt{->} \ \tau_1 \vdash e_2 : \tau_2
}
{\Gamma \vdash \texttt{let} \ f \ x \ \texttt{=} \ e_1 \ \texttt{in} \ e_2 : \tau_2
}
\ \textsf{(LetFun)}

\frac
{\Gamma \vdash e_1 : \tau_1 \ \texttt{*} \ \tau_2 \ \texttt{*} \dots \texttt{*} \ \tau_n
 \qquad
 \Gamma, x_1 : \tau_1, x_2 : \tau_2, \dots, x_n : \tau_n \vdash e_2 : \tau'
}
{\Gamma \vdash \texttt{let (} x_1 \texttt, x_2 \texttt,\dots\texttt,x_n \texttt{) =} \ e_1 \ \texttt{in} \ e_2 : \tau'
}
\ \textsf{(LetTuple)}

Function Application

\frac
{\Gamma \vdash f : \tau \to \tau_1
 \qquad
 \Gamma \vdash e : \tau
}
{\Gamma \vdash f \ e : \tau_1}
\ \textsf{(App)}

If-expressions

\frac
{\Gamma \vdash e : \texttt{bool}
 \qquad
 \Gamma \vdash e_1 : \tau
 \qquad
 \Gamma \vdash e_2 : \tau
}
{\Gamma \vdash \texttt{if} \ e \ \texttt{then} \ e_1 \ \texttt{else} \ e_2 : \tau}
\ \textsf{(If)}

Pattern matching

\frac
{\Gamma \vdash e : \tau
 \qquad
 \Gamma \vdash p_1 : \tau
 \ \dots \
 \Gamma \vdash p_n : \tau
 \qquad
 \Gamma \vdash e_1 : \tau'
 \ \dots \
 \Gamma \vdash e_n : \tau'
}
{\Gamma \vdash \texttt{match} \ e \ \texttt{with} \ p_1 \ \texttt{->} \ e_1 \ \texttt{|} \ \dots \ \texttt{|} \ p_n \ \texttt{->} \ e_n : \tau'}
\ \textsf{(Pattern)}

Note. This rule is slightly informal because we haven't defined exactly what a pattern is. You won't be expected to write a typing derivation with this rule.

Tuples

\frac
{\Gamma \vdash e_1 : \tau_1
 \qquad
 \Gamma \vdash e_2 : \tau_2
 \qquad
 \dots
 \qquad
 \Gamma \vdash e_n : \tau_n
}
{\Gamma \vdash \texttt{(}e_1\texttt{,} e_2\texttt{,} \dots \texttt{,} e_n \texttt{)} :
\tau_1 \ \texttt{*} \ \tau_2 \ \texttt{*} \dots \texttt{*} \ \tau_n}
\ \textsf{(Tuple)}

Lists

\frac
{}
{\Gamma \vdash \texttt{[]} : \alpha \ \texttt{list}}
\ \textsf{(Nil)}
\qquad
\frac
{\Gamma \vdash e : \tau
 \qquad
 \Gamma \vdash l : \tau \ \texttt{list}
}
{\Gamma \vdash (e \ \texttt{::} \ l) : \tau \ \texttt{list}
}
\ \textsf{(Cons)}

\frac
{\Gamma \vdash e_1 : \tau
 \qquad
 \Gamma \vdash e_2 : \tau
 \qquad
 \dots
 \qquad
 \Gamma \vdash e_n : \tau
}
{\Gamma \vdash \texttt{[} e_1 \texttt{;} e_2\texttt{;}\dots\texttt;e_n\texttt{]} : \tau \ \texttt{list}}
\ \textsf{(ListLit)}

\frac
{\Gamma \vdash e : \tau \ \texttt{list}
 \qquad
 \Gamma \vdash e_1 : \tau'
 \qquad
 \Gamma, h : \tau, t : \tau \ \texttt{list} \vdash e_2 : \tau'
}
{\Gamma \vdash \left(\texttt{match} \ e \ \texttt{with [] -> } e_1 \ \texttt{|} \ h \ \texttt{::} \ t \texttt{ -> } e_2 \right) : \tau'
}
\ \textsf{(ListMatch)}

Semantic judgments

We read e \Downarrow v as "the expression e evaluates to the value v.

Variables

This rules says that a variable evaluates to itself, without any premises.

\frac
{x \text{ is a variable}}
{x \Downarrow x}
\ \textsf{(VarEval)}

Literals

This rule says that any literal evaluates to itself, without any premises.

\frac
{v \text{ is an integer/float/string/Boolean literal}}
{v \Downarrow v}
\ \textsf{(LitEval)}

Operators

We will treat all operators for now as built-in. When we evaluate an expression, we have to evaluate its operands and the apply the operator.

\frac
{e_1 \Downarrow v_1
 \qquad
 e_2 \Downarrow v_2
 \qquad
 v_1 \ \mathsf{op} \ v_2 = v
}
{e_1 \ \texttt{op} \ e_2 \Downarrow v}
\ \textsf{(OpEval)}

So for, example, these rules express that floating-point operators behave as expected. Note that in expressions we use typewriter font (e.g., \texttt{+.}) to represent an operator, whereas for values we use mathematical font (e.g., +).

\frac
{e_1 \Downarrow v_1
 \qquad
 e_2 \Downarrow v_2
 \qquad
 v_1 + v_2 = v
}
{e_1 \ \texttt{+.} \ e_2 \Downarrow v}
\ \textsf{(FloatAddEval)}
\qquad
\frac
{e_1 \Downarrow v_1
 \qquad
 e_2 \Downarrow v_2
 \qquad
 v_1 - v_2 = v
}
{e_1 \ \texttt{-.} \ e_2 \Downarrow v}
\ \textsf{(FloatSubEval)}

\frac
{e_1 \Downarrow v_1
 \qquad
 e_2 \Downarrow v_2
 \qquad
 v_1 * v_2 = v
}
{e_1 \ \texttt{*.} \ e_2 \Downarrow v}
\ \textsf{(FloatMulEval)}
\qquad
\frac
{e_1 \Downarrow v_1
 \qquad
 e_2 \Downarrow v_2
 \qquad
 v_1 / v_2 = v
}
{e_1 \ \texttt{/.} \ e_2 \Downarrow v}
\ \textsf{(FloatDivEval)}

Also note that premises like 'v_1 + v_2 = v' are not a part of a derivation, they are like the side-conditions above. For example, we would write

\frac
{\texttt{2} \Downarrow \texttt{2}
 \qquad
 \texttt{3} \Downarrow \texttt{3}
}
{\texttt{2 + 3} \Downarrow \texttt{5}}

for a particular case of the rule for adding two integers.

Let-expressions

The rule on the left reads

\frac
{e_1 \Downarrow v_1
 \qquad
 [v_1/x]e_2 \Downarrow v_2
}
{\texttt{let} \ x \ \texttt{=} \ e_1 \ \texttt{in} \ e_2 \Downarrow v_2}
\ \textsf{(LetEval)}

\frac
{e_1 \Downarrow \texttt{(} v_1\texttt{,} v_2\texttt{,} \dots \texttt{,} v_n \texttt{)}
 \qquad
 [v_1 / x_1, v_2 / x_2, \dots, v_n / x_n]e_2 \Downarrow v_2
}
{\texttt{let (} x_1 \texttt, x_2 \texttt,\dots\texttt,x_n \texttt{) =} \ e_1 \ \texttt{in} \ e_2 \Downarrow v_2
}
\ \textsf{(LetTupleEval)}

If-expressions

\frac
{e \Downarrow \texttt{true}
 \qquad
 e_1 \Downarrow v_1
}
{\texttt{if} \ e \ \texttt{then} \ e_1 \ \texttt{else} \ e_2 \Downarrow v_1}
\ \textsf{(IfTrue)}
\qquad
\frac
{e \Downarrow \texttt{false}
 \qquad
 e_2 \Downarrow v_2
}
{\texttt{if} \ e \ \texttt{then} \ e_1 \ \texttt{else} \ e_2 \Downarrow v_2}
\ \textsf{(IfFalse)}

Pattern matching

\frac
{e \Downarrow v
 \qquad
 v \text{ matches } p_i
 \qquad
 \forall j < i.(v \text{ does not match } p_j)
 \qquad
 e_i \Downarrow v_i
}
{\texttt{match} \ e \ \texttt{with} \ p_1 \ \texttt{->} \ e_1 \ \texttt{|} \ \dots \ \texttt{|} \ p_n \ \texttt{->} \ e_n \Downarrow v_i}
\ \textsf{(PatternEval)}

Note. This rule is slightly informal because we haven't defined exactly what a pattern is. You won't be expected to write a derivation of a semantic judgment with this rule.

Tuples

\frac
{e_1 \Downarrow v_1
 \qquad
 e_2 \Downarrow v_2
 \qquad
 \dots
 \qquad
 e_n \Downarrow v_n
}
{\texttt{(} e_1\texttt{,} e_2\texttt{,} \dots \texttt{,} e_n \texttt{)}
 \Downarrow
 \texttt{(} v_1\texttt{,} v_2\texttt{,} \dots \texttt{,} v_n \texttt{)}
}
\ \textsf{(TupleEval)}

Lists

\frac{}{\texttt{[]} \Downarrow \texttt{[]}}
\ \textsf{(NilEval)}
\qquad
\frac
{e \Downarrow v
 \qquad
 l \Downarrow \texttt{[} v_1 \texttt{;} v_2\texttt{;}\dots\texttt;v_n\texttt{]}
}
{e \ \texttt{::} \ l \Downarrow
 \texttt{[} v \texttt{;} v_1 \texttt{;} v_2\texttt{;}\dots\texttt;v_n\texttt{]}
}
\ \textsf{(ConsEval)}

\frac
{e \Downarrow \texttt{[]}
 \qquad
 e_1 \Downarrow v_1
}
{\left(\texttt{match} \ e \ \texttt{with [] -> } e_1 \ \texttt{|} \ h \ \texttt{::} \ t \texttt{ -> } e_2 \right)
 \Downarrow
 v_1
}
\ \textsf{(ListMatchNilEval)}

\frac
{e \Downarrow (v \ \texttt{::} \ v')
 \qquad
 [v / h][v' / t]e_2 \Downarrow v_2
}
{\left(\texttt{match} \ e \ \texttt{with [] -> } e_1 \ \texttt{|} \ h \ \texttt{::} \ t \texttt{ -> } e_2 \right)
 \Downarrow
 v_2
}
\ \textsf{(ListMatchConsEval)}

\frac
{e_1 \Downarrow v_1 \qquad e_1 \Downarrow v_2 \qquad \dots \qquad e_n \Downarrow v_n}
{\texttt{[} e_1 \texttt{;} e_2 \texttt{;}\dots\texttt;e_n\texttt{]} \Downarrow \texttt{[} v_1 \texttt{;} v_2 \texttt{;}\dots\texttt;v_n\texttt{]}}
\ \textsf{(ListLitEval)}