We should support explicit type annotations of the form term : term. The dynamic semantics would be to reduce to the left-hand term and ignore the annotation. The static semantics would be:
Γ ⊢ t : q
---------------
Γ ⊢ (t : q) : q
Benefits:
Useful for bidirectional type checking, to switch between inference/pull mode and checking/push mode. See #3.
Top-level type signatures name : q = t can be desugared to name = t : q, maybe using #44.
Syntactic clues for typing (such as special keywords or System F syntax) can be desugared. For example, type name = t to name = t : * and value name = t to value = t : (_ : *). See #4 for System F Syntax and #3 for the _ wildcard.
Sometimes useful for debugging, to annotate the type we think a sub expression has, and get it confirmed by the type checker.
Given benefit 3, maybe the colon should be right-associative, so that t : q : s is parsed as t : (q : s)?
We should support explicit type annotations of the form
term : term. The dynamic semantics would be to reduce to the left-hand term and ignore the annotation. The static semantics would be:Benefits:
name : q = tcan be desugared toname = t : q, maybe using #44.type name = ttoname = t : *andvalue name = ttovalue = t : (_ : *). See #4 for System F Syntax and #3 for the_wildcard.Given benefit 3, maybe the colon should be right-associative, so that
t : q : sis parsed ast : (q : s)?