[Grace-core] Type checking dialect

Timothy Jones tim at ecs.vuw.ac.nz
Tue Dec 3 02:46:44 PST 2013


The structural type checking dialect is now live on Github, and an updated
version that supports declarative types and methods is on my branch, which I
imagine Michael will merge once he gets this email.  The checking is actually
composed of two dialects: a dialect for writing a type checker, and the checker
itself.

The "checking" dialect provides two conveniences: a visitor pattern based on
matching, and scope management.  It also makes available a 'typeOf' method,
which either calculates the type of a node in the AST from the rules you've
defined, or retrieves it from the cache if it's already worked it out.  So for
the type of a block literal, we write something like this:

rule { block : BlockLiteral ->
    scope.enter {
        for(block.parameters) do { param ->
            scope.variables.at(param.name) put(param.dtype)
        }

        typeOf(block.body.last)
    }
}

The scope manages variable, method, and type scopes.

The "structural" dialect contains the rules, plus a bunch of classes for
constructing types of expressions and methods.  It's capable of dealing with
interactions with dynamic types, as well as more complicated things such as
method subtyping.

The main issue it has at the moment is that it doesn't know the type of the
prelude.  It has most of the standard types and values available, but if it
can't resolve the location of a variable or method it gives up and assumes it's
in the prelude, giving it the type Dynamic.  This is also a problem for imports.
Resolving this might involve having to tidy up the xmodule code that makes the
types of other modules available.

There's also not a particularly good test suite for it, so fire away and see if
you can break it.  I'll work on this at some point but it's not an immediate
priority for me.

-- 
Tim


More information about the Grace-core mailing list