Re: [MLton] towards type checking let polymorphism

On May 21, 2015, at 21:55 , Matthew Fluet <[email protected]> wrote:
> 
> On Wed, May 20, 2015 at 6:02 AM, Baojian Hua <[email protected]> wrote:
>> I'm reading Pierce's text "Types and Programming language". On page
>> 334 of that book, there is an example program of nested let binding
>> and says that the type checking would be very slow.
>> 
>> And I'm curious about the typing checking time, so I tried this program
>> both in SML/NJ and MLton. But I'm a little surprised to see that the
>> checking time of the NJ compiler is indeed very slow (I kill the
>> process after running several minutes); however, MLton
>> will check that program very quickly. I'm curious about how this
>> different behavior happens? Is there any special trick that MLton uses
>> to handle this case?
> 
> The general issue is that the type inferred for an expression can be
> exponentially larger than the (untyped) expression itself.  However,
> that exponential size is with respect to the "tree" structure of the
> inferred type.  The only way for a small expression to generate a
> large type is if there is some repetition in the type; by representing
> a type as a DAG rather than a tree, one can keep the representation of
> types small.

Not always. With H/M polymorphism, even a DAG representation can grow exponentially. See e.g. my answer to a similar question on SO for a simple example:

http://stackoverflow.com/questions/22060592/growth-of-type-definition-in-sml-using-hindley-milner-type-inference/22061847#22061847

/Andreas


------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud 
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y