Global definitions are those that can appear in the typing context, as opposed to local definitions which can be represented by let-bindings and ultimately as just functions. Global definitions could be useful in investigating record types with manifest fields.
Bidirectional typechecking is a way of presenting the typing rules that is more algorithmic and thus better suited for implementation. It is also said to increase the quality of error messages. But most importantly, putting rules into the bidirectional format makes them less fishy.
Another way to make the presentation of your type theory less fishy, more concrete and down-to-earth and more amenable to implementation.
How to infer, in general, an inductive characterization of normal forms from the reduction relation?
Let's call this Partial types - something like Singleton Types, but it also has something to do with (first-class?) patterns and refinement types.
Examples:
{x : nat ^^^ x = S (S ?n)}- type of naturals that definitionally compute to2 + something. How do we compute with this? Dunno, but maybecoe : {x : nat ^^^ _} -> nat, with the rulecoe x => S (S ?n), whatever that means.{l : list A ^^^ l = []}- singleton type of empty lists.{p : nat * nat ^^^ fst p = 42}- type of pairs of naturals whose left component is definitionally equal to42, i.e.fst (coe p) = 42.{x : nat + bool ^^^ x = inr ?b}- sum type ofnatandbool, but its element are definitionally equal toinr something, so thatmatch coe x with | inl a => f a | inr b => g b endcomputes tog ?b.{s : Stream nat ^^^ hd s = 42}- type of streams whose head is42.{f : bool -> nat ^^^ f true = 42}- type of functions frombooltonatthat compute to42ontrue.{f : bool -> nat ^^^ f true = f false}- type of definitionally weakly constant functions frombooltonat.{f : bool -> nat ^^^ f _ = 42}- type of definitionally strongly constant functions that always returns42.- Maybe we need intersection and union types for this?