A.12 Proposition

< Free Open Study >

Suppose that S V T = J and, for some U, that S <: U and T <: U. Then J <: U.
Suppose that S ∧ T = M and, for some L, that L <: S and L <: T. Then L <: M.

Proof: The two parts are proved together, by induction on the sizes of S and T (actually, induction on almost anything will do). Given S and T, we consider the two parts in turn.

For part (1), proceed by cases on the form of U. If U is Top, then we are done, since J <: Top no matter what J is. If U = Bool, then the inversion lemma (15.3.2) tells us that S and T must also be Bool, so J = Bool and we are finished. The other cases are more interesting.

If U = U₁→U₂, then, by the inversion lemma, S = S₁→S₂ and T = T₁→T₂, with U₁ <: S₁, U₁ <: T₁, S₂ <: U₂, and T₂ <: U₂. By the induction hypothesis, the meet M₁ of S₁ and T₁ lies above U₁, while the join J₂ of S₂ and T₂ lies below U₂. By S-ARROW, M₁→J₂ <: U₁→U₂.

If U is a record type, then, by the inversion lemma, so are S and T. Moreover, the labels of S and T are supersets of the labels of U, and the type of every field in U is a supertype of the corresponding fields in S and T. Thus, the join of S and T will contain at least the labels of U, and (by the induction hypothesis) the fields of the join will be subtypes of the corresponding fields of U. By S-RCD, J <: U.

For part (2), we again proceed by cases on the forms of S and T. If either is Top, then the meet is the other, and the result is immediate. The cases where S and T have different (non-Top) shapes cannot occur, as we saw in the proof of A.10. If both are Bool, then the result is again immediate. The remaining cases (S and T both arrows or both records) are more interesting.

If S = S₁→S₂ and T = T₁→T₂, then by the inversion lemma we must have L = L₁→L₂, with S₁ <: L₁, T₁ <: L₁, L₂ <: S₂, and L₂ <: T₂. By the induction hypothesis, the join J₁ of S₁ and T₁ lies below L₁, while the meet M₂ of S₂ and T₂ lies above L₂. By S-ARROW, L₁→L₂ <: J₁→M₂.
If S and T are record types, then, by the inversion lemma, so is L. Further-more, L must have all the labels of S and T (and perhaps more), and the corresponding fields must be in the subtype relation. Now, for each label m_l in the meet M of S and T, there are three possibilities. If m_l occurs in both S and T, then its type in M is the meet of its types in S and T, and the corresponding type in L is a subtype of the one in M by the induction hypothesis. On the other hand, if m_l occurs only in S, then the corresponding type in M is the same as in S, and we already know that the type in L is smaller. The case where m_l occurs only in T is similar.

16.3.3 Solution

The minimal type of this term is Top-the join of Bool and {}. However, the fact that this term is typable should probably be viewed as a weakness in our language, since it is hard to imagine that the programmer really intended to write this expression-after all, no operations can be performed on a value of type Top, so there is little point in computing it in the first place! There are two possible responses to this weakness. One is simply to remove Top from the system and make V a partial operation. The other is to keep Top, but make the typechecker generate a warning whenever it encounters a term whose minimal type is Top.

16.3.4 Solution

Handling Ref types is straightforward. We simply add one clause to the meet and join algorithms:

When we refine Ref with Source and Sink constructors, however, we encounter a major difficulty: the subtype relation no longer has joins (or meets)! For example, the types Ref{a:Nat,b:Bool} and Ref{a:Nat} are subtypes of both Source{a:Nat} and Sink{a:Nat,b:Bool}, but these types have no common lower bound.

There are various ways to address this difficulty. Perhaps the simplest is to add either Source or Sink, but not both, to the system. For many application domains, this will suffice. For example, for the refined implementation of classes in §18.12, we need just Source. In a concurrent language with channel types (§15.5), on the other hand, we might prefer to have just Sink, since this will give us the ability to define a server process and pass around just the "send capability" on its access channel (the receive capability is needed only by the server process itself).

With just Source types, the join algorithm remains complete when refined as follows (we also need the Ref clause from above; analogous clauses are added to the meet algorithm):

A different solution (suggested by Hennessy and Riely, 1998) is to refine the Ref type constructor so that, instead of one argument, it takes two: the elements of Ref S T are reference cells that can be used to store elements of type S and retrieve elements of type T. The new Ref is contravariant in its first parameter and covariant in its second. Now Sink S can be defined as an abbreviation for Ref S Top, and Source T can be defined as Ref Bot T.

16.4.1 Solution

Yes:

The alternative rule

is appealing, and would be safe (since Bot is empty, the evaluation of t₁ can never yield a regular result), but this rule would assign some types to terms that cannot be assigned by the declarative typing rules; choosing it would break Theorem 16.2.4.

17.3.1 Solution

The solution just requires transcribing the algorithms from Exercise 16.3.2.

   let rec join tyS tyT =     match (tyS,tyT) with     (TyArr(tyS1,tyS2),TyArr(tyT1,tyT2)) →       (try TyArr(meet tyS1 tyT1, join tyS2 tyT2)         with Not_found → TyTop)   | (TyBool,TyBool) →       TyBool   | (TyRecord(fS), TyRecord(fT)) →       let labelsS = List.map (fun (li,_) → li) fS in       let labelsT = List.map (fun (li,_) → li) fT in       let commonLabels =         List.find_all (fun l → List.mem l labelsT) labelsS in       let commonFields =         List.map (fun li →                     let tySi = List.assoc li fS in                     let tyTi = List.assoc li fT in                     (li, join tySi tyTi))                  commonLabels in       TyRecord(commonFields)   | _ →       TyTop and meet tyS tyT =   match (tyS,tyT) with     (TyArr(tyS1,tyS2),TyArr(tyT1,tyT2)) →       TyArr(join tyS1 tyT1, meet tyS2 tyT2)   | (TyBool,TyBool) →       TyBool   | (TyRecord(fS), TyRecord(fT)) →       let labelsS = List.map (fun (li,_) → li) fS in       let labelsT = List.map (fun (li,_) → li) fT in       let allLabels =         List.append           labelsS           (List.find_all             (fun l → not (List.mem l labelsS)) labelsT) in       let allFields =         List.map (fun li →                     if List.mem li allLabels then                       let tySi = List.assoc li fS in                       let tyTi = List.assoc li fT in                       (li, meet tySi tyTi)                     else if List.mem li labelsS then                       (li, List.assoc li fS)                     else                       (li, List.assoc li fT))                  allLabels in       TyRecord(allFields)   | _ →       raise Not_found let rec typeof ctx t =   match t with     ...   | TmTrue(fi) →       TyBool   | TmFalse(fi) →       TyBool   | TmIf(fi,t1,t2,t3) →       if subtype (typeof ctx t1) TyBool then         join (typeof ctx t2) (typeof ctx t3)       else error fi "guard of conditional not a boolean"

17.3.2 Solution

See the rcssubbot implementation.

18.6.1 Solution

   DecCounter = {get:Unit→Nat, inc:Unit→Unit, reset:Unit→Unit,                 dec:Unit→Unit};   decCounterClass =     λr:CounterRep.       let super = resetCounterClass r in         {get = super.get,          inc = super.inc,          reset = super.reset,          dec = λ_:Unit. r.x:=pred(!(r.x))};

18.7.1 Solution

   BackupCounter2 = {get:Unit→Nat, inc:Unit→Unit,                     reset:Unit→Unit, backup: Unit→Unit,                     reset2:Unit→Unit, backup2: Unit→Unit};   BackupCounterRep2 = {x: Ref Nat, b: Ref Nat, b2: Ref Nat};   backupCounterClass2 =     λr:BackupCounterRep2.       let super = backupCounterClass r in          {get = super.get, inc = super.inc,           reset = super.reset, backup = super.backup,           reset2 = λ_:Unit. r.x:=!(r.b2),           backup2 = λ_:Unit. r.b2:=!(r.x)};

18.11.1 Solution

   instrCounterClass =     λr:InstrCounterRep.        λself: Unit→InstrCounter.          λ_:Unit.            let super = setCounterClass r self unit in               {get = λ_:Unit. (r.a:=succ(!(r.a)); super.get unit),                set = λi:Nat. (r.a:=succ(!(r.a)); super.set i),                inc = super.inc,                accesses = λ_:Unit. !(r.a)};   ResetInstrCounter = {get:Unit→Nat, set:Nat→Unit,                        inc:Unit→Unit, accesses:Unit→Nat,                        reset:Unit→Unit};   resetInstrCounterClass =     λr:InstrCounterRep.        λself: Unit→ResetInstrCounter.          λ_:Unit.            let super = instrCounterClass r self unit in               {get = super.get,                set = super.set,                inc = super.inc,                accesses = super.accesses,                reset = λ_:Unit. r.x:=0};   BackupInstrCounter = {get:Unit→Nat, set:Nat→Unit,                         inc:Unit→Unit, accesses:Unit→Nat,                         backup:Unit→Unit, reset:Unit→Unit};   BackupInstrCounterRep = {x: Ref Nat, a: Ref Nat, b: Ref Nat};   backupInstrCounterClass =     λr:BackupInstrCounterRep.        λself: Unit→BackupInstrCounter.          λ_:Unit.            let super = resetInstrCounterClass r self unit in              {get = super.get,               set = super.set,               inc = super.inc,               accesses = super.accesses,               reset = λ_:Unit. r.x:=!(r.b),               backup = λ_:Unit. r.b:=!(r.x)};   newBackupInstrCounter =     λ_:Unit. let r = {x=ref 1, a=ref 0, b=ref 0} in                 fix (backupInstrCounterClass r) unit;

18.13.1 Solution

One way to test for identity is using reference cells. We extend the internal representation of our objects with an instance variable id of type Ref Nat

   IdCounterRep = {x: Ref Nat, id: Ref (Ref Nat)};

and an id method that just returns the id field:

   IdCounter = {get:Unit→Nat, inc:Unit→Unit, id:Unit→(Ref Nat)};   idCounterClass =     λr:IdCounterRep.       {get = λ_:Unit. !(r.x),        inc = λ_:Unit. r.x:=succ(!(r.x)),        id  = λ_:Unit. !(r.id)};

Now, the sameObject function takes two objects with id methods and checks whether the references returned by the id methods are the same.

   sameObject =     λa:{id:Unit→(Ref Nat)}. λb:{id:Unit→(Ref Nat)}.       ((b.id unit) := 1;       (a.id unit) := 0;       iszero (!(b.id unit)));

The trick here is using aliasing to test whether two reference cells are the same: we make sure the second is non-zero, assign zero to the first, and test the second to see whether it has become zero.

19.4.1 Solution

Since every class declaration must include an extends clause, and since these clauses are not allowed to be cyclic, the chain of extends clauses from every class must eventually end with Object.

19.4.2 Solution

One obvious improvements would be to combine the three typing rules for casting into one

and drop the concept of stupid casts. Another would be to omit constructors, since they do nothing anyway.

19.4.6 Solution

The formulation of interfaces for FJ is routine.
Suppose we declare the following interfaces:
```
   interface A {}   interface B {}   interface C extends A,B {}   interface D extends A,B {} 
```
Then C and D have both A and B as common upper bounds, but no least upper bound.
Instead of the standard algorithmic rule for conditional expressions,

Java uses the following restricted rules:

These are intuitively sound, but they interact poorly with the small-step style of operational semantics used for FJ-the type preservation property is actually false! (It is easy to construct an example that shows this.)

19.4.7 Solution

Surprisingly, handling super is harder than handling self, since we need some way of remembering what class the "currently executing method body" came from. There are at least two ways to accomplish this:

Annotate terms with some indication of where super references should be looked up.
Add a preprocessing step in which the whole class table is rewritten, transforming references to super into references to this with "mangled" names indicating which class they come from.

19.5.1 Solution

Before giving the main proof, we develop some required lemmas. As always, the critical one (A.14) relates typing and substitution.

< Free Open Study >