Lambda the Ultimate

I first wrote to Sean McDirmid about this regarding the previous "Subtyping is a pig" thread here on LtU, and he advised me to post to the forum seeing if anyone's interested and able to engage the material.

I'm going to try to convey here the shortest outline I can manage of the paper I've been brewing. It has been brewing for a number of years, because I do not have any fellow type-theorist to turn to and I'm godawful at writing scientific papers.

Anyway...

Start with a structural type system that has prenex polymorphism and structural subtyping. To integrate for those two, we allow for bounded quantification. How can we go about inferring types for this system in a sound and complete way? Previous proposals (correctly, I think) have pointed to having sets of inequality constraints.

How do I think I'm solving those?

1. I temporarily alter one of the subtyping rules (regarding variable <: variable constraints when both variables are bounded) to read slightly differently, using the Transitive Property of Subtyping.

2. I run an inference procedure in that "modified universe" that is quite similar to unification (takes advantage of structural subtyping rather than nominal). For each type variable \alpha, this procedure finds the smallest convex sublattice (of the total subtyping lattice induced by structural subtyping) containing the concrete types and other free variables constrained to subtype \alpha.

3. I "modify" (invoking Curry-Howard to get my logical soundness here) the inference procedure's results to obtain equivalent typings for the "original universe" with the correct variable <: variable subtyping rule. Specifically, when variables map to a convex sublattice bounded on one end by \top or \bot, I throw out those sublattices and replace those variables with the non-truistic bounds (because \bot <: \alpha means \bot \arrow \alpha, which is a truism).

4. I perform a last step of inference to actually enforce the correct, original variable <: variable subtyping rule where it remains applicable.

At this point, I believe I now have a substitution mapping every type variable to either a concrete type, or a minimal convex sublattice "centered on" that variable.

Anyone interested in this? What have previous approaches to this problem done (I may have heard of them already)? Have other problems ever yielded to an approach like this one?

I can zoom in on any part of the logic if necessary.

Thanks and cheers,
Eli