Machine Problem 8
PPL Fall 2007

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 for DemeterF programs.
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:

ComplementTransform { 
    transform: PathSpec
    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 { 
    transform: PathSpec
    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.

On the Address translation we used:

AddrTrans {
  transform: Exp
  Addr apply(Var var, SymList senv);
}

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 {
  transform: Exp
  Ident apply(Var var, SymList senv);
}

because in an Exp it is not legal to put an Ident in place of a Var.

To define the typing rules, 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) or Y apply(X x, Z z).

Definition: (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.

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:

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.

In dir?? you have a partial implementation of your type checker.
Complete it, test it and turn it in.