Type equation inference

luqui on 2005-09-15T02:46:18

Before TaPL comes in the mail and I'm "forced" to actually read about this, I'm working on a type inference algorithm. It's always kind of fun to pretend that all that research out there doesn't exist and become a pioneer. You'll either come up with an inferior approach that makes some trade-offs that the real pioneers didn't think of, or you'll come up with the same thing they did, but you'll understand it really well, because you thought of it. The latter happens to me a lot.

Anyway, here's my algorithm. It considers all types to be sets, nothing more, nothing less. It also considers type classes to be sets of types (sets of sets). That way, you can use the same algorithm to do type inference and type class inference. It also lets you trivially do type class classes, whatever those are.

The two operations it works with are "does" (subset) and "in" (element). Let's look at how it would translate some simple code into type equations:

    sub fact($x) {        # fact: a --> b
        if $x == 0 { 1 }
              # ==: c,c --> Bool | Eq[c]
        else       { $x * fact($x - 1) }
              # -: d,d --> d | Num[d]
              # *: e,e --> e | Num[e]
    }

This gives rise to the following type equations:

    # conditional
    a does c
    0  in  c
    c  in  Eq
    Bool does Bool
    # if branch
    1  in  b
    # else branch
    a does d
    1  in  d
    d  in  Num
    d does e
    a does e
    e does b

I think that's all of them. Clearly these can be programmatically generated, if you give the code a function that can create unique variables. Then it's just a simple (!) matter of solving the equations, and you have all the type constraints everywhere in your function.

My current approach for solving these is to consider all the "does" relations to form the edges of a graph, and all the "in" relations to form the edges of another graph. I take the transitive closure of the "does" graph. All strongly connected vertices are then exactly the same thing (if you remember from your abstract math class, if a is a subset of b and b is a subset of a, then a = b). Then I substitue into the "in" graph, which gives me back all the constraints. Currently, however, there's a little problem, because it will give constraints like "a does some class that is a member of Num", which aren't exactly user-friendly. They don't mean a lot to me, either. So, that's the kink at the moment. More updates once I have some code, instead of paper scribbles.

---

Nitpicks and comments

roger.hale on 2005-09-15T07:59:47

Instead of
        d does e
I get
        d does a
        b does e
(from the call to fact).

Inferring
        a == d
        b == e
leaves
        1 in a in Num
        1 in b in Num
        0 in c in Eq
        a does b
        a does c
which may not be as tight as you'd like but expresses the constraints reasonably. It allows, for instance,
        a == [1..5]
        b == [1..120]
        c == Nat
which a more detailed interval analysis might point to. On the other hand, it dislikes
        a == [0..5]
        b == [1..120],
demanding b be widened to [0..120], basically because a does not get narrowed to [1..5] on the else branch, as it might. Way down the line this might be a fruitful extension to pursue.

Re:Nitpicks and comments

luqui on 2005-09-15T17:35:38

> Instead of
> d does e
> I get
> d does a
> b does e
> (from the call to fact).

That's right, good eye.

> 1 in a in Num
> 1 in b in Num
[...]
> which may not be as tight as you'd like but
> expresses the constraints reasonably. It allows,
> for instance,
> a == [1..5]

Actually it doesn't. "a in Num" means that a is a ring. If you say 4 + 3 (which are both in a here), you get 7, which is not in a, so a is not in Num.

What I'm currently stumpted on is if you say fact(3). The caller is supposed to provide the instances present in the constraints. But 3 is in Int, Float, Bigint, Z_4 (integers mod 4), etc. Which one do you pick? Also, what do you pick for your return value? Why would you have to provide the Eq[c] instance, when you don't even know what c represents.

But, upon looking at the constraints, this is all you can really infer without monotypes. So I'm hoping there's a way around it.