Home » forums » LtU Forum

An attempted approach to type inference with subtyping

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

By Eli Sennesh at 2013-07-23 16:49 | LtU Forum | previous forum topic | next forum topic | other blogs | 4829 reads

Comment viewing options

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

Inferred type of twice

Are you sure you want a complete algorithm? Think about what type you want to infer for twice:
twice f x = f (f x)

The discussion in section 2.5 in Polymorphic subtyping in O’Haskell should be relevant food for thought.

By Peter A Jonsson at Tue, 2013-07-23 20:08 | login or register to post comments

Nordlander's paper is

Nordlander's paper is actually my biggest precedent! I tried to talk about this work with him, but he didn't have the time and has long-since moved on to other things.

Shouldn't twice come out as the following? I would think it should, since we need to constrain the output of the first application of f to feed directly into the input of the next application of f.


twice f x = f (f x)
twice :: forall 'a. forall 'b. ('a -> 'b) -> 'a -> 'b | 'b <: 'a

So yes, I do believe I want completeness here. The distinction with the previous "constraint set" approaches is that I don't generate arbitrary sets of subtyping constraints, I generate the minimal convex lattice describing the variable (the formal definition for those is in my notes).

If we want simpler types as Nordlander was generating, it's very simple from within the system I have to just take each minimal convex lattice consisting only of free variables and collapse it down to a single replacement variable. That will recover the nice simple HM-style types Haskell yields, but that's a step into aesthetically-pleasing incompleteness from what my type system and inference engine will currently generate.

By Eli Sennesh at Tue, 2013-07-23 21:22 | login or register to post comments