Combining Inference and Checking
← Back to Bidirectional Type Checking
Bidirectional type checking alternates between synthesis mode (inferring a type from the expression structure) and checking mode (verifying that an expression has an expected type). This flow of type information in both directions reduces annotation requirements while supporting advanced features like higher-rank polymorphism.