Podtipi in objekti

Spoznali smo že polimorfizem, to je lastnost, da ima lahko izraz več kot en tip. Na primer, v OCamlu ima preslikava

fun (x, y) -> (y, x)

tip α × β → β × α, kjer sta α in β poljubna tipa. Danes bomo spoznali podtipe, ki delujejo podobno: če ima izraz e tip t, ga lahko uporabljamo, kot da bi imel tudi vse nadtipe tipa t.

Na primer, v nekaterih programskih jezikih lahko izraz e tipa int vedno uporabimo, kot da bi ime tip float, saj bo jezik samo pretvoril e.

V Javi poznamo podrazrede, ki so tudi vrsta podtipov, a jih bomo obravnavali prihodnjič.

Relacija podtip `A ≤ B`

Najprej se dogovorimo za zapis relacije “podtip”. Za tipa A in B zapis

A ≤ B

preberemo “A je podtip B” ali “B je nadtip A”. Sledimo naslednjemu osnovnemu načelu:

A je podtip B, če lahko vrednosti tipa A uporabljamo, kot da bi imele tip B.

S pravilom sklepanja to zapišemo takole:

e : A    A ≤ B
--------------
    e : B

in preberemo: “Če ima e tip A in je A podtip B, potem ima e tudi tip B”

Pozor: zmotno bi si bilo predstavljati, da je A ≤ B isto kot A ⊆ B, se pravi, da je podtip ista reč kot množica. V razdelku o podtipih zapisov bomo namreč spoznali podtipe, ki se razlikujejo od relacije podmnožica.

Kaj pričakujemo od relacije podtip? Zapišimo pravila. Vsekakor je relacija refleksivna in tranzitivna:

-----
A ≤ A


A ≤ B    B ≤ C
--------------
    A ≤ C

Morda velja antisimetričnost: če A ≤ B in B ≤ A, potem A = B? Ne, kasneje bomo videli protiprimer.

Nadalje zapišemo še pravila, ki opredeljujejo, kako se obnašajo podtipi za razne operacije na tipih. Kartezični produkti delujejo po pričakovanjih:

A₁ ≤ B₁         A₂ ≤ B₂
-----------------------
   A₁ × A₂ ≤ B₁ × B₂

Pravilo za funkcijske tipe je bolj zanimivo, pozorno ga preberite:

B₁ ≤ A₁         A₂ ≤ B₂
-----------------------
   A₁ → A₂ ≤ B₁ → B₂

Obrnili smo vrsti red v domeni! Pravimo, da je → kontravarianten (obrača smer) v prvem argumentu in kovarianten (ohranja smer) v drugem. Skupaj premislimo, zakaj pričakujemo tako pravilo.

Kaj pa osnovni tipi? Ali je na primer int ≤ float? To je odvisno od programskega jezika: Java samodejno pretvori celo število v realno, zato bi lahko rekli, da v javi velja int ≤ float. V OCamlu to ne drži, saj mora programer sam pretvoriti celoštevilsko vrednost v realno s funkcijo float.

Lahko se celo zgodi, da v programskem jeziku velja int ≤ float in hkrati float ≤ int, na primer, če jezik samodejno zaokroži realno vrednost, kadar potrebuje celoštevilsko. A takih jezikov in veliko.

Podtipi zapisov

Spoznali smo že zapise, to so nabori polj s poimenovanimi komponentami. Na primer, točke v ravnini lahko predstavimo z vrednostmi tipa zapisov

{ x : float; y : float }

Primer vrednosti tega tipa je zapis {x = 3.14; y = 2.78}.

V splošnem je tip zapisa

{ ℓ₁ : A₁; ℓ₂ : A₂; …; ℓ_n : A_n }

njegove vrednosti pa so oblike

{ ℓ₁ = e₁; ℓ₂ = e₂; …; ℓ_n = e_n }

kjer mora veljati eᵢ : Aᵢ. Zahtevamo še, da so imena polj ℓ₁, …, ℓ_n med seboj paroma različna.

Če je v zapis tipa { ℓ₁ : A₁; ℓ₂ : A₂; …; ℓ_n : A_n }, potem je v.ℓᵢ vrednost njegove i-te komponente, ki ima tip Aᵢ.

V zapisu vrstni red polj ni pomemben, to je, {x = 3.14; y = 2.78} = {y = 2.78; x = 3.14}.

Zapisi so uporaben podatkovni tip, ne samo v programiranju, ampak tudi na drugih področjih računalništva, kjer želimo predstviti strukturirane podatke. Na primer, vrstica v tabeli podatkovne baze ni nič drugega kot zapis (in shema za tabelo tip zapisa).

Tudi objekti nas nekoliko spominjajo na zapise, le da vsebujejo poleg polj (atributov) še metode:

public class Point {
   float x;
   float y

   ...
}

Zapisi tipov imajo zanimivo relacijo ≤.

Obravnavajmo primer. Na primer, da imamo tipa zapisov

A := { x : float; y : float }

B := { x : float; y : float ; z : float }

Ali morda velja A ≤ B ali B ≤ A?

Najprej, A ≤ B ne velja. Izraz a = {x = 3.14; y = 2.78} ima tip A. Če bi ga lahko uporabljali, kot da ima tip B, potem bi smeli pisati a.z, kar seveda ne gre.

Velja pa B ≤ A! Izraz b = {x = 3.14; y = 2.78; z = 1.0} ima tip B in res ga lahko uporabimo, kot da bi imel tip A, saj smemo pisati b.x in b.y. Dejstvo, da b vsebuje še polje z nas pri tem nič ne moti.

Zapišimo pravilo za podtipe zapisov, ki izhaja iz zgornjega razmisleka:

     za vsak j ≤ m obstaja i ≤ n, da je ℓᵢ = kⱼ in Aᵢ = Bⱼ
   -----------------------------------------------------
   { ℓ₁ : A₁; …; ℓ_n : A_n } ≤ { k₁ : B₁; …; k_m : B_m }

Povedano z besedami, prvi tip zapisa je podtip drugega, če se vsako polje kⱼ : Bⱼ iz drugega zapisa pojavi v prvem. Tej vrsti podtipov pravimo podtip zapisa po širini, ker je podtip “širši” (ima več polj) kot njegov podtip.

Velja torej:

{ z : float; x : float; y : float } ≤ { x : float; y : float }

Vaja: ali obstaja tip zapisa, ki je podtip vseh ostalih tipov zapisov? Kaj pa tip zapisa, ki je nadtip vseh ostalih tipov zapisov?

Poznamo še eno podtip zapisa v globino. Spet poglejmo primer, pri čemer predpostavimo, da velja int ≤ float. Zapis

v = { x = 3; y = 5 }

ima tip {x : int; y : int}. Ali ga lahko uporabljamo, kot da bi imel tudi tip {x : float; y : float}? Da, saj lahko njegovi komponenti v.x in v.y uporabljamo, kot da bi imeli tip float, zahvaljujoč int ≤ float.

Pravilo, za podtipe zapisov v globino se glasi:

          A₁ ≤ B₁     A₂ ≤ B₂    ⋯    A_n ≤ B_n
----------------------------------------------------------
   { ℓ₁ : A₁; …; ℓ_n : A_n } ≤ { ℓ₁ : B₁; …; ℓ_n : B_n }

Obe pravili, za širino in globino, lahko združimo v eno kombinirano pravilo:

     za vsak j ≤ m obstaja i ≤ n, da je ℓᵢ = kⱼ in Aᵢ ≤ Bⱼ
   -----------------------------------------------------
   { ℓ₁ : A₁; …; ℓ_n : A_n } ≤ { k₁ : B₁; …; k_m : B_m }

Zapisi s spremenljivimi polji

Katera pravila za podtipe zapisov pridejo v poštev, je odvisno od tega, kako lahko zapise uporabljamo. Denimo, če imamo zapise s spremenljivimi polji, se pravi, da lahko zapisu spremenjamo vrednosti polj, potem podtipi v globino niso več veljavni. Na primer, če imamo tipa

A = { mutable x : int; mutable y : int}

B = { mutable x : float; mutable x : float}

potem ne velja A ≤ B. Če bi to veljalo, bi lahko v zapis v : A vrednost polja x nastavili na 3.14. Zapišimo tip A še v OCamlu:

type a = { mutable x : int; mutable y : int}

Takole naredimo vrednost in ji nastavimo atribut:

# let p = {x = 10; y = 20} ;;
val p : a = {x = 10; y = 20}
# p.x <- 42 ;;
- : unit = ()
# p ;;
- : a = {x = 42; y = 20}

Problem koherentnosti

Težave nastopijo, če lahko vrednosti tipa A pretvorimo v nadtip B na več načinov, se pravi, če imamo

A ≤ B
A ≤ C
B ≤ D
C ≤ D

Zaradi tranzitivnosti sledi A ≤ D, kar lahko izpeljemo na dva načina:

A ≤ B ≤ D
A ≤ C ≤ D

To pa lahko vpliva na implicitne pretvorbe. Če imamo e : A, ga lahko pretvorimo v D preko pretvorb A → B → D ali preko A → C → D. Kako vemo, da bomo obakrat dobili isto? Temu pravimo problem koherentnosti. Pojavi se vedno, ko imamo implicitna (ali samodejne) pretvorbe vrednosti iz enega tipa v drugega.

Podtipi na nivoju struktur