<p>I sometimes read articles or papers about type systems that use some funny-looking, two-dimensional notation with lots of unfamiliar symbols and Greek letters. The notation seems mathematical, but it’s entirely unlike any mathematics I learned in school. It’s quite intimidating, and I don’t even know where to start.</p>
<p>How should I read this notation? What does it mean?</p>

<types><type-systems>
How should I read type system notation?
CC BY-SA 4.0
2023-08-13T16:05:47.373Z
Related: https://stackoverflow.com/questions/12532552/what-part-of-hindley-milner-do-you-not-understand
leftaroundabout
CC BY-SA 4.0
2023-08-15T17:25:58.287Z
Nice question.  I learned a lot of this stuff in my university language design course, but that was nearly 30 years ago now so a refresher is definitely helpful :)
occipita
<p>The notation used to describe type systems varies from presentation to presentation, so giving a comprehensive overview is impossible. However, most presentations share a large, common subset, so this answer will attempt to provide a foundation of enough of the basics to understand variations on the common theme.</p>
<h1>Syntax and grammars</h1>
<p>Type systems as applied to programming language are <em>syntactic</em> systems. That is, a type system is a set of rules that operate on the (abstract) syntax of a programming language. For this reason, comprehensive treatments of type systems begin by providing the <a href="https://en.wikipedia.org/wiki/Formal_grammar" rel="noreferrer">grammar</a> of all the syntactic constructs considered by the type system using <a href="https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form" rel="noreferrer">BNF</a> notation. In the simplest typed languages, syntax is needed for precisely two things: <em>expressions</em> and <em>types</em>.</p>
<p>For example, let’s consider the grammar for an extremely simple language of booleans and integers:
<span class="math-container">$$
\begin{array}{rcll}
e \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu} \mathsf{true}\hskip{10mu}|\hskip{10mu}\mathsf{false} &amp;\textrm{boolean literal}\\
  &amp; | &amp;\hskip{-10mu} 0 \hskip{5mu}|\hskip{5mu} 1 \hskip{5mu}|\hskip{5mu} {-1} \hskip{5mu}|\hskip{5mu} 2 \hskip{5mu}|\hskip{5mu} {-2} \hskip{5mu}|\hskip{5mu} \ldots &amp;\textrm{integer literal}\\
  &amp; | &amp;\hskip{-10mu} \mathbf{if}\ e\ \mathbf{then}\ e\ \mathbf{else}\ e &amp;\textrm{conditional}\\
  &amp; | &amp;\hskip{-10mu} e + e \hskip{10mu}|\hskip{10mu} e - e \hskip{10mu}|\hskip{10mu} e × e &amp;\textrm{arithmetic}\\
  &amp; | &amp;\hskip{-10mu} e = e \hskip{10mu}|\hskip{10mu} e &lt; e \hskip{10mu}|\hskip{10mu} e &gt; e &amp;\textrm{comparison}\\[8pt]
\tau \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu} \mathsf{Bool} &amp;\textrm{booleans}\\
  &amp; | &amp;\hskip{-10mu} \mathsf{Int} &amp;\textrm{integers}
\end{array}
$$</span>
Here, <span class="math-container">$e$</span> corresponds to an expression and <span class="math-container">$\tau$</span> corresponds to a type, which is a standard notational convention. Some presentations use other symbols for types, such as <span class="math-container">$t$</span>, <span class="math-container">$T$</span>, <span class="math-container">$\sigma$</span>, or other lowercase Greek letters, but the overall structure will look roughly the same.</p>
<p>More complex languages will naturally have more complex grammars: imperative languages will include the grammar of statements, languages with pattern-matching will include the grammar of patterns, and so on. This language is so simple that it doesn’t even have variables! However, this core syntactic division between <em>terms</em> (things that have types) and <em>types</em> is essential, as defining the relationship between them is what type systems are all about.</p>
<h1>Relations, judgments, axioms, and inference rules</h1>
<p>Once the grammar has been specified, the next step is to define the <em>typing relation</em>, which is generally written <span class="math-container">$e : \tau$</span> and can be read “<span class="math-container">$e$</span> has type <span class="math-container">$\tau$</span>”. Intuitively, we understand that some statements of this form “make sense” and others do not:</p>
<ul>
<li><p><span class="math-container">$1 + 2 : \mathsf{Int}$</span> means “<span class="math-container">$1 + 2$</span> has type <span class="math-container">$\mathsf{Int}$</span>”, which certainly makes sense.</p>
</li>
<li><p><span class="math-container">$1 + 2 : \mathsf{Bool}$</span> means “<span class="math-container">$1 + 2$</span> has type <span class="math-container">$\mathsf{Bool}$</span>”, which does <em>not</em> make sense.</p>
</li>
<li><p><span class="math-container">$\mathsf{true} + 2 : \mathsf{Int}$</span> means “<span class="math-container">$\mathsf{true} + 2$</span> has type <span class="math-container">$\mathsf{Int}$</span>”, which makes even <em>less</em> sense, as the expression <span class="math-container">$\mathsf{true} + 2$</span> is nonsense and does not have any type at all.</p>
</li>
</ul>
<p>We’d like to write down some rules that precisely capture our intuitions about which statements “make sense” and which do not. To do this, we’ll define the <em>typing judgment</em>, which is written using the following notation:
<span class="math-container">$$
⊢ e : \tau
$$</span>
Here, the <span class="math-container">$⊢$</span> can be read to mean “the following statement is true”. (The <span class="math-container">$⊢$</span> might seem a bit unnecessary, and indeed it is sometimes omitted in simple systems like this one, but it will play a more significant role later.) Using this notation, we can write down the some of the <em>typing rules</em> for our type system:
<span class="math-container">$$
\begin{array}{l}\hline ⊢ \mathsf{true} : \mathsf{Bool}\end{array} \quad \quad
\begin{array}{l}\hline ⊢ \mathsf{false} : \mathsf{Bool}\end{array}
$$</span>
The horizontal bar over each of these rules with nothing on top means that they are <em>always</em> true, which makes them <em>axioms</em>. We also have an infinite number of similar axioms for integer literals:
<span class="math-container">$$
\begin{array}{l}\hline ⊢ 0 : \mathsf{Int}\end{array} \quad
\begin{array}{l}\hline ⊢ 1 : \mathsf{Int}\end{array} \quad
\begin{array}{l}\hline ⊢ -1 : \mathsf{Int}\end{array} \quad
\begin{array}{l}\hline ⊢ 2 : \mathsf{Int}\end{array} \quad \cdots
$$</span></p>
<p>Of course, the typing rules for literals are fairly boring. Things get much more interesting when we consider rules for expressions that have subexpressions! Here are the typing rules for <span class="math-container">$+$</span> and <span class="math-container">$&lt;$</span>:
<span class="math-container">$$
\begin{array}{l}
⊢ e_1 : \mathsf{Int} \\
⊢ e_2 : \mathsf{Int} \\
\hline
⊢ e_1 + e_2 : \mathsf{Int}
\end{array} \quad \quad \quad \begin{array}{l}
⊢ e_1 : \mathsf{Int} \\
⊢ e_2 : \mathsf{Int} \\
\hline
⊢ e_1 &lt; e_2 : \mathsf{Bool}
\end{array}
$$</span>
Now we have things both above <em>and</em> below the horizontal bars, which makes these <em>inference rules</em>. These represent conditional typing rules: the statement under the bar is true <strong>if</strong> all of the statements above the bar are true. For example, the first rule can be read as “if <span class="math-container">$e_1 : \mathsf{Int}$</span> and <span class="math-container">$e_2 : \mathsf{Int}$</span> are true, then <span class="math-container">$e_1 + e_2 : \mathsf{Int}$</span> is true,” which should hopefully make intuitive sense.</p>
<p>Rules for <span class="math-container">$-$</span>, <span class="math-container">$×$</span>, <span class="math-container">$=$</span>, and <span class="math-container">$&gt;$</span> are nearly identical to the ones given above, but the rule for <span class="math-container">$\mathbf{if} \ldots \mathbf{then} \ldots \mathbf{else}$</span> must be slightly more complex. This is because the branches of these expressions can be any type, as long as they agree. That is, both
<span class="math-container">$$ \mathbf{if}\ \mathsf{true}\ \mathbf{then}\ 1\ \mathbf{else}\ 2 $$</span>
and
<span class="math-container">$$ \mathbf{if}\ \mathsf{true}\ \mathbf{then}\ \mathsf{false}\ \mathbf{else}\ \mathsf{true} $$</span>
are legal, but
<span class="math-container">$$
\mathbf{if}\ \mathsf{true}\ \mathbf{then}\ 1\ \mathbf{else}\ \mathsf{true}
$$</span>
is not. To capture this, the typing rule uses a variable to stand for the type of the branches:
<span class="math-container">$$
\begin{array}{l}
⊢ e_1 : \mathsf{Bool} \\
⊢ e_2 : \tau \\
⊢ e_3 : \tau \\
\hline
⊢ \mathbf{if}\ e_1\ \mathbf{then}\ e_2\ \mathbf{else}\ e_3 : \tau
\end{array}
$$</span>
When the rule is applied, any type may be picked for <span class="math-container">$\tau$</span> as long as the choice is used consistently.</p>
<p>This notation originates in formal logic, and in particular, the style used to specify type systems most closely resembles <a href="https://en.wikipedia.org/wiki/Natural_deduction" rel="noreferrer">natural deduction</a>. Though I will not go into the formal details of the notation in this answer, rules expressed in this way can be used to construct formal proofs about the system’s properties, which is important for proving things like <a href="https://en.wikipedia.org/wiki/Type_safety" rel="noreferrer">type soundness</a>.</p>
<h2>Judgments as an algorithmic specification</h2>
<p>So far, I’ve intentionally refrained from saying anything about the computational interpretation of typing judgments. In general, judgments are just logical rules, and some type systems specified this way do not directly correspond to a decidable typechecking algorithm. However, if you are not used to thinking about proof systems, this perspective can be extremely difficult to wrap your head around.</p>
<p>Fortunately, in many cases, there <em>is</em> a way to read typing rules that directly yields a typechecking algorithm: it’s possible to interpret <span class="math-container">$⊢ e : \tau$</span> as a <em>function</em> from an expression <span class="math-container">$e$</span> to its type <span class="math-container">$\tau$</span>. This is because there is usually exactly one rule defined for each case in the grammar of expressions, which makes it possible to think of each typing rule as a distinct case in a recursive typechecking function.</p>
<p>For example, consider the rules for our little language given above. They correspond directly to an <span class="math-container">$\mathrm{infer}$</span> function with the following shape:
<span class="math-container">$$
\begin{array}{l}
\mathrm{infer} : \mathsf{Expr} → \mathsf{Type} \\
\mathrm{infer}(e) = \mathbf{match}\ e\ \mathbf{where} \\
\quad \begin{alignedat}{2}
  &amp;\mathsf{true}\ |\ \mathsf{false} &amp;&amp;↦ \mathsf{Bool} \\
  &amp;0\ |\ 1\ |\ {-1}\ |\ 2\ |\ \ldots &amp;&amp;↦ \mathsf{Int} \\
  &amp;e_1 + e_2 &amp;&amp;↦ \mathbf{assert}\: \mathrm{infer}(e_1) = \mathsf{Int}; \\
    &amp;&amp;&amp;\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e_2) = \mathsf{Int}; \\
    &amp;&amp;&amp;\phantom{{}↦{}} \mathsf{Int} \\
  &amp;e_1 &lt; e_2 &amp;&amp;↦ \mathbf{assert}\: \mathrm{infer}(e_1) = \mathsf{Int}; \\
    &amp;&amp;&amp;\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e_2) = \mathsf{Int}; \\
    &amp;&amp;&amp;\phantom{{}↦{}} \mathsf{Bool} \\
  &amp;\mathbf{if}\ e_1\ \mathbf{then}\ e_2\ \mathbf{else}\ e_3
    &amp;&amp;↦ \mathbf{assert}\: \mathrm{infer}(e_1) = \mathsf{Bool}; \\
    &amp;&amp;&amp;\phantom{{}↦{}} \mathbf{let}\: \tau = \mathrm{infer}(e_2); \\
    &amp;&amp;&amp;\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e_3) = \tau; \\
    &amp;&amp;&amp;\phantom{{}↦{}} \tau
\end{alignedat}
\end{array}
$$</span></p>
<p>Even when it isn’t possible to perform such a direct translation from typing rules to typechecking algorithm, it can be extremely helpful to consider information flow when reasoning about logical judgments. That is, for the <span class="math-container">$⊢ e : \tau$</span> judgment we defined above, <span class="math-container">$e$</span> can be considered an “input” to the judgment and <span class="math-container">$\tau$</span> considered an “output”. This strict directionality does not always apply to every rule in a type system, but it often applies to many of them, and it is a useful way to wrap your head around what the rules represent.</p>
<h1>Variables, contexts, and environments</h1>
<p>The language we’ve been using as a running example so far is exceptionally simple. One complication I’ve intentionally chosen to avoid so far is <em>variables</em>, but we need to consider them if we want to be able to write typing rules for any useful programming language. Let’s therefore expand our example language by adding functions, making it a variant of the <a href="https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus" rel="noreferrer">simply typed lambda calculus</a> (STLC). This requires the following additions to the language’s grammar:
<span class="math-container">$$
\begin{array}{rcll}
e \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu}\ldots\\
  &amp; | &amp;\hskip{-10mu} x &amp;\textrm{variable}\\
  &amp; | &amp;\hskip{-10mu} λx{:}\tau. e &amp;\textrm{function abstraction}\\
  &amp; | &amp;\hskip{-10mu} e\ e &amp;\textrm{function application}\\[8pt]
\tau \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu}\ldots\\
  &amp; | &amp;\hskip{-10mu} \tau → \tau &amp;\textrm{functions}
\end{array}
$$</span>
Here, <span class="math-container">$x$</span> stands for “some variable”. If you are unfamiliar with the lambda calculus, the notation used here might appear somewhat exotic, but it is likely not as foreign as it seems: the STLC syntax <span class="math-container">$λx{:}\tau. e$</span> corresponds directly to <code>(x:τ) =&gt; e</code> in TypeScript, and <span class="math-container">$f\ x$</span> corresponds to <code>f(x)</code>.</p>
<p>With these additions to our grammar, the notation used for our typing relation does not change—it’s still just <span class="math-container">$e : \tau$</span>—but the structure of our typing <em>judgment</em> must be extended. The trouble appears when we attempt to write a typing rule for variables:
<span class="math-container">$$
\begin{array}{l}
\hline
⊢ x : \text{???}
\end{array}
$$</span>
The problem is that the type of a variable depends on the <em>context</em> it appears in. Therefore, we need to extend the typing judgment to keep track of the types of all variables that happen to be in scope, which we do using the following notation:
<span class="math-container">$$
Γ ⊢ e : \tau
$$</span>
<span class="math-container">$Γ$</span> is called “the context” or “the type environment”, and the role of the <span class="math-container">$⊢$</span> now becomes clearer: it separates contextual assumptions from the statement to be proved. The extended judgment can therefore be pronounced “under the context <span class="math-container">$Γ$</span>, the expression <span class="math-container">$e$</span> has type <span class="math-container">$\tau$</span>”, and algorithmically, <span class="math-container">$Γ$</span> can be considered an additional “input” to the judgment of type <code>Map&lt;Variable, Type&gt;</code>. However, formally speaking, every typing rule must be defined syntactically, so contexts are explicitly represented in typing rules as syntactic constructs with the following shape:
<span class="math-container">$$
\begin{array}{rcll}
Γ \hskip{-10mu}
  &amp;::=&amp;\hskip{-10mu} \varnothing &amp;\textrm{empty context}\\
  &amp; | &amp;\hskip{-10mu} Γ, x{:}\tau &amp;\textrm{variable binding}
\end{array}
$$</span>
Sometimes <span class="math-container">$\bullet$</span> is used instead of <span class="math-container">$\varnothing$</span> to represent the empty context. Under this representation, a context is essentially an <a href="https://en.wikipedia.org/wiki/Association_list" rel="noreferrer">association list</a> mapping variable names to types.</p>
<p>Most typing rules have no reason to care about the context. Most inference rules just pass it along unaltered, and most axioms ignore it altogether. For example, here are a couple typing rules from above adapted to our new judgment:
<span class="math-container">$$
\begin{array}{l}\hline
Γ ⊢ \mathsf{true} : \mathsf{Bool}
\end{array} \quad \quad \begin{array}{l}
Γ ⊢ e_1 : \mathsf{Int} \\
Γ ⊢ e_2 : \mathsf{Int} \\
\hline
Γ ⊢ e_1 + e_2 : \mathsf{Int}
\end{array}
$$</span>
However, the context is essential for two new typing rules, which handle variable uses and lambda expressions:
<span class="math-container">$$
\begin{array}{l}
x{:}\tau \in Γ \\
\hline
Γ ⊢ x : \tau
\end{array} \quad \quad
\begin{array}{l}
Γ,x{:}\tau_1 ⊢ e : \tau_2 \\
\hline
Γ ⊢ (λx{:}\tau_1. e) : \tau_1 → \tau_2
\end{array}
$$</span>
The second of these two rules is the more complex one, as it’s where all the magic happens: while typechecking the body <span class="math-container">$e$</span> of the lambda expression, the context is extended with a new binding <span class="math-container">$x{:}\tau_1$</span>. This information is then utilized by the first rule, which says that if there is a variable binding <span class="math-container">$x$</span> with type <span class="math-container">$\tau$</span> in the current context (and therefore in scope), then <span class="math-container">$x$</span> has type <span class="math-container">$\tau$</span>. In other words, the context is used as a communication mechanism to propagate information between these two rules.</p>
<p>(Observant readers may note that this model does not handle variable shadowing. As a simplifying assumption, type systems specified this way usually assume that all variables have already been resolved and made unique.)</p>
<p>If this still seems a bit confusing to you, it may help to consider the way these additions affect our <span class="math-container">$\mathrm{infer}$</span> function from earlier:
<span class="math-container">$$
\begin{array}{l}
\mathrm{infer} : (\mathsf{Context}, \mathsf{Expr}) → \mathsf{Type} \\
\mathrm{infer}(Γ, e) = \mathbf{match}\ e\ \mathbf{where} \\
\quad \begin{alignedat}{2}
  &amp;\ldots\\
  &amp;x &amp;&amp;↦ \mathrm{lookup}(Γ, x) \\
  &amp;(λx{:}\tau_1. e') &amp;&amp;↦ \mathbf{let}\: Γ' = \mathrm{extend}(Γ, x, \tau_1); \\
    &amp;&amp;&amp;\phantom{{}↦{}} \mathbf{let}\: \tau_2 = \mathrm{infer}(Γ', e'); \\
    &amp;&amp;&amp;\phantom{{}↦{}} \mathsf{\tau_1 → \tau_2}
\end{alignedat}
\end{array}
$$</span></p>
<p>The only remaining rule we need to add to cope with the addition of functions is a rule for function application:
<span class="math-container">$$
\begin{array}{l}
Γ ⊢ e_1 : \tau_1 → \tau_2 \\
Γ ⊢ e_2 : \tau_1 \\
\hline
Γ ⊢ e_1\ e_2 : \tau_2
\end{array}
$$</span>
That’s it!</p>
<h1>Other common notation and considerations</h1>
<p>The above describes the large majority of notation used to specify type systems if measured by volume, but modifications and extensions to this foundation are extremely common. It would be impossible to cover all of them, but fortunately, good papers usually explain whatever nonstandard notation they choose to introduce. However, some conventions are common enough that they are often used without explanation; this section attempts to provide a basic survey and describe a few notational quirks.</p>
<p>Since this is not and can never be an exhaustive list, please open a separate question if you find some notation not covered here!</p>
<h2>Inference rule layout</h2>
<p>So far, all of the examples in this answer have laid out inference rules in a very regular, vertical way. However, placing each condition on its own line is not by any means required, so several conditions may appear side-by-side:
<span class="math-container">$$
\begin{array}{c}
Γ ⊢ e_1 : \mathsf{Int} \hskip{25mu}
Γ ⊢ e_2 : \mathsf{Int} \\
\hline
Γ ⊢ e_1 + e_2 : \mathsf{Int}
\end{array}
$$</span>
Vertical and horizontal arrangement may even be combined within the same rule.</p>
<h2>Side conditions</h2>
<p>Usually, the conditions that appear above the horizontal bar in an inference rule are themselves judgments that must be satisfied by some combination of inference rules and axioms. However, this is not always the case: rules may also include arbitrary boolean expressions known as <em>side conditions</em>, which must all be true in order for the rule to be applied. The <span class="math-container">$x{:}\tau \in Γ$</span> condition in our typing rule for variables is an example of a side condition.</p>
<p>A special type of side condition that sometimes appears in algorithmic type systems is written <span class="math-container">$\alpha\ \mathbf{fresh}$</span>. This means that <span class="math-container">$\alpha$</span> should be a fresh type variable, i.e. a type variable distinct from all other type variables.</p>
<h2>Subtyping</h2>
<p>Subtyping introduces a weaker notion of consistency between types than strict equality, and the subtyping relation must be explicitly defined. It is usually denoted <span class="math-container">$\tau_1 &lt;: \tau_2$</span>, which can be read as “<span class="math-container">$\tau_1$</span> is a subtype of <span class="math-container">$\tau_2$</span>”.</p>
<p>The relation is often defined using the same syntax used to define judgments. For example, a very simple subtyping relation might introduce two special types, <span class="math-container">$\top$</span> (pronounced “top”) and <span class="math-container">$\bot$</span> (pronounced “bottom”), which are the supertype and subtype of all types, respectively. This relation can be expressed using three simple axioms:
<span class="math-container">$$
\begin{array}{l}\hline \tau &lt;: \tau \end{array} \quad \quad
\begin{array}{l}\hline \tau &lt;: \top \end{array} \quad \quad
\begin{array}{l}\hline \bot &lt;: \tau \end{array}
$$</span>
The first rule is the reflexive rule, often abbreviated to “refl”, which states that every type is a subtype of itself and ensures that subtyping is strictly weaker than equality.</p>
<p>The defined subtyping relation must then be used explicitly in every rule that permits subtyping. For example, a system that supports subtyping might use the following rule for function application:
<span class="math-container">$$
\begin{array}{l}
Γ ⊢ e_1 : \tau_2 → \tau_3 \\
Γ ⊢ e_2 : \tau_1 \\
\tau_1 &lt;: \tau_2 \\
\hline
Γ ⊢ e_1\ e_2 : \tau_3
\end{array}
$$</span></p>
<h2>Multiple contexts</h2>
<p>Some type systems define typing judgments involving more than one context. The second context is usually named <span class="math-container">$Δ$</span>. Common notations for multi-context rules are <span class="math-container">$Γ;Δ ⊢ e : \tau$</span> (used when both contexts are morally “inputs”) and <span class="math-container">$Γ ⊢ e : \tau ⊣ Δ$</span> (used when <span class="math-container">$Δ$</span> is morally an “output”).</p>
<p>The second context may be used for any number of different things. Perhaps certain variables can be referenced from inside certain expressions but not others, or perhaps an output context is used to keep track of which variables are “consumed” in a resource-aware programming language.</p>
<h2>Bidirectional typechecking</h2>
<p><a href="https://arxiv.org/abs/1908.05839" rel="noreferrer">Bidirectional typechecking</a> is an approach for performing a limited form of nonlocal type inference without the need to use a constraint solver. A bidirectional system splits the usual <span class="math-container">$Γ ⊢ e : \tau$</span> typing judgment into two specialized judgments:</p>
<ul>
<li><p><span class="math-container">$Γ ⊢ e ⇐ \tau$</span> is the <em>checking</em> judgment, which checks that <span class="math-container">$e$</span> has some expected type <span class="math-container">$\tau$</span>. Algorithmically, <span class="math-container">$\tau$</span> is an <em>input</em> to this judgment.</p>
</li>
<li><p><span class="math-container">$Γ ⊢ e ⇒ \tau$</span> is the <em>inference</em> judgment, which is used whenever expected type information is not available. Algorithmically, <span class="math-container">$\tau$</span> is an <em>output</em> from this judgment.</p>
</li>
</ul>
<p>The two judgments are defined in a mutually-recursive way to propagate type information bidirectionally, which allows some type annotations to sometimes be omitted. For example, the checking variant of the rule for lambda abstraction may omit the annotation on the variable binder since it can be determined from the expected type:
<span class="math-container">$$
\begin{array}{c}
Γ,x{:}\tau_1 ⊢ e ⇐ \tau_2 \\
\hline
Γ ⊢ (λx. e) ⇐ \tau_1 → \tau_2
\end{array}
$$</span></p>

CC BY-SA 4.0
2023-08-13T02:18:06.827Z
2023-08-14T21:34:58.543Z
2023-08-14T21:34:58.543Z
Alexis King
CC BY-SA 4.0
2023-08-18T16:06:48.563Z
What is this symbol, `⊣`, and its usage as seen in `Γ⊢e:τ⊣Δ` ?
Erik Eidt
CC BY-SA 4.0
2023-08-20T16:01:13.860Z
@ErikEidt It is nothing more than $⊢$ flipped to point the other way (called `\dashv` in LaTeX). I don’t believe it has any particular meaning in formal logic, at least not in the way $⊢$ does; it’s just syntax.
Alexis King
CC BY-SA 4.0
2024-06-27T01:18:46.383Z
It is an odd quirk of the notation that in `e ::= e + e`, each occurance of `e` can be a different expression, but in the typing judgment for `if` expressions, each occurance of τ must correspond to the same type....
Brian Goetz
CC BY-SA 4.0
2024-06-27T16:36:30.990Z
@BrianGoetz In a grammar, it would be sort of annoying to write subscripts for each occurrence since you almost never want to require that two subterms are the same. On the other hand, in an inference rule it's fairly common that you want two things to be the same.
David Young
CC BY-SA 4.0
2024-06-27T21:08:35.153Z
@DavidYoung Oh, I get it.  I just found it notable that I've intuitively understood this inconsistency for many years but never consciously noticed it before.  But I can imagine others being confused by this, since it is not explicitly written down (nor is very much written down about CSM at all, as Guy reminds us all.)
Brian Goetz
CC BY-SA 4.0
2023-08-14T09:25:02.177Z
What does the weighty tome [Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/tapl/) add beyond this that justifies its weight?
Bruce Adams
CC BY-SA 4.0
2023-08-14T10:50:00.320Z
@BruceAdams Using this notation, TAPL (a) motivates and presents a bunch of type systems (b) define how to check they're sensible (type safety) (c) *proves* those type systems are type-safe (d) presents core implementations of those type systems. Researchers only learned how to do those proofs around 1992; it's pretty cool we got a textbook popularizing those techniques in just around ten years.
Blaisorblade
CC BY-SA 4.0
2023-08-14T15:37:45.827Z
To me, the barrier to entry when coming from mathematics is showcased well by the fact that the `::=` symbol is BNF-specific and isn't explained, even in this fantastic answer, nor even in the wikipedia link about BNF.  It's clearly a [common question](https://stackoverflow.com/questions/9196066/what-does-a-double-colon-followed-by-an-equals-sign-mean-in-programming-do) that people have upon first exposure to BNF
Indigenuity
CC BY-SA 4.0
2023-08-14T21:30:58.770Z
@Indigenuity I think it could be valuable to have a separate question at some point that covers BNF grammars at the same level of detail that this answer does with type system notation. But I intentionally chose not to go into that detail here, as BNF grammars are very common in programming (not just in computer science; they appear in most RFCs), and this answer is long enough already. A question, though: you say “when coming **from** mathematics”; do you mean you have a mathematical background but *not* a programming background?
Alexis King
CC BY-SA 4.0
2023-08-15T12:37:39.200Z
Guy Steele gave a great talk about this topic a few years back https://www.youtube.com/watch?v=dCuZkaaou0Q&t=2s
Jared Smith
CC BY-SA 4.0
2023-08-15T17:32:21.380Z
Suggestion: it might be useful to add guidance on how to pronounce unfamiliar symbols.  There are a few that I've never been entirely sure of, e.g. what's the name of the '⊢' symbol?  And I know 'Γ' is a greek capital letter, but I can't remember which...
occipita
CC BY-SA 4.0
2023-08-15T21:39:25.457Z
This was an excellent intro! I also noticed what @Indigenuity brought up about how the context is defined though. Also I think it would maybe be helpful to include an example of how something like 'let' works for introducing new variables (I know there is a let on the RHS in the function case for infer, but I mean how let would work in the lang we are trying to type).
Joseph Garvin
CC BY-SA 4.0
2023-08-16T00:46:33.060Z
@occipita Yeah, I agree, knowing how to pronounce symbols always helps me! “⊢” can be read as “entails”. “Γ” is the typing context (ie. Gamma - no idea why this letter is used). “∈” can be read as “element of”.
brendanzab
# How should I read type system notation?
Posted by: username_0 on 2023-08-13
I sometimes read articles or papers about type systems that use some funny-looking, two-dimensional notation with lots of unfamiliar symbols and Greek letters. The notation seems mathematical, but it’s entirely unlike any mathematics I learned in school. It’s quite intimidating, and I don’t even know where to start.

How should I read this notation? What does it mean?
**Tags:** types type-systems
> **Comments:**
> **username_1**: Related: https://stackoverflow.com/questions/12532552/what-part-of-hindley-milner-do-you-not-understand  
> **username_2**: Nice question.  I learned a lot of this stuff in my university language design course, but that was nearly 30 years ago now so a refresher is definitely helpful :)  
---
## 1 answers
### Answer by username_0 on 2023-08-13. Score: 176
The notation used to describe type systems varies from presentation to presentation, so giving a comprehensive overview is impossible. However, most presentations share a large, common subset, so this answer will attempt to provide a foundation of enough of the basics to understand variations on the common theme.

# Syntax and grammars

Type systems as applied to programming language are *syntactic* systems. That is, a type system is a set of rules that operate on the (abstract) syntax of a programming language. For this reason, comprehensive treatments of type systems begin by providing the [grammar](https://en.wikipedia.org/wiki/Formal_grammar) of all the syntactic constructs considered by the type system using [BNF](https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form) notation. In the simplest typed languages, syntax is needed for precisely two things: *expressions* and *types*.

For example, let’s consider the grammar for an extremely simple language of booleans and integers:
$$
\begin{array}{rcll}
e \hskip{-10mu}
&::=&\hskip{-10mu} \mathsf{true}\hskip{10mu}|\hskip{10mu}\mathsf{false} &\textrm{boolean literal}\\
& | &\hskip{-10mu} 0 \hskip{5mu}|\hskip{5mu} 1 \hskip{5mu}|\hskip{5mu} {-1} \hskip{5mu}|\hskip{5mu} 2 \hskip{5mu}|\hskip{5mu} {-2} \hskip{5mu}|\hskip{5mu} \ldots &\textrm{integer literal}\\
& | &\hskip{-10mu} \mathbf{if}\ e\ \mathbf{then}\ e\ \mathbf{else}\ e &\textrm{conditional}\\
& | &\hskip{-10mu} e + e \hskip{10mu}|\hskip{10mu} e - e \hskip{10mu}|\hskip{10mu} e × e &\textrm{arithmetic}\\
& | &\hskip{-10mu} e = e \hskip{10mu}|\hskip{10mu} e < e \hskip{10mu}|\hskip{10mu} e > e &\textrm{comparison}\\[8pt]
\tau \hskip{-10mu}
&::=&\hskip{-10mu} \mathsf{Bool} &\textrm{booleans}\\
& | &\hskip{-10mu} \mathsf{Int} &\textrm{integers}
\end{array}
$$
Here, $e$ corresponds to an expression and $\tau$ corresponds to a type, which is a standard notational convention. Some presentations use other symbols for types, such as $t$, $T$, $\sigma$, or other lowercase Greek letters, but the overall structure will look roughly the same.

More complex languages will naturally have more complex grammars: imperative languages will include the grammar of statements, languages with pattern-matching will include the grammar of patterns, and so on. This language is so simple that it doesn’t even have variables! However, this core syntactic division between *terms* (things that have types) and *types* is essential, as defining the relationship between them is what type systems are all about.

# Relations, judgments, axioms, and inference rules

Once the grammar has been specified, the next step is to define the *typing relation*, which is generally written $e : \tau$ and can be read “$e$ has type $\tau$”. Intuitively, we understand that some statements of this form “make sense” and others do not:

* $1 + 2 : \mathsf{Int}$ means “$1 + 2$ has type $\mathsf{Int}$”, which certainly makes sense.
* $1 + 2 : \mathsf{Bool}$ means “$1 + 2$ has type $\mathsf{Bool}$”, which does *not* make sense.
* $\mathsf{true} + 2 : \mathsf{Int}$ means “$\mathsf{true} + 2$ has type $\mathsf{Int}$”, which makes even *less* sense, as the expression $\mathsf{true} + 2$ is nonsense and does not have any type at all.

We’d like to write down some rules that precisely capture our intuitions about which statements “make sense” and which do not. To do this, we’ll define the *typing judgment*, which is written using the following notation:
$$
⊢ e : \tau
$$
Here, the $⊢$ can be read to mean “the following statement is true”. (The $⊢$ might seem a bit unnecessary, and indeed it is sometimes omitted in simple systems like this one, but it will play a more significant role later.) Using this notation, we can write down the some of the *typing rules* for our type system:
$$
\begin{array}{l}\hline ⊢ \mathsf{true} : \mathsf{Bool}\end{array} \quad \quad
\begin{array}{l}\hline ⊢ \mathsf{false} : \mathsf{Bool}\end{array}
$$
The horizontal bar over each of these rules with nothing on top means that they are *always* true, which makes them *axioms*. We also have an infinite number of similar axioms for integer literals:
$$
\begin{array}{l}\hline ⊢ 0 : \mathsf{Int}\end{array} \quad
\begin{array}{l}\hline ⊢ 1 : \mathsf{Int}\end{array} \quad
\begin{array}{l}\hline ⊢ -1 : \mathsf{Int}\end{array} \quad
\begin{array}{l}\hline ⊢ 2 : \mathsf{Int}\end{array} \quad \cdots
$$

Of course, the typing rules for literals are fairly boring. Things get much more interesting when we consider rules for expressions that have subexpressions! Here are the typing rules for $+$ and $<$:
$$
\begin{array}{l}
⊢ e\_1 : \mathsf{Int} \\
⊢ e\_2 : \mathsf{Int} \\
\hline
⊢ e\_1 + e\_2 : \mathsf{Int}
\end{array} \quad \quad \quad \begin{array}{l}
⊢ e\_1 : \mathsf{Int} \\
⊢ e\_2 : \mathsf{Int} \\
\hline
⊢ e\_1 < e\_2 : \mathsf{Bool}
\end{array}
$$
Now we have things both above *and* below the horizontal bars, which makes these *inference rules*. These represent conditional typing rules: the statement under the bar is true **if** all of the statements above the bar are true. For example, the first rule can be read as “if $e\_1 : \mathsf{Int}$ and $e\_2 : \mathsf{Int}$ are true, then $e\_1 + e\_2 : \mathsf{Int}$ is true,” which should hopefully make intuitive sense.

Rules for $-$, $×$, $=$, and $>$ are nearly identical to the ones given above, but the rule for $\mathbf{if} \ldots \mathbf{then} \ldots \mathbf{else}$ must be slightly more complex. This is because the branches of these expressions can be any type, as long as they agree. That is, both
$$ \mathbf{if}\ \mathsf{true}\ \mathbf{then}\ 1\ \mathbf{else}\ 2 $$
and
$$ \mathbf{if}\ \mathsf{true}\ \mathbf{then}\ \mathsf{false}\ \mathbf{else}\ \mathsf{true} $$
are legal, but
$$
\mathbf{if}\ \mathsf{true}\ \mathbf{then}\ 1\ \mathbf{else}\ \mathsf{true}
$$
is not. To capture this, the typing rule uses a variable to stand for the type of the branches:
$$
\begin{array}{l}
⊢ e\_1 : \mathsf{Bool} \\
⊢ e\_2 : \tau \\
⊢ e\_3 : \tau \\
\hline
⊢ \mathbf{if}\ e\_1\ \mathbf{then}\ e\_2\ \mathbf{else}\ e\_3 : \tau
\end{array}
$$
When the rule is applied, any type may be picked for $\tau$ as long as the choice is used consistently.

This notation originates in formal logic, and in particular, the style used to specify type systems most closely resembles [natural deduction](https://en.wikipedia.org/wiki/Natural_deduction). Though I will not go into the formal details of the notation in this answer, rules expressed in this way can be used to construct formal proofs about the system’s properties, which is important for proving things like [type soundness](https://en.wikipedia.org/wiki/Type_safety).

## Judgments as an algorithmic specification

So far, I’ve intentionally refrained from saying anything about the computational interpretation of typing judgments. In general, judgments are just logical rules, and some type systems specified this way do not directly correspond to a decidable typechecking algorithm. However, if you are not used to thinking about proof systems, this perspective can be extremely difficult to wrap your head around.

Fortunately, in many cases, there *is* a way to read typing rules that directly yields a typechecking algorithm: it’s possible to interpret $⊢ e : \tau$ as a *function* from an expression $e$ to its type $\tau$. This is because there is usually exactly one rule defined for each case in the grammar of expressions, which makes it possible to think of each typing rule as a distinct case in a recursive typechecking function.

For example, consider the rules for our little language given above. They correspond directly to an $\mathrm{infer}$ function with the following shape:
$$
\begin{array}{l}
\mathrm{infer} : \mathsf{Expr} → \mathsf{Type} \\
\mathrm{infer}(e) = \mathbf{match}\ e\ \mathbf{where} \\
\quad \begin{alignedat}{2}
&\mathsf{true}\ |\ \mathsf{false} &&↦ \mathsf{Bool} \\
&0\ |\ 1\ |\ {-1}\ |\ 2\ |\ \ldots &&↦ \mathsf{Int} \\
&e\_1 + e\_2 &&↦ \mathbf{assert}\: \mathrm{infer}(e\_1) = \mathsf{Int}; \\
&&&\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e\_2) = \mathsf{Int}; \\
&&&\phantom{{}↦{}} \mathsf{Int} \\
&e\_1 < e\_2 &&↦ \mathbf{assert}\: \mathrm{infer}(e\_1) = \mathsf{Int}; \\
&&&\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e\_2) = \mathsf{Int}; \\
&&&\phantom{{}↦{}} \mathsf{Bool} \\
&\mathbf{if}\ e\_1\ \mathbf{then}\ e\_2\ \mathbf{else}\ e\_3
&&↦ \mathbf{assert}\: \mathrm{infer}(e\_1) = \mathsf{Bool}; \\
&&&\phantom{{}↦{}} \mathbf{let}\: \tau = \mathrm{infer}(e\_2); \\
&&&\phantom{{}↦{}} \mathbf{assert}\: \mathrm{infer}(e\_3) = \tau; \\
&&&\phantom{{}↦{}} \tau
\end{alignedat}
\end{array}
$$

Even when it isn’t possible to perform such a direct translation from typing rules to typechecking algorithm, it can be extremely helpful to consider information flow when reasoning about logical judgments. That is, for the $⊢ e : \tau$ judgment we defined above, $e$ can be considered an “input” to the judgment and $\tau$ considered an “output”. This strict directionality does not always apply to every rule in a type system, but it often applies to many of them, and it is a useful way to wrap your head around what the rules represent.

# Variables, contexts, and environments

The language we’ve been using as a running example so far is exceptionally simple. One complication I’ve intentionally chosen to avoid so far is *variables*, but we need to consider them if we want to be able to write typing rules for any useful programming language. Let’s therefore expand our example language by adding functions, making it a variant of the [simply typed lambda calculus](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus) (STLC). This requires the following additions to the language’s grammar:
$$
\begin{array}{rcll}
e \hskip{-10mu}
&::=&\hskip{-10mu}\ldots\\
& | &\hskip{-10mu} x &\textrm{variable}\\
& | &\hskip{-10mu} λx{:}\tau. e &\textrm{function abstraction}\\
& | &\hskip{-10mu} e\ e &\textrm{function application}\\[8pt]
\tau \hskip{-10mu}
&::=&\hskip{-10mu}\ldots\\
& | &\hskip{-10mu} \tau → \tau &\textrm{functions}
\end{array}
$$
Here, $x$ stands for “some variable”. If you are unfamiliar with the lambda calculus, the notation used here might appear somewhat exotic, but it is likely not as foreign as it seems: the STLC syntax $λx{:}\tau. e$ corresponds directly to `(x:τ) => e` in TypeScript, and $f\ x$ corresponds to `f(x)`.

With these additions to our grammar, the notation used for our typing relation does not change—it’s still just $e : \tau$—but the structure of our typing *judgment* must be extended. The trouble appears when we attempt to write a typing rule for variables:
$$
\begin{array}{l}
\hline
⊢ x : \text{???}
\end{array}
$$
The problem is that the type of a variable depends on the *context* it appears in. Therefore, we need to extend the typing judgment to keep track of the types of all variables that happen to be in scope, which we do using the following notation:
$$
Γ ⊢ e : \tau
$$
$Γ$ is called “the context” or “the type environment”, and the role of the $⊢$ now becomes clearer: it separates contextual assumptions from the statement to be proved. The extended judgment can therefore be pronounced “under the context $Γ$, the expression $e$ has type $\tau$”, and algorithmically, $Γ$ can be considered an additional “input” to the judgment of type `Map`. However, formally speaking, every typing rule must be defined syntactically, so contexts are explicitly represented in typing rules as syntactic constructs with the following shape:
$$
\begin{array}{rcll}
Γ \hskip{-10mu}
&::=&\hskip{-10mu} \varnothing &\textrm{empty context}\\
& | &\hskip{-10mu} Γ, x{:}\tau &\textrm{variable binding}
\end{array}
$$
Sometimes $\bullet$ is used instead of $\varnothing$ to represent the empty context. Under this representation, a context is essentially an [association list](https://en.wikipedia.org/wiki/Association_list) mapping variable names to types.

Most typing rules have no reason to care about the context. Most inference rules just pass it along unaltered, and most axioms ignore it altogether. For example, here are a couple typing rules from above adapted to our new judgment:
$$
\begin{array}{l}\hline
Γ ⊢ \mathsf{true} : \mathsf{Bool}
\end{array} \quad \quad \begin{array}{l}
Γ ⊢ e\_1 : \mathsf{Int} \\
Γ ⊢ e\_2 : \mathsf{Int} \\
\hline
Γ ⊢ e\_1 + e\_2 : \mathsf{Int}
\end{array}
$$
However, the context is essential for two new typing rules, which handle variable uses and lambda expressions:
$$
\begin{array}{l}
x{:}\tau \in Γ \\
\hline
Γ ⊢ x : \tau
\end{array} \quad \quad
\begin{array}{l}
Γ,x{:}\tau\_1 ⊢ e : \tau\_2 \\
\hline
Γ ⊢ (λx{:}\tau\_1. e) : \tau\_1 → \tau\_2
\end{array}
$$
The second of these two rules is the more complex one, as it’s where all the magic happens: while typechecking the body $e$ of the lambda expression, the context is extended with a new binding $x{:}\tau\_1$. This information is then utilized by the first rule, which says that if there is a variable binding $x$ with type $\tau$ in the current context (and therefore in scope), then $x$ has type $\tau$. In other words, the context is used as a communication mechanism to propagate information between these two rules.

(Observant readers may note that this model does not handle variable shadowing. As a simplifying assumption, type systems specified this way usually assume that all variables have already been resolved and made unique.)

If this still seems a bit confusing to you, it may help to consider the way these additions affect our $\mathrm{infer}$ function from earlier:
$$
\begin{array}{l}
\mathrm{infer} : (\mathsf{Context}, \mathsf{Expr}) → \mathsf{Type} \\
\mathrm{infer}(Γ, e) = \mathbf{match}\ e\ \mathbf{where} \\
\quad \begin{alignedat}{2}
&\ldots\\
&x &&↦ \mathrm{lookup}(Γ, x) \\
&(λx{:}\tau\_1. e') &&↦ \mathbf{let}\: Γ' = \mathrm{extend}(Γ, x, \tau\_1); \\
&&&\phantom{{}↦{}} \mathbf{let}\: \tau\_2 = \mathrm{infer}(Γ', e'); \\
&&&\phantom{{}↦{}} \mathsf{\tau\_1 → \tau\_2}
\end{alignedat}
\end{array}
$$

The only remaining rule we need to add to cope with the addition of functions is a rule for function application:
$$
\begin{array}{l}
Γ ⊢ e\_1 : \tau\_1 → \tau\_2 \\
Γ ⊢ e\_2 : \tau\_1 \\
\hline
Γ ⊢ e\_1\ e\_2 : \tau\_2
\end{array}
$$
That’s it!

# Other common notation and considerations

The above describes the large majority of notation used to specify type systems if measured by volume, but modifications and extensions to this foundation are extremely common. It would be impossible to cover all of them, but fortunately, good papers usually explain whatever nonstandard notation they choose to introduce. However, some conventions are common enough that they are often used without explanation; this section attempts to provide a basic survey and describe a few notational quirks.

Since this is not and can never be an exhaustive list, please open a separate question if you find some notation not covered here!

## Inference rule layout

So far, all of the examples in this answer have laid out inference rules in a very regular, vertical way. However, placing each condition on its own line is not by any means required, so several conditions may appear side-by-side:
$$
\begin{array}{c}
Γ ⊢ e\_1 : \mathsf{Int} \hskip{25mu}
Γ ⊢ e\_2 : \mathsf{Int} \\
\hline
Γ ⊢ e\_1 + e\_2 : \mathsf{Int}
\end{array}
$$
Vertical and horizontal arrangement may even be combined within the same rule.

## Side conditions

Usually, the conditions that appear above the horizontal bar in an inference rule are themselves judgments that must be satisfied by some combination of inference rules and axioms. However, this is not always the case: rules may also include arbitrary boolean expressions known as *side conditions*, which must all be true in order for the rule to be applied. The $x{:}\tau \in Γ$ condition in our typing rule for variables is an example of a side condition.

A special type of side condition that sometimes appears in algorithmic type systems is written $\alpha\ \mathbf{fresh}$. This means that $\alpha$ should be a fresh type variable, i.e. a type variable distinct from all other type variables.

## Subtyping

Subtyping introduces a weaker notion of consistency between types than strict equality, and the subtyping relation must be explicitly defined. It is usually denoted $\tau\_1 <: \tau\_2$, which can be read as “$\tau\_1$ is a subtype of $\tau\_2$”.

The relation is often defined using the same syntax used to define judgments. For example, a very simple subtyping relation might introduce two special types, $\top$ (pronounced “top”) and $\bot$ (pronounced “bottom”), which are the supertype and subtype of all types, respectively. This relation can be expressed using three simple axioms:
$$
\begin{array}{l}\hline \tau <: \tau \end{array} \quad \quad
\begin{array}{l}\hline \tau <: \top \end{array} \quad \quad
\begin{array}{l}\hline \bot <: \tau \end{array}
$$
The first rule is the reflexive rule, often abbreviated to “refl”, which states that every type is a subtype of itself and ensures that subtyping is strictly weaker than equality.

The defined subtyping relation must then be used explicitly in every rule that permits subtyping. For example, a system that supports subtyping might use the following rule for function application:
$$
\begin{array}{l}
Γ ⊢ e\_1 : \tau\_2 → \tau\_3 \\
Γ ⊢ e\_2 : \tau\_1 \\
\tau\_1 <: \tau\_2 \\
\hline
Γ ⊢ e\_1\ e\_2 : \tau\_3
\end{array}
$$

## Multiple contexts

Some type systems define typing judgments involving more than one context. The second context is usually named $Δ$. Common notations for multi-context rules are $Γ;Δ ⊢ e : \tau$ (used when both contexts are morally “inputs”) and $Γ ⊢ e : \tau ⊣ Δ$ (used when $Δ$ is morally an “output”).

The second context may be used for any number of different things. Perhaps certain variables can be referenced from inside certain expressions but not others, or perhaps an output context is used to keep track of which variables are “consumed” in a resource-aware programming language.

## Bidirectional typechecking

[Bidirectional typechecking](https://arxiv.org/abs/1908.05839) is an approach for performing a limited form of nonlocal type inference without the need to use a constraint solver. A bidirectional system splits the usual $Γ ⊢ e : \tau$ typing judgment into two specialized judgments:

* $Γ ⊢ e ⇐ \tau$ is the *checking* judgment, which checks that $e$ has some expected type $\tau$. Algorithmically, $\tau$ is an *input* to this judgment.
* $Γ ⊢ e ⇒ \tau$ is the *inference* judgment, which is used whenever expected type information is not available. Algorithmically, $\tau$ is an *output* from this judgment.

The two judgments are defined in a mutually-recursive way to propagate type information bidirectionally, which allows some type annotations to sometimes be omitted. For example, the checking variant of the rule for lambda abstraction may omit the annotation on the variable binder since it can be determined from the expected type:
$$
\begin{array}{c}
Γ,x{:}\tau\_1 ⊢ e ⇐ \tau\_2 \\
\hline
Γ ⊢ (λx. e) ⇐ \tau\_1 → \tau\_2
\end{array}
$$
> **Comments:**
> **username_6** (2023-08-14): What does the weighty tome [Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/tapl/) add beyond this that justifies its weight?  
> **username_7** (2023-08-14): @BruceAdams Using this notation, TAPL (a) motivates and presents a bunch of type systems (b) define how to check they're sensible (type safety) (c) *proves* those type systems are type-safe (d) presents core implementations of those type systems. Researchers only learned how to do those proofs around 1992; it's pretty cool we got a textbook popularizing those techniques in just around ten years.  
> **username_8** (2023-08-14): To me, the barrier to entry when coming from mathematics is showcased well by the fact that the `::=` symbol is BNF-specific and isn't explained, even in this fantastic answer, nor even in the wikipedia link about BNF.  It's clearly a [common question](https://stackoverflow.com/questions/9196066/what-does-a-double-colon-followed-by-an-equals-sign-mean-in-programming-do) that people have upon first exposure to BNF  
> **username_0** (2023-08-14): @Indigenuity I think it could be valuable to have a separate question at some point that covers BNF grammars at the same level of detail that this answer does with type system notation. But I intentionally chose not to go into that detail here, as BNF grammars are very common in programming (not just in computer science; they appear in most RFCs), and this answer is long enough already. A question, though: you say “when coming **from** mathematics”; do you mean you have a mathematical background but *not* a programming background?  
> **username_9** (2023-08-15): Guy Steele gave a great talk about this topic a few years back https://www.youtube.com/watch?v=dCuZkaaou0Q&t=2s  
> **username_2** (2023-08-15): Suggestion: it might be useful to add guidance on how to pronounce unfamiliar symbols.  There are a few that I've never been entirely sure of, e.g. what's the name of the '⊢' symbol?  And I know 'Γ' is a greek capital letter, but I can't remember which...  
> **username_10** (2023-08-15): This was an excellent intro! I also noticed what @Indigenuity brought up about how the context is defined though. Also I think it would maybe be helpful to include an example of how something like 'let' works for introducing new variables (I know there is a let on the RHS in the function case for infer, but I mean how let would work in the lang we are trying to type).  
> **username_11** (2023-08-16): @occipita Yeah, I agree, knowing how to pronounce symbols always helps me! “⊢” can be read as “entails”. “Γ” is the typing context (ie. Gamma - no idea why this letter is used). “∈” can be read as “element of”.  
> **username_3** (2023-08-18): What is this symbol, `⊣`, and its usage as seen in `Γ⊢e:τ⊣Δ` ?  
> **username_0** (2023-08-20): @ErikEidt It is nothing more than $⊢$ flipped to point the other way (called `\dashv` in LaTeX). I don’t believe it has any particular meaning in formal logic, at least not in the way $⊢$ does; it’s just syntax.  
> **username_4** (2024-06-27): It is an odd quirk of the notation that in `e ::= e + e`, each occurance of `e` can be a different expression, but in the typing judgment for `if` expressions, each occurance of τ must correspond to the same type....  
> **username_5** (2024-06-27): @BrianGoetz In a grammar, it would be sort of annoying to write subscripts for each occurrence since you almost never want to require that two subterms are the same. On the other hand, in an inference rule it's fairly common that you want two things to be the same.  
> **username_4** (2024-06-27): @DavidYoung Oh, I get it.  I just found it notable that I've intuitively understood this inconsistency for many years but never consciously noticed it before.  But I can imagine others being confused by this, since it is not explicitly written down (nor is very much written down about CSM at all, as Guy reminds us all.)  
---
