Semantic Inference

I’m beginning to think about the finer details of my experimental language. In particular, I think that most of the semantic inference will come from type inference. And that is tricky, because I want subtyping and I want references (for type theory virgins, that’s a really tough combination; i.e. it is undecidable in general). And it is even trickier because some of the usage information is going to be missing.

However, I am not trying to do type inference in order to do type checking, which makes it a bit nicer. I am doing type inference in order to get whatever information I can out of the code to reconstruct the semantics the user was intending. So if you say something like:

    let x = 4
    print x

No type inference need be done, because the program is already semantically unambiguous.

What I want is a calculus which can pick objects of various types and combine them together to get a particular type. For example:

    list = [1,2,3,4,5]
    total = 0
    for i {
        total += i
    }

We can figure out that list :: List Int, total :: Int, and i :: Int. We also have that (after desugaring) for :: (a -> (), List a) -> (). The block given to for is of type Int -> () (by our inference on i), so it is looking for a List Int to fill the gap. list is clearly our candidate.

My guess is that this is not decidable. But this isn’t the kind of language that cares about that. It’ll just say “uh, I can’t figure this one out, please give me more info” and then the user will be all “ok, here you go”. It’s not about getting everything right, it’s just about reducing the programmer’s workload in common cases.

Okay, so how do we deal with references (a side note, Firefox 2 has a spell checker and it doesn’t think that “Okay” is a word. Hmph.)? You can’t infer them if you have a type calculus with subtyping (you can use colored local type inference to get a lot of them right, though). First, because I’m a pure functional kind of dude nowadays, I think I’ll do references the ML way: you can only assign variables once, but you can put a reference in a variable and change the reference. That, of course, does not solve the problem. So I’m going to recommend that references be explicitly typed. If they aren’t, the type will default to Any; i.e. no semantic inference can be done with them.

So I think the bulk of my language will be a lambda calculus with a semantic/type inferencer as described above, plus some nice name correspondence rules.

Here’s something that’s a little strange: name resolution can depend on type inference. Consider this code:

    class Point {
        has x, y;
    }
    pt = getLocation();
    print x

This will not compile if getLocation‘s type cannot be determined. But if you annotate it getLocation :: Point, this will compile, since when it sees the unresolved identifier x, it will look for things in its scope which have an x member. Since that looks so funny, I may want to reserve that kind of inference .x instead.

Even weirder: type inference can depend on naming. This is the inflector module, which I haven’t talked about much. If you see code like this:

    class Point {
        has x,y;
    }
    point = getLocation();

Without any information about getLocation (or any other way to determine the type of point), the language will assume that point is of type Point. I would also like it to assume that points is of type List Point (or maybe something more general like Aggregate Point). Finally, I’d like it to build a connection that infers foo :: a implies foos :: List a (and vice versa).

I’m not certain if this incredibly presumptuous type inferencer plus a semantic inferencer based on that will give me everything I want, but it is possible that it will do an awful lot.

UPDATE: Ooh, I was lying in bed thinking about this, and I realized that the sort of type inference we are doing is much weaker than usual type inference. The fact that we don’t care what the type is, we’re only asking questions about it (eg. does it fit in an Aggregate?), makes the job much simpler (doable with an equation reduction algorithm) and also allows for a more versatile type system. Cool!

About these ads

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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 )

Google+ photo

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

Connecting to %s