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