Types
Type Syntax
Type ::= Number | Shape |
Shape ::= ((FieldType^*) (MethodType^*)) |
FieldType ::= (FieldName Type) |
MethodType ::= (MethodName (Type^*) Type) |
Here Number is the literal word 'Number'.
Any two FieldNames in a Shape must be distinct. Any two MethodNamess in a Shape must also be distinct.
Example ( ((x Number) (y Number)) ((distanceO () Number)) ) would be the Shape type for a CartesianCoordinate class with two numeric fields (x and y) and a method named distanceO.
Types, the Model
TypedSystem ::= (TypedModule^* |
Import^* |
Declaration^* |
Statement^* |
Expression) |
|
TypedModule ::= (tmodule ModuleName Import^* Class Shape) |
Conventions
meta-variable
standing in for
Modules
a collection of modules
SClasses
Shapes of Classes, a mapping from ClassNames to Shapes
TVar
Types of Variables a mapping from Variabless to Types
T
any type
S
Shape type
Tf
the type of a field
Tm
the type of a method
sys
a system
mod
a module
imp
an import specification
cls
a class
meth
a method
Judgments
read judgment as
the formal judgment
a system is valid:
⊢ sys
a module is valid:
Modules ⊢ mod
a sequence of imports produces:
Modules ⊢ imp1 ... impI ⟹ SClasses
an import produces:
Modules, SClasses ⊢ (imp M) ⟹ SClasses [C : S]
Figure 14: Judgments for systems and modules in the Type language
read judgment as
the formal judgment
a class is valid:
SClasses ⊢ cls
a method is valid:
SClasses, TVar, ((Ta ...) Tr) ⊢ meth
Figure 15: Judgments for classes and methods in the Type language
read judgment as
the formal judgment
a program produces:
SClasses ⊢ def* stmt* exp ⟹ T
a block is valid:
SClasses ⊢ (block def* stmt*)
Figure 16: Judgments for bodies of blocks, systems, and methods in the Type language
read judgment as
the formal judgment
a sequence of declaration produces:
SClasses, TVar0 ⊢ def1 ... defd ⟹ TVar1
one declaration produces:
SClasses, TVar0 ⊢ (def x exp) ⟹ TVar0[x : T]
read judgment as
the formal judgment
a sequence of statements is valid:
SClasses, TVar ⊢ stmt1 ... stmtn
one statement is valid:
SClasses, TVar ⊢ stmt
Judgment Derivation Rules
∅ ⊢ mod1
for i from 2 to K:
{mod1, ..., modi-1} ⊢ modi
{mod1, ..., modK} ⊢ imp1 ... impI ⟹ SClasses
SClasses, ∅ ⊢ def* stmt* exp ⟹ Number
[system]
⊢ (mod1 ... modK imp1 ... impI def* stmt* exp)
Modules ⊢ imp1 ... impI ⟹ SClasses
SClasses [C : S] ⊢ (class C (f ...) (meth ...))
[module]
Modules ⊢ (tmodule MN imp1 ... impI (class C (f ...) (meth ...)) S)
SClasses0 = ∅
for i from 1 to I:
Modules, SClassesi-1 ⊢ impi ⟹ SClassesi
[imports]
Modules ⊢ imp1 ... impI ⟹ SClassesI
M is the name of mod in Modules
C is the name of the class defined in mod
S is the Shape of C in mod
[an import]
Modules, SClasses ⊢ (import M) ⟹ SClasses [C : S]
Figure 20: Typing rules for systems and modules in the Type language
SClasses[C] = S
S = (((f1T Tf1) ... (fgT Tfg)) ((m1T Tm1) ... (mkT Tmk)))
{f1, ..., fg} = {f1T, ... fgT}
{NameOf[methi], ..., NameOf[methk]} = {m1T, ..., mkT}
for all i:
SClasses, ∅ [this : S] , Tmj ⊢ methi , if NameOf[methi] is mj
[class]
SClasses ⊢ (class C (f1 ... fg) meth1 ... methk)
SClasses, TVar [y : Ta] , ... ⊢ def* stmt* exp ⟹ Tr
[method]
SClasses, TVar, ((Ta ...) Tr) ⊢ (method m (y ...) def* stmt* exp)
Simplification The fields in S must be specified in the same order as in C.
Figure 21: Typing rules for classes and methods in the Type language
Note the following modification: the judgment for blocks propagates a type-variable environment. The second modification fixes the same issue with the judgment for program and method bodies.
SClasses, TVar0 ⊢ def* ⟹ TVar1
SClasses, TVar1 ⊢ stmt*
SClasses, TVar1 ⊢ exp ⟹ T
[body]
SClasses, TVar0 ⊢ def* stmt* exp ⟹ T
SClasses, TVar0 ⊢ def* ⟹ TVar1
SClasses, TVar1 ⊢ stmt*
[block]
SClasses, TVar0 ⊢ (block def* stmt*)
Figure 22: Typing rules for bodies of blocks, systems, and methods in the Type language
for i from 1 to d:
SClasses, TVari-1 ⊢ (def xi expi) ⟹ TVari
[declarations]
SClasses, TVar0 ⊢ (def x1 exp1) ... (def xd expd) ⟹ TVar1
SClasses, TVar0 ⊢ exp ⟹ T
[one declaration]
SClasses, TVar0 ⊢ (def x exp) ⟹ TVar0[x : T]
Figure 23: Typing rules for declarations in the Type language
for all i
SClasses, TVar ⊢ stmti
[statements]
SClasses, TVar ⊢ stmt1 ... stmtn
TVar[x] = T
SClasses, TVar ⊢ exp ⟹ T
[assignment]
SClasses, TVar ⊢ x = exp
SClasses, TVar ⊢ tst ⟹ T
SClasses, TVar ⊢ thn
SClasses, TVar ⊢ els
[conditional]
SClasses, TVar ⊢ (if0 tst thn els)
SClasses, TVar ⊢ tst ⟹ T
SClasses, TVar ⊢ bdy
[loop]
SClasses, TVar ⊢ (while0 tst bdy)
SClasses, TVar ⊢ exp ⟹ T
TVar[o] = (((f1T Tf1) ... (fgT Tfg)) (Tm1T ... TmKT))
there exists an i such that f = fiT and Tfi = T
[field mutation]
SClasses, TVar ⊢ (o –> f = exp)
n is a literal number
[numerical literal]
SClasses, TVar ⊢ n ⟹ Number
TVar[x] = T
[variable]
SClasses, TVar ⊢ x ⟹ T
TVar[x] = Number, TVar[y] = Number
[+]
SClasses, TVar ⊢ (x + y) ⟹ Number
TVar[x] = Number, TVar[y] = Number
[/]
SClasses, TVar ⊢ (x / y) ⟹ Number
[==]
SClasses, TVar ⊢ (x == y) ⟹ Number
SClasses[C] = S
S = (((f1T Tf1) ... (fgT Tfg)) (Tm1T ... TmKT))
TVar[a1] = Tf1, ..., TVar[ag] = Tfg
[new]
SClasses, TVar ⊢ (new C (a1 ... ag)) ⟹ S
SClasses[C] = SC, TVar[o] = So
[isa]
SClasses, TVar ⊢ (o isa C) ⟹ Number
TVar[o] = (((f1T Tf1) ... (fgT Tfg)) (Tm1T ... TmKT))
there exists an i such that f = fiT
[get]
SClasses, TVar ⊢ (o –> f) ⟹ Tfi
TVar[o] = ((FT1T ... FT1T) ((m1T Tm1) ... (mkT Tmk)))
there exists an i such that m = mi
Tmi = ((T1 ... Tn) Tr)
TVar[a1] = T1, ..., TVar[an] = Tn
[call]
SClasses, TVar ⊢ (o –> m (a1 ... an)) ⟹ Tr
Figure 25: Typing rules for expressions in the Type language