Re: [MLton] towards type checking let polymorphism

Matthew Fluet <[email protected]> Thu, 21 May 2015 15:55:25 -0400
Newsgroups gmane.comp.lang.ml.mlton.devel
Message-ID <CAMrhFL6NWjQcMBDDz2vpG2_KrRvdnKyGAFjGtZAt3gapAwTQpg__20108.6987545297$1432238522$gmane$org@mail.gmail.com>
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.  You can also exploit the DAG representation to make
checking the equality of types and the instantiation of polymorphic
types more efficient.

Although MLton doesn't quite use full "hash-consing" for types when
performing type inference (it does use hash-consing for types later in
the compilation), the main idea is the same.

The importance of representing types as DAGs comes up in descriptions
of the FLINT intermediate language of SML/NJ:
  http://flint.cs.yale.edu/flint/publications/tic97.html
  http://flint.cs.yale.edu/flint/publications/imp.html
But, my understanding is that FLINT isn't directly used when
performing type inference, so SML/NJ may not be using a DAG
representation of types during type inference.

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