[Checkers] Thoughts on Type Inference: Part 2
mahmood at MIT.EDU
Thu Sep 11 01:02:04 EDT 2008
This email would touch on the type inference algorithm itself for IGJ
and how we can refractor it to make a more generic type inference.
__ IGJ specific core algorithm __
We do it in three stages:
1. Analysis to infer mutability, which is identical to Javari. Find
references that need to be mutable, and propagate their mutability to
any Object/reference that the reference could refer to.
2. If a reference is known to be a mutable reference, then all
remaining references that could point to this reference must be read-
onlys (i.e. cannot be immutable).
3. All remaining references are immutable!
Unfortunately, this is very IGJ specific algorithm and not very
__ More generic algorithm __
For any type system, we can generate constraints for a reference based
on the values it refers to and potential method invocation.
Basically, we simply reverse the rules used for type checking:
1. For any assignment (or pseudo-assignment) 'a = b', 'a' type needs
to be a supertype of 'b'.
2. For any method invocation (another form of pseudo-assignment),
'a.m()', 'a' type needs to be a subtype of 'm()' receiver.
3. needs to inverse some other rules (e.g. field re-assignment in IGJ,
de-referncing for nullness).
The qualifier on a reference 'a' type is the supertype of all
qualifiers of the types of values it 'a' could potentially refer to
and a subtype of qualifiers on receivers of the methods that could
potentially be invoked on 'a'. This should be sufficient for finding
all mutable references and read only references. Any remaining
references can be marked as Immutable, in IGJ. (I may need to
elaborate on this point).
__ Error in code __
Javari algorithm and most type inference algorithms assumes that the
code is valid code. Unfortunately, this is an unreasonable
assumptions for some type systems.
It is known, for example, that Java code are full of null pointer
errors. We cannot infer nullness property properly if the code is
invalid. Other type systems (maybe IGJ and Javari) may not have this
The second more generic approach could easily find such errors, as
they would result in a contradiction in the bounds of the reference.
OK... Need to sleep now. I will write a document later about this.
More information about the checkers