Lambda the Ultimate

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.

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.

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.

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

I updated the top post to include the links.

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^- ]$$

.)

Thank you very much.

This explanation is much better than mine :)