Type inference and generics post-mortem
This entry was taken from my old Fenris development blog. 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 gave my final presentation for CS 136c last week. This term I was adding three big features to the Fenris compiler and runtime: generic definitions (parametric polymorphism), fixpoint type inference, and garbage collection.
Generic definitions turned out fairly well. I implemented
polymorphism for both procedures (including functions, closures, and
methods), and classes. I ended up having to rewrite the class
inheritance system, but it was broken already. The type system also
required significant modification. I was surprised by how separate the
implementation was for both kinds of definitions, but they ended up
sharing a fair amount of code. The main limitation at the end was that
recursive polymorphism was not allowed. This is required for things
like the Java interface Compareable<T extends
Compareable<T>>
. The problem was just the order of
compilation.
Type inference didn't turn out as well as I had hoped. The main issue is that all definitions in a Fenris package are potentially mutually recursive, which imposes some theoretical limitations. The big limitation is that inference of polymorphic definitions is not possible, which is one of the nicest things about type inference in other languages. OCaml allows type inference for polymorphic definitions, but mutually recursive definitions can only call each other monomorphically, i.e., the type parameters are defined over the set of definitions rather than individuals. The other main problem with my type inference is that type constraints are collected from both uses and definitions. This was needed to resolve ambiguity mainly. It lets you do some cool stuff you wouldn't be able to do otherwise, but it causes some bad dependency issues. I think ultimately, I'll roll back my work on type inference. A future version of it might require types to be inferrable from definitions only, and global inference might not be allowed.
The last feature was garbage collection. I implemented a mostly-copying collector, and it ended up working quite well. This treats the stack conservatively, but the globals and the heap are all well-typed. There are some places where it can be optimized, but I would guess that performance is quite good. In any case, it's a big improvement over what I had before (allocating out of a big array and not collecting at all).
The future of Fenris is uncertain now. I ran into a lot of difficulties this term because the language is just too complex. I think the main problem is a lack of unified types. I would really like to see a future version of Fenris where every value is a class type (including functions). Variadic types might be added to accomodate a parameterized closure class, but I would get rid of structs, and primitive types. I also think definitions should be limited to variables, functions, in classes (mixed in any possible context), and the processing for each should be much more uniform across different contexts.
These changes will require some redesign for both the language and the compiler. There is a strong possibility that the compiler will be completely rewritten in another language (possibly OCaml or Haskell). Before any of that happens, I think I need to go out and learn a few languages to get some more experience with compilers. I'll be working with NVIDIA's compiler team this summer, and I'll have some free time for learning, so there's a strong possibility I will restart this project at some point at UCSD.