U L i k o o L matemaatika-informaatikateaduskond

on k˜oigi v˜orrandite vasakud pooled erinevad ning vasakutes pooltes esinevaid

muutujaid paremates pooltes ei esine (muid muutujaid v˜oib esineda).

Nii saamegi k¨atte muutujate v¨a¨artustuse. Asendades selle v¨a¨artustuse

muutumispiirkonna t¨u¨upi, saame k¨atte funktsiooni rakendamise tulemuse

t¨u¨ubi. M˜oned muutujad v˜oivad j¨a¨ada v¨a¨artustamata, need seotakse uuesti

kvantoritega, mis l¨ahevad tulemuse t¨u¨ubi ette.

Fumontrixis kasutatakse unifitseerimist ainult funktsiooni rakendamise

semantika andmisel, mitte n¨aidiste sobitamisel, valikuavaldises ega muutu-

ja t¨u¨ubi m¨a¨aramise (t¨u¨ubiinferentsi) jaoks nagu Haskellis. Seega k¨aituvad

pol¨umorfsed v¨a¨artused pol¨umorfselt ainult funktsiooni rakendamisel, mitte

aga n¨aiteks valikualternatiivi paremas pooles. Seega peavad valikuavaldises

alternatiivide paremad pooled olema k˜oik sama t¨u¨upi, vajadusel tuleb pol¨u-

morfsete v¨a¨artuste kvantoreid k¨asitsi avada.

Valikualternatiivis saaks pol¨umorfismi v˜oimaldada, kui defineerida sel-

le semantika funktsiooni rakendamise semantika kaudu (valikualternatiivist

moodustataks siis λ-abstraktsioon, kus n¨aidiseks oleks valikualternatiivi va-

sakuks pooleks olev n¨aidis), nagu on tehtud do-avaldise korral. Fumontrixis

seda siiski tehtud ei ole, kuna erinevalt do-avaldisest ei ole valikuavaldis rea-

liseeritud s¨untaktilise suhkruna.

7.6

T¨

u¨

ubitaseme programmeerimise semantikast

7.6.1

T¨

u¨

ubitaseme funktsioonid

T¨u¨ubitaseme funktsioonid konstrueeritakse Fumontrixis λ-abstraktsioonide-

na. Selleks on kaks eraldi konstruktsiooni — mitterekursiivne λ ja lihtrekur-

siivne λ.

Mitterekursiivse t¨u¨ubitaseme λ-abstraktsiooni semantikaks on funktsioon,

mis seab (fikseeritud liiki) t¨u¨ubitaseme objektidele vastavusse (samuti min-

git fikseeritud liiki, mis v˜oib olla erinev argumentide liigist) t¨u¨ubitaseme ob-

jektid. Sellele funktsioonile argumendi andmisel lisatakse argument konteksti

λ-abstraktsiooni peas m¨a¨aratud muutujanime alla ning selles t¨aiendatud kon-

tekstis v¨a¨artustatakse λ-abstraktsiooni keha.

Lihtrekursiivse t¨u¨ubitaseme λ-abstraktsiooni semantikaks on samuti funkt-

sioon, mis seab t¨u¨ubitaseme objektidele vastavusse t¨u¨ubitaseme objektid. See

funktsioon moodustatakse teistmoodi kui mitterekursiivsel juhul. Seda vaat-

leme l¨ahemalt jaotises 7.6.3.

λ-abstraktsiooniga defineeritud t¨u¨ubitaseme funktsioonide jaoks kasuta-

takse eraldi semantilist kategooriat GenType, mis sisaldab ka tavaliste t¨u¨upide

kategooriat Type. See on vajalik selleks, et λ-abstraktsiooni ei saaks t¨u¨u-

bikonstruktori parameetriks anda. Nagu n¨agime jaotises 6.2, oleks vastasel

70

---

korral v˜oimalik defineerida mittetermineeruv t¨u¨ubitaseme funktsioon.

7.6.2

V¨

a¨

artused t¨

u¨

ubitasemel

Fumontrixis on v˜oimalik andmetaseme v¨a¨artustega arvutada ka t¨u¨ubitase-

mel. Kuna t¨u¨ubitase ja andmetase on teineteisest eraldatud ja automaatset

v¨a¨artuste liikumist nende vahel ei toimu, siis tuleb see liikumine ilmutatult

teha. Selleks on Fumontrixis olemas value- ja type-konstruktsioonid.

value-konstruktsioon muudab andmetaseme v¨a¨artuse t¨u¨ubitaseme objek-

tiks liiki @. S¨untaktiliselt on value-konstruktsiooni argumendiks andmetase-

me avaldis, mille v¨a¨artus v˜oib s˜oltuda keskkonnast. T¨u¨ubitasemel keskkonda

ei ole, seega t¨u¨ubitasemel v¨a¨artustega arvutamisel v¨alja arvutatud v¨a¨artuse

sisse vaadata ei saa ning v¨a¨artust saab kasutada musta kastina, mille kohta

on teada ainult selle t¨u¨up.

Et p¨arast t¨u¨ubitasemel t¨o¨otlemist tulemuseks saadud v¨a¨artust j¨alle and-

metasemel kasutada, on vaja teada keskkonda, milles see v¨a¨artus v¨alja ar-

vutada. Kui v˜otta selleks see keskkond, milles toimub v¨a¨artuse kasutamine

andmetasemel, siis oleks value-konstruktsiooni sees olevas avaldises esine-

vad identifikaatorid, mis ei ole defineeritud selle sama konstruktsiooni sees,

d¨unaamilise skoopimisega.

Selline piiramatu d¨unaamiline skoopimine, kus kasutatav on kogu d¨unaa-

miline keskkond, tekitab probleeme. N¨aiteks on v˜oimalik tekitada rekursioon

ilma rekursioonioperaatorit kasutamata. Saame kirjutada isegi t¨u¨ubitaseme

funktsiooni, mis ei termineeru:

type rf = \ x : @ . value (type rf x);

v = type rf (value 3);

Kuna rf kutsutakse v¨alja v defineerimisel, siis rf sees olevale avaldisele

type rf x rakendatakse d¨unaamilist skoopi, milles on see sama rf juba ole-

mas, seega rf saab kasutada rekursiivselt iseennast ning praegusel juhul tuleb

l˜opmatu rekursioon.

Kuna Fumontrixis soovitakse garanteerida t¨u¨ubikontrolli termineerumi-

ne, siis siin d¨unaamilist skoopimist ei kasutata ning ka value-konstruktsiooni

sees rakendatakse leksilist skoopimist. Selleks on value-konstruktsiooni ra-

kendamise ajal vaja k¨atte saada see keskkond, milles see konstruktsioon te-

kitati. Kuna v¨a¨artustega arvutatakse ka t¨u¨ubitasemel, siis keskkonda ennast

ei saa value-konstruktsiooni juurde lisada (seda ei ole t¨u¨ubitasemel veel ole-

mas). Selle asemel m¨a¨aratakse skoobile unikaalne identifikaator ning lisa-

takse see value-konstruktsioonile selle moodustamisel. Samuti arvutatakse

kohe moodustamisel v¨alja value-konstruktsioonis oleva avaldise t¨u¨up (seda

saab t¨u¨ubitasemel teha). value-konstruktsiooni semantikaks on siis nelik, mis

71

---

koosneb avaldisest, keskkonna (selle, milles avaldis tuleb v¨a¨artustada) iden-

tifikaatorist, selle avaldise t¨u¨ubist ning lisainfost (StatSemInfo), mis tuleb

t¨u¨ubitasemelt andmetasemele edastada selle avaldise v¨a¨artustamiseks.

Selleks, et value-konstruktsiooni sees oleva avaldise v¨a¨artust kasutada on

vaja see t¨u¨ubitasemelt tagasi andmetasemele viia. Selleks on olemas type-

konstruktsioon, mis muudab liiki @ t¨u¨ubitaseme objekti andmetaseme v¨a¨ar-

tuseks. Liiki @ t¨u¨ubitaseme objekte saab tekitada ainult value-konstruktsioo-

niga ning t¨u¨ubitasemel nende sisu muuta ei saa, seega kui liiki @ t¨u¨ubitaseme

avaldis v¨a¨artustada, siis tulemuseks on mingi value-konstruktsiooni seman-

tika.

value-konstruktsioon v˜oib esineda ainult mingi t¨u¨ubitaseme avaldise sees.

Selleks v˜oib olla kas type-konstruktsioon v˜oi type-deklaratsiooni parem pool.

P˜ohim˜otteliselt v˜oiks seda kasutada ka t¨u¨ubiannotatsioonis (n¨aiteks argu-

mendina liiki @ -> * t¨u¨ubikonstruktorile), aga sellel pole m˜otet, kuna sellis-

te t¨u¨upide v˜ordsust ei saa t¨u¨ubitasemel kontrollida (value-konstruktsiooni

sees oleva avaldise v¨a¨artus selgub alles andmetasemel) ja seet˜ottu loetakse

iga value-t¨u¨up k˜oigi muude t¨u¨upidega (sh iseendaga) mittev˜ordseks ja mit-

teunifitseeruvaks. Seega selline annotatsioon p˜ohjustab alati t¨u¨ubivea.

Seet˜ottu m¨a¨aratakse liigitasemel (skoobi piires) unikaalsed identifikaato-

rid k˜oigi type-deklaratsioonide ja type-avaldiste skoopide jaoks. Andmetase-

mel salvestatakse type-deklaratsiooni korral selle keskkond vastava unikaal-

se identifikaatori alla jooksvasse keskkonda. Selleks on keskkonnas kujutus

eSavedEnv, mis seab skoobi identifikaatorile vastavusse salvestatud keskkon-

na. Samuti salvestatakse keskkond type-avaldise v¨a¨artustamise ajaks vastava

unikaalse identifikaatori alla.

Igale value-konstruktsioonile seatakse liigitasemel vastavusse k˜oige sise-

mise seda sisaldava type-deklaratsiooni v˜oi type-avaldise skoobi identifikaa-

tor, mille j¨argi saab hiljem andmetasemel jooksvast keskkonnast salvestatud

(leksilise skoobi) keskkonna k¨atte.

Andmetasemel value-konstruktsiooni sees oleva avaldise kasutamiseks

tuleb see type-konstruktsiooniga tagasi andmetasemele tuua. Seega type-

konstruktsiooni sees olev t¨u¨ubitaseme objekt v¨a¨artustatakse, saades value-

konstruktsiooni, mille juures on skoobi identifikaator. Selle j¨argi v˜oetakse

jooksvast keskkonnast salvestatud leksilise skoobi keskkond ja v¨a¨artustatak-

se avaldis selles salvestatud keskkonnas. Saadud tulemus ongi type-avaldise

v¨a¨artuseks.

P˜ohim˜otteliselt v˜oiks ka otse value-konstruktsioonidele skoobiidentifikaa-

torid juurde lisada, kuid sellisel juhul tuleks ka t¨u¨ubitaseme avaldistele and-

metaseme semantika anda. Samuti tuleks k˜oik type-deklaratsiooni sees ole-

vate value-avaldiste salvestatud leksilised keskkonnad lisada samasse skoopi

kui selle type-deklaratsiooniga defineeritav t¨u¨ubitaseme muutuja. See skoop

72

---