A Cool programozási nyelv

Típusok

Típusok

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 kulcsszó

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.

 

Típusellenőrzés

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.

Típus környezetek

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 <- 33 in ... end;

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) =

T

O(d)

ha d=c

különben

Típusellenőrzési szabályok

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 e
1 : T'
T >= 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' =

SELF_TYPEC

T

ha T = SELF_TYPE

különben

___________________________________________
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
...
O, M, C en : T
n

T0' =

C

T0

ha T0 = SELF_TYPEC

különben

M(T0', f) = (T1', ..., Tn', Tn+1')
T
i' >= Ti ahol n >= i >= 1

Tn+1 =

T0

Tn+1'

ha Tn+1' = SELF_TYPE

különben

_______________________________
O, M, C e0.f(e1...en) : Tn+1

 

O, M, C e0 : T0
...
O, M, C en : T
n
T >= T
0
M(T, f) = (T
1', ..., Tn', Tn+1')
T
i' >= Ti ahol n >= i >= 1

Tn+1 =

T0

Tn+1'

ha Tn+1' = SELF_TYPE

különben

_______________________________
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 e
2 : T2
O, M, C e
3 : T3

______________________________________
O, M, C if e
1 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 en : T
n

______________________________________
O, M, C begin e1 ... e
n end : Tn

A let típusellenőrzési szabálya:

T0' =

SELF_TYPEC

T0

ha T0 = SELF_TYPE

különben

O, M, C e1 : T1
T
0' >= T1
O[T
0'/x], M, C e2 : T2

______________________________________
O, M, C let x : T
0 <- 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.

T0' =

SELF_TYPEC

T0

ha T0 = SELF_TYPE

különben

O[T0'/x], M, C e1 : T1

______________________________________
O, M, C let x : T
0 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[T
1/x1], M, C e1 : T1'
...
O[T
n/xn], M, C en : Tn'

________________________________________________________________
O, M, C case e
0 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 e
2 : T2

________________________
O, M, C while e
1 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 e
2 : Int
op{ <, <= }

________________________
O, M, C e
1 op e2 : Bool


O, M, C e : Int
________________________
O, M, C ~e : Int

O, M, C e1 : Int
O, M, C e
2 : Int
op { *, +, -, / }

________________________
O, M, C e
1 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 e
2 : T2
T
1 { Int, String, Bool } v T2 { Int, String, Bool } T1 = T2

_______________________________________________________
O, M, C e
1 = 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) =

SELF_TYPEC

T

ha T = SELF_TYPE

különben

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
O
C[SELF_TYPEC/self], M, C e1 : T1
T
0 >= T1

__________________________________
O
C, M, C x : T0 <- e1;


O
C(x) = T
_________________
O
C, 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)
O
C[SELF_TYPEC / self][T1/x1]...[Tn/xn], M, C e : T0'

T0' <=

SELF_TYPEC

T0

ha T0 = SELF_TYPE

különben

_____________________________________________
O
C, M, C f(x1 : T1, ..., xn : Tn) : T0 is e end;