[racket] Puzzled about type inference

On Aug 6, 2014, at 7:56 AM, Hendrik Boom wrote:

> On Tue, Aug 05, 2014 at 08:53:42PM -0400, Matthias Felleisen wrote:
>> 
>> You guys came up with some wonderful ideas. 
>> 
>> I think this particular one is easy to implement when 
>> the program type checks. But when it doesn't, what do 
>> you show? 
> 
> When the program fails to type-check, does the type-checker just throw 
> up its hands in despair because at the point where the contradiction 
> becommes apparrent it no longer has any knowledge as to where in the 
> source code it was working?  Is the assignment of types to expressions 
> not known at all until it is complete?  Hindley-Milner analysis is of 
> this kind.  Or does it assign types in a mostly bottom-up fashion with 
> possibly some top-down influence, until it finds one expression that 
> has a type incompatible with context?  In that case, there's still 
> clear information to present to the programmer.


Let's not wave hands for the sake of those who followed this thread up to this point. 

Conventional HM type inference (reconstruction) assigns type variables to all those places where programmers don't write down types, uses the algebraic structure of the type and expression language to set up equations among the types of expressions (including the type variables), and uses (symbolic) Gaussian elimination to solve those equations. If there are too few equations, you get solutions with free type variables, which yields HM's second-class parametric polymorphism. If you get contradictions, 

  Example:  
    f : __?__ = (lambda ({ x : __?__) 10) 
    assign TF and TX to __?__ places
    use type of lambda is [TX -> Integer] because 10 is Integer 
    equate TF = [TX -> Integer]
    one equation, two variables -> f is polymorphic like this: (forall (TX) [TX -> Integer]) 

If you apply this analysis to the entire module, you can (1) reduce a lot of the programmer's work and (2) smear the variables across a wide swath of space when you perform Gaussian elimination. 

Typed Racket performs local type inference. This means (1) we impose more work on the programmer and (2) smear type variables across a smaller space. 

BUT when type inference fails, you have already lost track of the original relations among variables and you have at least two contradictory equations. Worse, a solution may change almost all equations in your system. So no, you don't know all that much when a theorem prover (even a specialized one such as HM) fails on you. But yes, since we are doing local inference and these expressions tend to be small, one could investigate the idea and see how far users can follow. 

-- Matthias