<p>I'm reading <em>Practical Foundations for Programming Languages</em> by Robert Harper and am confused by the exercises in Chapter 4, &quot;Statics&quot;, where he discusses a (monomorphic) type system.</p>
<p>The exercise instructs to provide an &quot;operational&quot; reading to typing judgements by refining <span class="math-container">$e : \tau$</span> relation into two: an &quot;analytic&quot; <span class="math-container">$\Gamma \vdash e \downarrow \tau$</span> indicating that the judgement is derivable, and a &quot;synthetic&quot; <span class="math-container">$\Gamma \vdash e \uparrow \tau$</span> saying that the type can be determined from the context <span class="math-container">$\Gamma$</span> and the expression <span class="math-container">$e$</span>.</p>
<p>I'm unsure if I've grasped the author's intent correctly. I replaced <span class="math-container">$:$</span> of the typical rules with &quot;synthetic&quot; <span class="math-container">$\uparrow$</span>, with an additional rule saying that &quot;analyzable given synthetic&quot;, i.e., <span class="math-container">$e \downarrow \tau$</span> given <span class="math-container">$e \uparrow \tau$</span>.</p>
<p>For the following exercise, I constrained the rules so that all the elimination forms are &quot;synthetic&quot; while the introduction forms are &quot;analytic&quot;.</p>
<p>My interpretation is that the whole purpose of this set of exercises is to augment the syntax with &quot;type-casting&quot; annotations in the let-construct to streamline the type-checking procedure, avoiding the standard unification algorithm.
Is this a correct understanding of the author's intentions?</p>

<static-typing><type-inference>
Understanding the "operational" reading of typing judgements in PFPL by Robert Harper, Chapter 4 Statics
<p>Your understanding is right but not quite the full picture.</p>
<p>What this is leading up to is <em>bidirectional typechecking</em>, where typechecking is split into these two judgements. This helps with mechanisation because it annotates the typing rules with <em>modes</em>. That is, in the checking judgement <span class="math-container">$\Gamma \vdash e \downarrow \tau$</span>, the context <span class="math-container">$\Gamma$</span>, term <span class="math-container">$e$</span>, and type <span class="math-container">$\tau$</span> all have <em>input</em> mode, while in the synthesis judgement <span class="math-container">$\Gamma \vdash e \uparrow \tau$</span>, the type <span class="math-container">$\tau$</span> is an <em>output</em>. These modes help derive a syntax-directed algorithm that tells you whether to do checking or synthesis at each step.</p>
<p>You switch between synthesis and checking when you hit an annotation, as you’ve seen. You also correctly surmised that in a “pure” bidirectional system, you should do <em>checking</em> of introduction forms and <em>synthesis</em> for elimination forms. But in practice, you will want to add some extra rules, otherwise you won’t be able to derive “obvious” things like <span class="math-container">$\Gamma \vdash \mathrm{true} \uparrow \mathrm{Bool}$</span> without annotations.</p>
<p>You may still do unification to solve congruences or subtyping constraints between types involving unknown metavariables. However, the difference is that in the traditional Damas–Hindley–Milner / Algorithm W style, you first accumulate a set of constraints with no particular direction, and then solve them by unification. A folklore result is that bidirectional type checking tends to make it easier to produce helpful type error messages, and this is the reason: with HM, the flow of type information is harder to follow because it can change direction at any point during unification and travel far from where it originated.</p>

CC BY-SA 4.0
2024-04-20T21:43:51.793Z
2024-04-20T21:43:51.793Z
Jon Purdy
CC BY-SA 4.0
2024-04-21T15:18:21.527Z
Thank you for the comprehensive answer and especially for providing the pointer "bidirectional typechecking"! I found this thorough survey [Bidirectional Typing](https://arxiv.org/abs/1908.05839) on this topic. It would have been great if the intent was a little bit more explicit in the textbook though.
Jay Lee
# Understanding the "operational" reading of typing judgements in PFPL by Robert Harper, Chapter 4 Statics
Posted by: username_0 on 2024-04-20
I'm reading *Practical Foundations for Programming Languages* by Robert Harper and am confused by the exercises in Chapter 4, "Statics", where he discusses a (monomorphic) type system.

The exercise instructs to provide an "operational" reading to typing judgements by refining $e : \tau$ relation into two: an "analytic" $\Gamma \vdash e \downarrow \tau$ indicating that the judgement is derivable, and a "synthetic" $\Gamma \vdash e \uparrow \tau$ saying that the type can be determined from the context $\Gamma$ and the expression $e$.

I'm unsure if I've grasped the author's intent correctly. I replaced $:$ of the typical rules with "synthetic" $\uparrow$, with an additional rule saying that "analyzable given synthetic", i.e., $e \downarrow \tau$ given $e \uparrow \tau$.

For the following exercise, I constrained the rules so that all the elimination forms are "synthetic" while the introduction forms are "analytic".

My interpretation is that the whole purpose of this set of exercises is to augment the syntax with "type-casting" annotations in the let-construct to streamline the type-checking procedure, avoiding the standard unification algorithm.
Is this a correct understanding of the author's intentions?
**Tags:** static-typing type-inference
---
## 1 answers
### Answer by username_1 on 2024-04-20. Score: 7 | Accepted answer
Your understanding is right but not quite the full picture.

What this is leading up to is *bidirectional typechecking*, where typechecking is split into these two judgements. This helps with mechanisation because it annotates the typing rules with *modes*. That is, in the checking judgement $\Gamma \vdash e \downarrow \tau$, the context $\Gamma$, term $e$, and type $\tau$ all have *input* mode, while in the synthesis judgement $\Gamma \vdash e \uparrow \tau$, the type $\tau$ is an *output*. These modes help derive a syntax-directed algorithm that tells you whether to do checking or synthesis at each step.

You switch between synthesis and checking when you hit an annotation, as you’ve seen. You also correctly surmised that in a “pure” bidirectional system, you should do *checking* of introduction forms and *synthesis* for elimination forms. But in practice, you will want to add some extra rules, otherwise you won’t be able to derive “obvious” things like $\Gamma \vdash \mathrm{true} \uparrow \mathrm{Bool}$ without annotations.

You may still do unification to solve congruences or subtyping constraints between types involving unknown metavariables. However, the difference is that in the traditional Damas–Hindley–Milner / Algorithm W style, you first accumulate a set of constraints with no particular direction, and then solve them by unification. A folklore result is that bidirectional type checking tends to make it easier to produce helpful type error messages, and this is the reason: with HM, the flow of type information is harder to follow because it can change direction at any point during unification and travel far from where it originated.
> **Comments:**
> **username_0** (2024-04-21): Thank you for the comprehensive answer and especially for providing the pointer "bidirectional typechecking"! I found this thorough survey [Bidirectional Typing](https://arxiv.org/abs/1908.05839) on this topic. It would have been great if the intent was a little bit more explicit in the textbook though.  
---
