| Given an invocation m.(x) with only a known type for x, the choice of |
| possible types for m may be derived by searching all operations with |
| parameter type typeof(x). Eventually, this may lead to a set of |
| constraints that allows for exactly determining the type of m, almost |
| like in a Sudoku. |
| |
| When an operation declares an argument without specifying its type explicitly, |
| from the uses of the argument in the operation definition a number of |
| constraints on the argument's type can be derived. Applying to it an operation |
| call requires a conforming operation to be present on the argument's type. |
| Assigning the argument to some variable requires the argument's type to conform |
| to the variable's type. Using the argument as an argument to some other |
| operation requires that the used argument's type conforms to the invoked |
| operation's argument's type. Analogously, the use of the argument in any |
| association manipulation or navigation operation will establish one or more |
| constraints on the type of the argument. |
| |
| Architecturally (compiler, tools), I'd love to implement the type inference as |
| an instant event- and constraint-driven knowledge base updater. Whenever a tiny |
| change is applied to the program's abstract syntax tree, the constraint solver |
| should determine the new updated solution or should flag inconsistencies and |
| constraint violations. |