According to the Pfenning philosphy of bidirectional typing, as also explained by Dunfield and Krishnaswamy 2013, 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. I cannot explain some choices in the tutorial according to the Pfenning philosophy:
Sigma x A B and
Pi x A B,
Eq A from to,
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
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?