documenting check/synth of forms

[pnwamk]

In a previous discussion with @david-christiansen and @dfried00 there was a desire to have the documentation indicate which positions are visited in check-mode and which are visited in synthesis-mode by the type checker.

Would superscript "c" (for check) and "s" (for synthesis) on identifier names (with a comment at the top of the docs indicating their meaning) be a reasonable solution? e.g.:

[david-christiansen]

That could work.

What about, alternatively, replacing the :s below the description with⇐ for check or ⇒ for synth? This matches notations used elsewhere, at least, but that might require more Scribble hacking.

[david-christiansen]

Also, how would you propose documenting check/synth for the resulting type? A superscript on the whole eliminator expression, or alternately the type after the arrow up top?

[pnwamk]

So, part of the reason I liked the initial solution I suggested is because I'm lazy and it was easy.

However, I really like your suggestion of (hopefully a little) hacking and making a scribble-like form that uses the double arrows, e.g.:

(iter-Nat target base step) ⇒ X
  target ⇐ Nat
  base ⇒ X
  step ⇐ (→ Nat X)

I wonder how difficult it would be...

[david-christiansen]

I imagine that something starting with a copy-paste of defform wouldn't be too hard, but that code is pretty abstracted and engineered...

[xieyuheng]

Why use the word synth or synthesis instead of infer ?

Does this choice have a reason ? If it does, I wish to learn :)

[david-christiansen]

I've seen both in the literature.

The reason I've come to prefer the term "synthesis" over "inference" in bidirectional type checking is to distinguish it from the more global type inference in Hindley-Milner-style systems. It seems to confuse somewhat fewer people, which makes me prefer it.