<p>IMHO, it's not like <em>constructors</em> are checked, but <em>introduction rules</em> (including tuples, lambdas, data constructors, etc.) are checked (while elimination rules are synthesized). The kind constructors you mentioned are called <em>formation rules</em>, which are not introduction rules. You can also think this way: if a <em>constructor</em> is checked, then it has a <em>corresponding eliminator</em> which is synthesized. If type constructors should be checked, there should be a corresponding thing synthesized. But there's no such thing (you can't pattern match on <span class="math-container">$\cal U$</span>).</p>

CC BY-SA 4.0
2021-05-19T07:50:11.750Z
2021-05-20T01:12:41.613Z
2021-05-20T01:12:41.613Z
ice1000
<p>I don't have an answer for that question, I'm afraid.  But I'll just point out that the rule you cite doesn't say that we should use <code>Γ ⊢ e₁ e₂ ⇒ τ</code> just because function application is an eliminator.  Instead, it says that within the typing rule for function application, the part that checks the actual function should synthesize (i.e. should be <code>Γ ⊢ e₁ ⇒ τ₁ → τ₂</code>), and once you have this, then which of <code>e₂</code> and <code>e₁ e₂</code> are checked or synthesized are simple/obvious engineering choices.</p>

CC BY-SA 4.0
2021-05-19T20:05:30.267Z
Thanks! I guess I misread the explanation. Can you clarify for me the *correct* explanation of which part should be checked and which should be synthesized, in general?
Siddharth Bhat
CC BY-SA 4.0
2021-05-19T18:17:12.450Z
2021-05-19T18:17:12.450Z
Stefan
<p>According to the <a href="https://www.cs.cmu.edu/%7Efp/courses/15312-f04/handouts/15-bidirectional.pdf" rel="nofollow noreferrer">Pfenning philosphy of bidirectional typing</a>, as also explained by <a href="https://arxiv.org/abs/1306.6032" rel="nofollow noreferrer">Dunfield and Krishnaswamy 2013</a>, constructors should be checked, while eliminators should be synthesized. Cconvention is followed for the most part in the tutorial <a href="http://davidchristiansen.dk/tutorials/nbe/" rel="nofollow noreferrer">Checking Dependent Types with Normalization by Evaluation: A Tutorial
by David Christiansen</a>. I cannot explain some choices in the tutorial according to the Pfenning philosophy:</p>
<p>The types <code>Sigma x A B</code> and <code>Pi x A B</code>, <code>Nat</code>, <code>Eq A from to</code>, <code>Trivial</code>, and <code>Absurd</code> are all checked in <em>synthesis mode</em>. However, these are <em>kind constructors</em>, as they let us construct values that live in <code>Univ</code>. Why are they checked in synthesis mode?</p>
<p>Can we view these as eliminators of some object that I am unaware of? As an example of what I mean by this, recall that identifiers such as <code>x</code> are also run in synthesis mode. With a bit of squinting, one can convince themselves that identifiers are <em>projections on the context</em> <code>Γ</code>
, and thus deserve to be run in synthesis mode.</p>
<p>Is there a similar explanation for why <code>Pi</code>, <code>Simga</code>, <code>Eq</code>, <code>Trivial</code>, <code>Absurd</code> are typed in synthesis mode? what rule-of-thumb does one use to decide whether these should be typed  in checking or synthesis mode?</p>

<dependent-type><type-inference>
Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?
Siddharth Bhat
# Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?

(Asked by: username_0 on 2021-05-19)

According to the [Pfenning philosphy of bidirectional typing](https://www.cs.cmu.edu/%7Efp/courses/15312-f04/handouts/15-bidirectional.pdf), as also explained by [Dunfield and Krishnaswamy 2013](https://arxiv.org/abs/1306.6032), constructors should be checked, while eliminators should be synthesized. Cconvention is followed for the most part in the tutorial [Checking Dependent Types with Normalization by Evaluation: A Tutorial
by David Christiansen](http://davidchristiansen.dk/tutorials/nbe/). I cannot explain some choices in the tutorial according to the Pfenning philosophy:

The types `Sigma x A B` and `Pi x A B`, `Nat`, `Eq A from to`, `Trivial`, and `Absurd` are all checked in *synthesis mode*. However, these are *kind constructors*, as they let us construct values that live in `Univ`. Why are they checked in synthesis mode?

Can we view these as eliminators of some object that I am unaware of? As an example of what I mean by this, recall that identifiers such as `x` are also run in synthesis mode. With a bit of squinting, one can convince themselves that identifiers are *projections on the context* `Γ`
, and thus deserve to be run in synthesis mode.

Is there a similar explanation for why `Pi`, `Simga`, `Eq`, `Trivial`, `Absurd` are typed in synthesis mode? what rule-of-thumb does one use to decide whether these should be typed in checking or synthesis mode?

**Tags:** dependent-type, type-inference


---

## 2 answers

### Answer by username_1 on 2021-05-19. Score: 2 | Accepted answer

IMHO, it's not like *constructors* are checked, but *introduction rules* (including tuples, lambdas, data constructors, etc.) are checked (while elimination rules are synthesized). The kind constructors you mentioned are called *formation rules*, which are not introduction rules. You can also think this way: if a *constructor* is checked, then it has a *corresponding eliminator* which is synthesized. If type constructors should be checked, there should be a corresponding thing synthesized. But there's no such thing (you can't pattern match on $\cal U$).


---

### Answer by username_2 on 2021-05-19. Score: 2

I don't have an answer for that question, I'm afraid. But I'll just point out that the rule you cite doesn't say that we should use `Γ ⊢ e₁ e₂ ⇒ τ` just because function application is an eliminator. Instead, it says that within the typing rule for function application, the part that checks the actual function should synthesize (i.e. should be `Γ ⊢ e₁ ⇒ τ₁ → τ₂`), and once you have this, then which of `e₂` and `e₁ e₂` are checked or synthesized are simple/obvious engineering choices.

> **Comments:**
> **username_0**: Thanks! I guess I misread the explanation. Can you clarify for me the *correct* explanation of which part should be checked and which should be synthesized, in general?  

---

