Bidirectional type checking

Graudalizer is using bidirectional type checking.

This means that the type checker has two modes:

• When an expression is checked against a specified type, the type checking starts with the whole expression and then proceeds into each part of the expression. When type checking an expression in this mode, no type is returned.
• When there is no specified type, the type checking is performed in the other direction. Types are propagated from the sub expressions outward. This is similar to Type inference, although by default, the only types that are propagated are types that are specified in a spec. This is to maintain the graduality property. See Gradual typing.

References:

• Bidirectional Typing, Jana Dunfield, Neel Krishnaswami

TODO:

• Add more links to papers about bidirectional type checking