Slash Boxes
NOTE: use Perl; is on undef hiatus. You can read content, but you can't post it. More info will be forthcoming forthcomingly.

All the Perl that's Practical to Extract and Report

use Perl Log In

Log In

[ Create a new account ]

Journal of luqui (5770)

Wednesday September 14, 2005
09:46 PM

Type equation inference

[ #26728 ]

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.

The Fine Print: The following comments are owned by whoever posted them. We are not responsible for them in any way.
More | Login | Reply
Loading... please wait.
  • Instead of
            d does e
    I get
            d does a
            b does e
    (from the call to fact).

            a == d
            b == e
            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 reasonab
    • > 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 stu