-- []<>Users>sturgis.pa>cirio>typeNotes.tioga -- Sturgis, March 4, 1989 12:41:05 pm PST remark There is a folder amongst the Cirio stuff that contains assorted corrections to the contents of this note. They must be installed to move towards correctness. intro This is an attempt to justify the type conformance checking algorithm I am about to install in Cirio. The issue is to get REF INT, REF VariantRecord, REF ANY, REF REF INT, REF REF VariantRecord, and REF REF ANY to behave correctly. We use a fairly naive model of types. A type t defines a set of values. However, this set is dependent on the run-time state. If we let (One should remember that Cedar types contain more information than that contained in t and most of this other information.) Values can be divided into two broad classes: atomic and compound. Examples of atomic values are integers and pointers. Examples of compound values are records, arrays, and procedure descriptors. The atomic values can be further divided into pure and indirects. Integers and Booleans are pure. Pointers and REFs are indirects. In addition, handles held by Cirio on target world state are indirects. Given an indirect to a compound value, one can obtain an indirect to a component of the value. Given a type t, there is an associated type I(t). Informally, structures which must hold values of type t. That is, one would not be surprised if, in looking at such a data structure, one found a value of type t. Further, as time passes, one would expect to find different values, but all of type t. The purpose of this note is to address a particular subtlety. Let us introduce the binary, associative, commutative operation, that applies to types. We require that requires that Suppose that t = t1 The important fact is that, if the sequal that each If p values of On the other hand, if p values in This distinction is important in Cedar because the REF type constructor sometimes produces I(t) and sometimes produces I(t1) I(t2). Cedar Types We assume that a Cedar type can be described as a family of types: T = {t1, t2, ...}. Let set of values of this type. We define The intention is that when an indirect is formed, it will contain distinct indirect types for each of the types in the family. Cedar Type Constructors We consider three type constructors: Record, Indirect, and REF. We assume given the record type constructor for ordinary types: . For Cedar types we define by: = { | ti We define the indirect Cedar type I(T) by I(T) = { (We define REF later.) Assignment Safety We take the view that one always stores through an indirect. Thus, the assignment a _ exp is implemented by obtaining an indirect to the variable a, a value for the expression exp, and then storing the value through the indirect. Further r^ _ exp (where r is a REF) is implemented by obtaining the indirect contained in r, a value for the expression exp, and storing the value through the indirect. Now we come to the crucial point. Given the Cedar type of an indirect, the set of values which one may safely store through that indirect may be considerably smaller than the set of values that one might find when loading from it. Let T = {I(t1), I(t2), ...}. Then the set of values that one can safely store through an indirect of type T is contained in However, the set of values which one might load through such an indirect includes We define two type operators. LTarget(I) is intended to be the Cedar type of the values which may be safely stored through an indirect of Cedar type I, and RTarget(I) is intended to be the Cedar type of the values which might be obtained when loading from an indirect of Cedar type I. We define these operators for certain indirect types by RTarget(I(T)) = T if |T| > 1, then LTarget(I(T)) = { if |T| = 1, then LTarget(I(T)) = T. We can show that these definitions are suitable as follows. Suppose that u has been loaded thorough an indirect of Cedar type I(T), where T = {I(t1), I(t2), ...}. Then u case, the values u that are safe to store thorugh the indirect include contained in this set. On the other hand, if |T| > 1, then Conformance Let Conforms(t2, t1) be a previously defined primitive notion. In fact, let it mean For Cedar types, define Conforms(T2, T1) by Conforms( Observe that Conforms(T2, T1) is equivalent to Hence Conforms(T2, T1) <=> Conforms( <=> Further, we assume that Conforms satisfies: If Conforms(I(t1), I(t2)), then Conforms(t1, t2) and Conforms(t2, t1). [This follows from an argument that legal configurations must lead to legal configurations .... ???] [Is it even possible that it is a definition of Conforms(I(t1), I(t2))?] [Do Conforms(t1, t2) and Conforms(t2, t1) together imply Conforms(I(t1), I(t2))??] Given these definitions and assumptions, let us compute Conforms(I(T1), I(T2)). Conforms(I(T1), I(T2)) <=> Conforms({ <=> Conforms( <=> Conforms( We offer two special cases: (1) if both T1 and T2 are singletons (i.e., T1 = {t1} and T2 = {t2}), then this reduces to: <=> Conforms(I(t1), I(t2)) <=> Conforms(t1, t2) and Conforms(t2, t1) <=> Conforms(T1, T2) and Conforms(T2, T1) (2) if T1 => => Conforms( => Conforms(I(T1), I(T2)) Ref Target Types REF T is really a pointer to a record of two fields: , where CODE(T) is a type containing a single integer value, the type code for T. We define RTT(T) to be this record type. RTT stands for Ref Target Type. Variant Records We consider exactly one class of variant records. It contains the individual types VR, red VR, big red VR, small red VR, and blue VR. Some Cedar Types There is some confusion in the following between the ordinary type INT and the Cedar type INT. Perhaps I should fix that. INT = {INT} VR = {big red VR, small red VR, blue VR} red VR = {big red VR, small red VR} big red VR = {big red VR} RTT(INT) = {} RTT(VR) = {, , } RTT(red VR) = {, } RTT(big red VR) = {} RTT(ANY) = { | any Cedar type T} REF INT = I(RTT(INT)) = I({}) = {I()} REF VR = I(RTT(VR)) = {I( )} REF red VR = I(RTT(VR)) = {I() REF big red VR = I(RTT(big red VR)) ={I()} REF ANY = I(RTT(ANY)) = { REF REF INT = I(RTT(REF INT)) REF REF ANY = I(RTT(REF ANY)) Some assignments Given the above definitions we can consider the legality of some assignments. Remember that a _ exp is safe when Conforms(type(exp), LTarget(I(type(a)))) and r^ _ exp is safe when Conforms(type(exp), LTarget(type(r))). Assume the following declarations i: INT; ra: REF ANY; ri: REF INT; rvr: REF VR; rbrvr: REF big red VR; rra: REF REF ANY; rri: REF REF INT; ra^ _ i could be shown safe if Conforms(REF INT, LTarget(REF ANY)) <=> Conforms(REF INT, LTarget(I(RTT(ANY)))) <=> Conforms(REF INT, { is false (should I work it out?) ra _ ri is safe if Conforms(REF INT, LTarget(I(REF ANY))) <=> Conforms(REF INT, REF ANY) {because |REF ANY| = 1} <=> Conforms(I(RTT(INT)), I(RTT(ANY)) which follows from {} => RTT(INT) => Conforms(I(RTT(INT)), I(RTT(ANY)) rra _ rri could be shown safe if Conforms(REF REF INT, LTarget(I(REF REF ANY))) <=> Conforms(REF REF INT, REF REF ANY) {because |REF REF ANY| = 1} <=> Conforms(I(RTT(REF INT)), I(RTT(REF ANY))) <=> [Conforms(RTT(REF INT), RTT(REF ANY)) and Conforms(RTT(REF ANY), RTT(REF INT))] {because RTT(REF INT) and RTT(REF ANY) are both singletons} which requires at least Conforms(RTT(REF ANY), RTT(REF INT)) which requires at least Conforms(CODE(REF ANY), CODE(REF INT)) which fails.