A Cool nyelvben az osztálynevek típusok. Egy különeges típus, a SELF_TYPE,
csak speciális esetben használható.
A típus deklaráció
<változó> : <típus>
alakú. A típust minden új változónál meg kell adni.
A SELF_TYPE a self változó típusát adja meg. Ez olyan osztályokban használható, amelyeket később tovább származtatunk, segítségével a dinamikus típusra hivatkozhatunk. Például a
class Silly is
copy() : SELF_TYPE is
self end;
end;
class Sally inherits Silly is end;
class Main is
x : Sally <- (new Sally).copy();
main() : Sally is x end;
end;
programban a (new Sally).copy() utasítás típusa
Sally, vagyis a deklaráció helyes.
A SELF_TYPE jelentése nincsen rögzítve, mindig azon múlik, hogy éppen melyik
osztályban használjuk. általában a SELF_TYPE arra a C osztályra
hivatkozik melyben előfordul vagy egy másik olyan
osztályra ami illeszkedik C-hez. Ahol szükség van arra, hogy ki tudjuk fejezni mire hivatkozhat a SELF_TYPE indexként odaírjuk az
osztály nevét is melyben a SELF_TYPE előfordul: SELF_TYPEC.
Hogyha egy metódus A típusú változót vár, akkor bármilyen B típusú értéket
használhatunk helyette feltéve hogy az
osztályhierarchiában a B az A-nak leszármazottja.
Arra az esetre, hogyha egy A típusú változó helyett B
típusút használhatunk bevezetve az alábbi jelölést:
B >= A
az alábbi szabályok érvényesek bármely A, B és C típusok esetén:
Mivel az Object őse minden osztálynak, bármelyik A osztályra teljesül Object >= A
Teljesül még a SELF_TYPE-pal kapcsolatos alábbi két szabály is:
SELF_TYPEX >= SELF_TYPEX bármilyen X típus esetén
B >= SELF_TYPEC hogyha B >= C
A Cool típusrendszere garantálja, hogy ne léphessen fel futásidejű
típushiba. A típusellenőrzés során a fordító meghatározza minden kifejezésnek a
pontos típusát. Fontos megkülönböztetni a fordító által meghatározott típusát
egy objektumnak (a statikus típust) és a valódi típusát a futás során (a
dinamikus típust) ami az öröklődés miatt eltérhet a statikus típustól. Amit
elvárunk az az, hogy (a fenti jelöléseknél maradva)
statikus típus >= dinamikus típus
A fordító nem fogad el olyan programot amiben nem
felel meg minden objektum típusa tökéletesen az elvárásoknak, ami miatt esetleg
olyan programokat is visszadobhat, amik futásidejű hiba nélkül lefutnának.
A típusellenőrzést tekinthetjük egy lentről-felfelé haladó algoritmusnak: egy kifejezés típusát a részkifejezéseinek típusai alapján lehet kiszámolni. Például egy 2 egész számnak a típusa Int, és ebben az esetben nincsenek részkifejezések. Egy másik példa: hogyha a k kifejezés típusa K, akkor a begin a; b; c; d; e; f; g; h; i; j; k; end kifejezésnek szintén K lesz a típusa. Amikor egy objektum azonosítójának a típusát kell meghatározni problémák lépnek fel, mert ezt az alapján lehet megmondani, hogy milyen típust határozott meg a programozó a kifejezésünket befoglaló kifejezésben. Ennek a problémának a kiküszöbölésére használjuk a típus környezeteket. Egy környezet három részből áll: egy M metódus környezetből, egy O objektum környezetből és az aktuális osztályból ami a kifejezést tartalmazza. A metódus környezet és az objektum környezet egyaránt egy-egy függvény. Az objektum környezet egy
O(v) = T
ami hozzárendeli a T típust a v objektum azonosítóhoz. A metódus környezet sokkal összetettebb:
M(C, f) = (T1, ..., Tn)
C egy osztály neve (egy típus), f egy metódus neve, a T1, ..., Tn pedig típusok. Ez annyit jelent, hogy a C osztályban az f metódusnak T1...Tn-1 formális paramétere van és a visszatérési értékének típusa Tn. A típus környezet harmadik eleme az aktuális osztály típusa amire a SELF_TYPE-al való számoláshoz van szükség. Minden kifejezés típusellenőrzése egy típuskörnyezetben történik. A részkifejezéseinek ellenőrzése vagy ugyanabban a környezetben, vagy (ha a kifejezés bevezet egy új objektum azonosítót) egy módosított környezetben. Például:
let c : Int <-
a let kifejezés létrehoz egy Int típusú új változót, ezért az in és az end közötti részkifejezést egy módosított környezetben ellenőrzi a fordító. Ha a let kifejezés típus környezetének objektum környezet komponense O, a belső kifejezés környezete
O[Int/c]
ahol az O[Int/c] értelmezése:
O[Int/c](d) = |
|
|
Egy típusellenőrzési szabály általános formája:
.
.
.
___________________
O, M, C e : T
ami annyit jelent, hogy egy olyan
típuskörnyezetben, melynek objektum környezete O, metódus környezet M,
befoglaló osztálya pedig C, az e kifejezésnek T lesz a
típusa. A pontok a vízszintes vonal felett azt jelölik, hogy lehetnek még
további állítások az e részkifejezéseinek típusairól. Ezek a további
kifejezések a szabály feltételei. Hogyha a feltételek teljesülnek, a vonal
alatti állítás igaz.
Az objektum azonosítókra vonatkozó szabály egyszerűen
annyi, hogy ha a környezet az Id azonosítóhoz hozzárendeli a T
típust, akkor az Id típusa T:
O(Id)=T
___________________
O, M, C Id : T
Az értékadásra vonatkozó szabály sokkal összetettebb:
O(Id) = T |
______________________
O, M, C Id <- e1 : T
A szabály azt mondja ki, hogy az értékül adott e1 kifejezésnek T' típusa kell legyen, aminek illeszkedni kell az Id T
típusához a típuskörnyezetben. Az egész kifejezés típusa T' lesz.
A konstansokra vonatkozó szabályok nagyon egyszerűek:
_____________________
O, M, C true : Bool
_____________________
O, M, C false : Bool
i egy egész szám
_____________________
O, M, C i : Int
s egy string konstans
_____________________
O, M, C s : String
Két eset van a new és egy a new SELF_TYPE számára, és egy az összes többi esethez:
T' = |
|
|
___________________________________________
O, M, C new T : T'
A metódushívás a legbonyolultabb része a típusellenőrzésnek:
O, M, C e0 : T0
M(T0', f) = (T1',
..., Tn', Tn+1')
|
_______________________________
O, M, C e0.f(e1...en) : Tn+1
O, M, C e0 : T0
|
_______________________________
O, M, C e0@T.f(e1...en) : Tn+1
Egy metódushívás típusának meghatározásához az összes részkifejezés típusát
meg kell határozni. T0 (e0 típusa) határozza meg, hogy f-nek
melyik deklarációját kell nézni. A kifejezésben szereplő argumentumok típusának
illeszkedni kell a deklarációban szereplő típusokhoz. A metódushívás típusa az f deklarációjában megadott típus, vagy T0 amennyiben a deklarációban megadott típus
SELF_TYPE. A második esetben annyi a különbség, hogy meghatároz egy T
típust az e0 számára, mely T
típusnak illeszkednie kell a T0
típushoz.
A típusellenőrzési szabály az if-hez:
O, M, C e1 : Bool |
______________________________________
O, M, C if e1 then
e2 else e3 fi : T2 T3
A begin-end-re vonatkozó típusellenőrzés szabályok:
O, M, C e1 : T1 |
______________________________________
O, M, C begin e1
... en end
: Tn
A let típusellenőrzési szabálya:
O, M, C e1 : T1 |
______________________________________
O, M, C let x : T0 <- e1
in e2 end : T2
Először végrehajtjuk az e1 típusellenőrzését az egész kifejezés típus környezetében melyben nem szerepel az x. Ugyanis az x-et nem lehet az e1-ben használni, hacsak nincsen az egész kifejezésen kívül is definiálva. Utána a let törzsén, az e2-n is végrehajtjuk a típusellenőrzést egy módosított környezetben: az O-hoz hozzávesszük még az x : T0'-t. Az x típusa lehet SELF_TYPE is.
O[T0'/x], M, C e1 : T1 |
______________________________________
O, M, C let x : T0 in e1
end : T1
Egy inicializálás nélküli let esetén egyszerűen kihagyhatjuk az értékül adott kifejezéssel szemben támasztott illeszkedési elvárást. Egy többszörös let:
let x1 : T1 [<- e1], x2 : T2 [<- e2], ..., xn : Tn [<- en] in e end
ugyanazt jelenti, mint az alábbi:
let x1 : T1 [<- e1] in ( let x2 : T2 [<- e2], ..., xn : Tn [<- en] in e end) end
Egy case kifejezés típusellenőrzése:
O, M, C e0 : T0 |
________________________________________________________________
O, M, C case e0 of
x1 : T1 => e1;
...; xn : Tn => en;
esac : T1' ... Tn'
A case minden ágának ellenőrzésre kerül a típusa egy-egy olyan környezetben
ahol xi : Ti-vel kibővül az egyes ágak objektum környezete.
A teljes case kifejezés típusa az ágai típusainak a legközelebbi közös őse. A
case ágain szereplő xi-knek mindnek
különböző típusa kell legyen.
A ciklusok típusellenőrzésére vonatkozó szabály a következő:
O, M, C e1 : Bool |
________________________
O, M, C while e1
loop e2 pool :
Object
A ciklus feltételének típusa Bool kell hogy legyen. Az egész loop típusa mindig Object. Egy isvoid teszt típusa mindig Bool:
O, M, C e
: T
________________________
O, M, C isvoid e : Bool
Az egyenlőségvizsgálat kivételével az egyszerű logikai, összehasonlító és aritmetikai műveletekre vonatkozó típusellenőrzési szabályok nem túl bonyolultak:
O, M, C e : Bool
________________________
O, M, C not e : Bool
O, M, C e1 : Int |
________________________
O, M, C e1 op e2 : Bool
O, M, C e : Int
________________________
O, M, C ~e : Int
O, M, C e1 : Int |
________________________
O, M, C e1 op e2 : Int
Az egyenlőség vizsgálat bármilyen két típusú objektum között megengedett, kivéve az Int, String és Bool típusúakat, melyeket csak azonos típusú objektumokkal lehet összehasonlítani.
O, M, C e1 : T1 |
_______________________________________________________
O, M, C e1 = e2 : Bool
Az utolsó esetei a típusellenőrzésnek az attribútumok és a metódusok. Egy C objektum környezetét jelöljük OC-vel, mely megadja C összes attribútumának típusát (beleértve az öröklött attribútumokat is). Formálisabban leírva: hogyha x C-nek egy attribútuma (öröklött vagy nem öröklött), és x deklarációja x : T akkor
OC(x) = |
|
|
Az M metóduskörnyezet globális az egész programban és minden osztály számára
definiálja az összes metódusának szignatúráját (beleértve az öröklött
metódusokat is).
Az attribútumok ellenőrzésére vonatkozó két szabály hasonlít a let-re vonatkozó
szabályokra. A lényeges különbség hogy az attribútumok láthatók már az őket
inicializáló kifejezésben.
OC(x)
= T0 |
__________________________________
OC, M, C x : T0 <- e1;
OC(x) = T
_________________
OC, M, C x : T;
A metódusok típusellenőrzésére vonatkozó szabály ellenőrzi a metódus törzsét egy olyan környezetben ahol az OC-t kibővíti a formális paraméterekkel és a self-el. A metódus törzsének típusának illeszkednie kell a metódus visszatérési értékének típusához.
M(C, f) = (T1,
..., Tn, T0)
|
_____________________________________________
OC, M, C f(x1 : T1,
..., xn : Tn) : T0
is e end;