Fixpoint type inference

This entry was taken from my old Fenris development blog. It was originally posted on April 2, 2008. Although the Fenris project is now defunct, I think these old entries have some general appeal, so I've added them to this blog.

I'm planning on adding type inference to Fenris in the text few months, but I'm a bit concerned. Fenris allows interdependent definitions specified in arbitrary order, which is not the case with type inferred language I have worked with in the past. This could cause serious problems for type inference for globally accessible definitions. I have an idea for a solution to this involving a fixpoint type inference algorithm.

The algorithm would basically work like this: first, we make a list of all defined types. This includes primitives and all accessible classes. Second, we compile the module normally, putting in inferable types wherever types are unspecified. Each inferable type has a unique identifier, and we keep a list of all of them. While we do this, we build a list of constraints on each type. A constraint might take the form of "supports the + operator", "is the second parameter type for function foo", or "is a subclass of Bar". These constraints will depend on each other, which is not something we would get in a normal type inferred language. Once the initial compilation is complete, we run a fixpoint algorithm, copying constraints among inferred types until all constraints are stable. When this is complete, we go through the list of all inferred types and decide what type they really have, emitting errors if necessary. Finally, we make a pass through the compiled code, fixing and updating types and other code as necessary.

Obviously this algorithm needs a lot of details filled in. Things like function overloading and subtype polymorphism (especially covariance and contravariance) may make this very difficult. But I think it may actually work. Indeed, something like this is probably implemented in some language I haven't tried yet. If this doesn't work, I will need to compromise the language by either disabling arbitrary definition order or restricting type inference to inside functions (which may still have problems).

This also poses some challenges for indices and prototype caches. Indices should definitely have inferred types. The types of definitions in a package should not change depending on how they are used by other packages. On the other hand, definitions in prototypes may change, so it might be best to leave inferred types unspecified. Inferring types for prototypes would require more advanced dependency analysis as well.