Out: November 20, 2007
Due: November 29, 2007 (note: due Thursday)
Prepared in collaboration with Bryan Chadwick who implemented the type-checker. Please use the new DemeterF package prepared by Bryan: /home/chadwick/www/demeterf/newpackage.jar for this machine problem.
You have implemented many small educational languages in this course. Now is the time to implement a type-checker for something we actively use: the structure-shy tool which we call DemeterF. We focus on type-checking apply methods in DemeterF with respect to a class graph. And of course, we use DemeterF to implement the type checker.
This is a second machine problem about type-checking. Here the type checker will have access to data type definitions and will verify that method signatures are type-correct with respect to the type definitions. We ignore the body of the methods.
You have written several DemeterF programs but so far we did not have a static type-checker. We had a dynamic type checker only. In this machine problem you write program that solves a simple case of the type-checking problem for DemeterF programs. We call it the transformer type-checker.
In machine problem 6 we used something like:
ComplementTransform {
Complement apply(Merge m);
Complement apply(Join j);
}
to transform PathSpec objects.
This is type-correct because it is ok to insert, within a PathSpec, a Complement where there was a Merge or a Join. Our class dictionary for PathSpec explicitly allows for this. A transformation that uses the following signatures:
ComplementTransform {
Node apply(Merge m);
Ident apply(Join j);
}
is not type-correct because in the class graph
for a PathSpec, it is not permitted to replace
a Merge by a Node and it is not permitted
to replace a Join by an Ident.
In the address translation we used:
AddrTrans {
Addr apply(Var var);
}
This is type-correct because in the context
of an expression Exp it is permitted to replace
a Var by and Addr.
Recall the cd fragment:
Var : Sym | Addr. Addr = Integer.It would be illegal to use:
AddrTrans {
Ident apply(Var var);
}
because in an Exp it is not legal to put an Ident in place of a Var.
To define the typing rule, we use the notion of when a transformation X->Y is valid for a class graph G. A transformation X->Y corresponds to an apply method: Y apply(X x).
Definition: (will be used as typing rule at the object graph level) For a class graph G a transform X->Y is valid if for all og in Objects(G) and all replacements of an X-object in og by a Y-object we obtain an object in Objects(G). For definition of class graph G, Objects(G): see the paper with Mitch Wand from an earlier lecture. http://www.ccs.neu.edu/home/lieber/courses/csg111/f07/lectures-distribute/oct16/coreOfAP.pdf
The definition of validity is given in terms of objects and is not easily translated into an implementation. Fortunately, we can provide an equivalent definition entirely in terms of class graphs and this leads to an implementation in DemeterF.
This is an interesting self-application where we use DemeterF to improve DemeterF. This is a beneficial situation: should we improve the efficiency of our DemeterF implementation, it will also make our type checker run faster. Self-application is common in language development efforts. Examples are: a compiler that can compile itself. Or a grammar that defines its own syntax.
To prepare for your type checker implementation, you need to understand how to use data types to define data types. Study the class dictionary in: self-describing data types. Why is it only "almost" self-describing? How could you make it self-describing?
The following theorem and definition will help with your implementation: It lifts the type-checking problem to the class graph level.
Theorem: (also typing rule at class graph level)` For a class graph G a transform X->Y is valid iff for all construction edges -> *,*,S for some class S that is a superclass of X (X <= S), Y is a subclass of S (Y <= S).
(what is excluded: transformations X->Y so that there is no S: X <= S and Y <= S.)
Definition: For a class graph G a transform X->Y is type correct if it is valid.
We write A <= B if A is a subclass of B. <= is a reflexive and transitive relation. <= is the reflexive, transitive closure defined by the ":" relation:
S: T_1 | ... | T_n defines T_i <= S.
Implementation, about 20 lines of Java code, without documentation, based on the code provided in partial type checker. Complete it, test it and turn it in. The code provided implements a function to compute the superclass of a given class. The supertype computation uses all three kinds of helpers: an apply method (transformer), combine methods (builder) and an update method (augmentor). The apply method is used for the "leafs" and sends up a non-empty String if we found a type name we are looking for. The augmentor is used to have access to the enclosing object and the combine methods send up the supertype. Files extra/SuperType.java and program.beh contain the details. You only need to change file extra/MethodCheck.java.
To implement a transformer type-checker we need to make
a class graph available as an object. Therefore we need
a class graph for class graphs.
Once you have a class graph represented as an object
you need now to implement the following:
Identify all uses of a superclass of X on the right-hand-side
of a construction edge of G. For each such superclass S, check
that Y is a subclass of S.
Last modified: Tue Mar 27 16:48:19 EDT 2007