Re: [MLton] towards type checking let polymorphism

On Fri, May 22, 2015 at 8:21 PM, Andreas Rossberg <[email protected]> wrote:
> 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

Interesting. However, I think if you had type inference based on
flexible types in order to support higher-order polymorphism (ala HML)
even your stackoverflow example requires linear space. In HM inference
it's the specialization at each variable reference followed by
generalization at the val clause that prevents sharing. If flexible
types were used [1], the decision to specialize gets deferred and
sharing remains possible.

I wonder what it would take to make that system go exponential.

[1] http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski@icfp08:mlf-type-inference.pdf

------------------------------------------------------------------------------