Home

Polymorphism, subtyping and type inference in MLsub

I am very enthusiastic about the following paper: it brings new ideas and solves a problem that I did not expect to be solvable, namely usable type inference when both polymorphism and subtyping are implicit. (By "usable" here I mean that the inferred types are both compact and principal, while previous work generally had only one of those properties.)

Polymorphism, Subtyping, and Type Inference in MLsub
Stephen Dolan and Alan Mycroft
2017

We present a type system combining subtyping and ML-style parametric polymorphism. Unlike previous work, our system supports type inference and has compact principal types. We demonstrate this system in the minimal language MLsub, which types a strict superset of core ML programs.

This is made possible by keeping a strict separation between the types used to describe inputs and those used to describe outputs, and extending the classical unification algorithm to handle subtyping constraints between these input and output types. Principal types are kept compact by type simplification, which exploits deep connections between subtyping and the algebra of regular languages. An implementation is available online.

The paper is full of interesting ideas. For example, one idea is that adding type variables to the base grammar of types -- instead of defining them by their substitution -- forces us to look at our type systems in ways that are more open to extension with new features. I would recommend looking at this paper even if you are interested in ML and type inference, but not subtyping, or in polymorphism and subtyping, but not type inference, or in subtyping and type inference, but not functional languages.

This paper is also a teaser for the first's author PhD thesis, Algebraic Subtyping. There is also an implementation available.

(If you are looking for interesting work on inference of polymorphism and subtyping in object-oriented languages, I would recommend Getting F-Bounded Polymorphism into Shape by Ben Greenman, Fabian Muehlboeck and Ross Tate, 2014.)

By gasche at 2016-11-23 16:54 | Type Theory | other blogs | 74928 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Cool paper

This is indeed awesome work, and I'm glad to finally see it published as it deserves.

In case you'll miss POPL'17, Stephen Dolan already gave a talk about it at last year's (2015) ML workshop, which can be watched here.

By Andreas Rossberg at Wed, 2016-11-23 19:36 | login or register to post comments

Looks neat indeed.

Looks neat indeed. Interesting that a real solution to subtyping was found by sort of redefining the language describing the problem, ie. type variables no longer quantify over ground types solves many of the earlier difficulties in integrating subtyping.

The type syntax for MLSub actually looks simple enough to use by mere mortals too. Also neat that MLSub can type the self-application function, which isn't possible in ML.

By naasking at Thu, 2016-11-24 03:35 | login or register to post comments

Unneat

Also neat that MLSub can type the self-application function, which isn't possible in ML.

That's a very persistent myth. It is easily possible in ML if you choose to make it so via equi-recursive function types. Problem is, in practice, you don't want this! Because many plain bugs become well-typed and lead to obscure errors downstream. See OCaml's -rectypes option, which was the default initially but was turned into an option because users complained. MLsub probably has this very problem.

By Andreas Rossberg at Thu, 2016-11-24 07:03 | login or register to post comments

Restrict subtyping to fine types

First, let me agree that this paper looks awesome - great bang/buck. I think your particular complaint here points to a need for better UX around subtyping. "Matrix or String" isn't a very useful inferred type, either. I think we need coarse types that unify by equality to rule out nonsense like this example or self-application with fine types that support subtyping.

By Matt M at Fri, 2016-11-25 02:46 | login or register to post comments

Recursive types and type errors

Actually, MLsub types the self-application function nonrecursively, as ((a -> b) & a) -> b. You can call that passing e.g. a constant function returning integers (type Top -> int) and get back an integer, all without recursive types. Self-applying self-application does use recursive types, though, as you'd expect.

You're right about this making weird code become well-typed. MLsub is pretty willing to give a strange type to bad code, especially if you use currying pervasively (currying always interprets missing arguments as partial application, which can generate weird function types. Implementing multiple argument functions with tuples turns missing arguments into type errors).

On the other hand, I've found that the downstream type errors are less obscure than in unification-based systems. Because subtyping keeps track of the direction of data flow, type errors can always be explained by showing an introduction form in the program, a series of data-flow steps (e.g. from a variable's binding to its use), and then an elimination form into which the value doesn't fit.

So, compared to ML, more buggy definitions are initially accepted, but when you try to use them the type error makes more sense. I've not written large enough programs to know how the tradeoff pans out, though.

By Stephen Dolan at Sat, 2016-11-26 14:12 | login or register to post comments

While you're here...

Any advice for someone who wants to read through your thesis?

By Matt M at Fri, 2016-12-02 19:39 | login or register to post comments

Thesis draft and implementation

Stephen's thesis draft and implementation are available online.

By Catalin Hritcu at Sat, 2017-01-21 18:32 | login or register to post comments

Thanks

I updated the top post to include the links.

By gasche at Sat, 2017-01-21 21:35 | login or register to post comments

Reading the thesis

I am currently reading Dolan's thesis and though I can make sense of the concepts I cannot make sense of some notations, namely in section 5.3.1 page 81 the definition of a bisubstitution:

θ = [μ−β.α u [β/α−](t−)/α−]

The square brackets seem used both to denote the typing schemes as in [D-]t+ and substitutions proper as ξ = [t+/α+, t−/α−]

In the above θ what binds to what?
Is [β/α−](t−) a typing scheme?
Why does /α− appear TWICE with a different left hand side?
That would be binding the same α− to two different values???
Is the overall expression to be read:

[ (μ−β.α u [β/α−](t−)) /α−]

Or:

[μ−β.α u ([β/α−](t−))/α−) ]

Or something else?

By Kevembuangga at Fri, 2018-05-11 16:20 | login or register to post comments

Bisubstitution

It is the first interpretation you propose

$$\left[ \left(\mu^{-}\beta. \left(\alpha \sqcap [\beta/\alpha^{-}]t^{-}\right)\right) / \alpha^{-} \right]$$

which is built in the following way. You start from the bisubstitution representing the "naive" solution

$$[ (\alpha \sqcap t^{-}) / \alpha^{-} ]$$

but then you want to replace occurrences of \(\alpha\) within \(t^{-}\) by the solution \(\alpha \sqcap t^{-}\); the solution to this recursive replacement problem would be a type \(u^{-}\) defined by the following recursive equation

$$u^{-} = \alpha \sqcap [u^{-}/\alpha^{-}]t^{-}$$

which is precisely what you get using a \(\mu\)-type

$$\mu \beta.\ \alpha \sqcap [\beta/\alpha^{-}]t^{-}$$

so you get the final bisubstitution

$$[ \mu^- \beta. \alpha \sqcap [\beta/\alpha^-]t^- / \alpha^- ]$$

(note: in LtU I write this code with

$$[ \mu^- \beta. \alpha \sqcap [\beta/\alpha^-]t^- / \alpha^- ]$$

.)

By gasche at Fri, 2018-05-11 21:47 | login or register to post comments

Thank you very much.

Thank you very much.

By Kevembuangga at Sat, 2018-05-12 04:20 | login or register to post comments

Bisubstitution

This explanation is much better than mine :)

By Stephen Dolan at Thu, 2018-05-17 10:46 | login or register to post comments

Ad hoc polymorphism?

In section 10.2.3 (ad-hoc polymorphism) on page 142 of Stephen Dolan's thesis, the claim is made that the following rule holds for SubML:

$$(t_1 \sqcup t_1') \to (t_2 \sqcap t_2') = (t_1 \to t_2) \sqcap (t'_1 \to t_2')$$

An example is given that shows that this doesn't hold in languages with ad hoc polymorphism (in the form of typecase). But it looks like this property doesn't hold for refinement types, either. Choose:

$$ t_1 = t_2 = Int \{ \geq 0 \} $$

$$ t'_1 = t'_2 = Int \{ \leq 0 \} $$

Then the identity function is an element of the RHS of the rule above but not an element of the LHS (which would need to map all of Int to the singleton zero).

My question is whether someone can explain/characterize why this should work for "well behaved" type systems and why refinement types aren't well behaved in this sense.

By Matt M at Fri, 2018-07-13 00:37 | login or register to post comments