nac3-spec/hm-inference

Type Inference

This is a prototype before Rust implementation of the algorithm.

Implemented Features

• Primitive types: bool, float, integer. (limited magic methods are implemented, no casting for now)
• Statements:
  • For loop.
  • While loop.
  • If expression.
  • Simple assignment. (without type annotation, allows pattern matcing for tuples)
• Expressions:
  • Boolean operations.
  • Binary operations. (+, -, *, /, //)
  • Compare.
  • Function call. (posargs/kwargs/optional are supported)
  • Lambda.
  • Object Attribute.
  • List/tuple subscript. (tuple requires constant indexing)
  • Virtual.
  • Constraints for type variables.

User can define functions/types by adding them to the prelude.

Note that variables can be used before definition for now, we would do another pass after type checking to prevent this. The pass would also check for return.

We assume that class type do not contain any unbound type variables. (methods can contain unbound type variables, if the variable is bound to the class)

TODO

• Parse class/function definition.
• Occur check to prevent infinite function types.
• Pretty print for types. (especially type variables)
• Better error message. (we did not keep any context for now)

Implementation Notes

• Type variables would now retain a lot of information, including fields and its range for later checking.
• Function type is seperated from call type. We maintain a list of calls to the same function (potentially with different type signature) to allow different instantiation of the same function.
• We store the list of calls and the list of virtual types, and check the constraints at the end of the type inference phase. E.g. check subtyping relationship, check whether the type variable can be instantiated to a certain type.