Complete Lattice Type System

I implemented a simple-minded type inferencer for meme (all monotypes–no polymorphism). Then I started implementing “Builtin” AST nodes so that I could have polymorphism in specific examples, like if. That got me wondering whether I could do polymorphism, as long as it was declared. I ran through the type inferencer algorithm by hand for hours, trying out different features to handle that case (this was an extremely tedious process). Finally I took my simple type inferencer and added a bunch of features to experiment with in code, rather than by hand. It went through several iterations, the first being universal types instantiate themselves on the left side of a <:, and “generalize” on the right. This generalization was similar to instantiation, but it would be come an “uppercase” variable, which would need to be instantiated again if it ever passed through a function argument.

Of course, that first iteration was a miserable failure. After messing around with it and racking my brain a bit more, I eventually came up with a way to do suprema and infima à la my last type theory post. And after fixing a few key things, IT WORKED. That is to say, it worked on my example. But it wasn’t a totally trivial example; it underlined the key thing I wanted it to do. Namely, this expression: (\id -> (id 1, id "hi")) ((\x -> x) :: forall a. a -> a), which is better than Haskell does :-).

I made it so you mark the type variables your are solving for as either supremum or infimum types. Function parameters can safely be infima, and function return values can safely be suprema. All the rest, I think, can be marked singular (i.e. standing for an atomic or an arrow type). Then there are a few laws that reduction must follow with these types. Namely: limit types (that’s the name I give to infima, suprema, and universal types together) cannot instantiate in equations involving other limit types (this makes sense mathematically; if the two types are equal, and they truly are nonsingular, then there is in fact no valid instantiation). Then there are rules for instantiating limit types when they are in equations with singular types.

However, the algorithm isn’t totally clean. It does some hackish stuff to make sure that it terminates (in this example; I’m nowhere near proving that the algorithm always terminates). It marks instantiated variables as “I have been instantiated, don’t instantiate me again”, which I don’t consider to be a very clean or correct solution. However, it does seem to work (and I’ve tried giving the algorithm input that I thought would make it infinite loop, such as self-referential types, and it didn’t).

Anyway, I’m not going to go too in-depth at the moment. I have to get to bed. Suffice it to say that it’s very cool. The source code is here (needs GHC 6.6 to run). To see that the output worked, note that the result of id 1 above is the variable v4, and the result of id "hi" is the variable v6. Somewhere in the big spew of output, you’ll see the lines Int <: v4 and Str <: v6, and (very important) not Int <: v6 or vice versa.

1 thought on “Complete Lattice Type System

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s