[Checkers] Thoughts on Type Inference: Part 2

[Mahmood Ali]

Greetings again,

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  
extensible.

__ 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  
problem.

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.

Regards,
Mahmood