U L i k o o L matemaatika-informaatikateaduskond

4

T¨

u¨

ubis¨

usteemist

4.1

Fumontrixi t¨

u¨

ubis¨

usteemist ¨

uldiselt

Fumontrixi t¨u¨ubis¨usteemis on v˜oimalik t¨u¨upe koostada baast¨u¨ubi Int, t¨u¨ubi-

konstruktorite, ¨uldisuskvantorite ja olemasolukvantorite abil. Sarnaselt Has-

kelliga klassifitseeritakse t¨u¨ubitaseme objektid liikidesse, kuid erinevalt Has-

kellist on Fumontrixis olemas ka liik @, mis t¨ahistab t¨u¨ubitasemel kasutatavat

andmetaseme v¨a¨artust.

Erinevalt Haskellist ei kasutata Fumontrixis t¨u¨ubiinferentsi ning t¨u¨upi-

de m¨a¨aramiseks vajalik info saadakse p˜ohiliselt λ-abstraktsioonides n¨aidise-

le lisatud t¨u¨ubiannotatsioonidest. ¨

Uldisuskvantori avamiseks on Fumontrixis

operaator $:, mis avab tipmise taseme ¨uldisuskvantori ja v¨a¨artustab sellega

seotud muutuja antud t¨u¨ubiga. Kuna avatakse k˜oige tipmine ¨uldisuskvantor,

siis erinevalt GHC-st (kus kvantori avamiseks tuleb lisada annotatsioon, kus

kogu t¨u¨ubiavaldis on ¨umber kirjutatud ning k˜oik vaadeldava muutuja esine-

mised asendatud (¨uhe ja sama) soovitud t¨u¨ubiga) on Fumontrixis kvantorite

j¨arjekord oluline. Seega t¨u¨ubid

forall A. forall B. A -> B

forall B. forall A. A -> B

forall A. A -> (forall B. B)

on Fumontrixis k˜oik erinevad, erinevalt GHC-st, kus analoogilised t¨u¨ubid

(vaid kvantifitseeritud muutujad on v¨aikese t¨ahega) on k˜oik v˜ordsed ja GHC

teisendab need automaatselt kujule

forall a b. a -> b

Fumontrixis ei oleks selliseid automaatseid teisendusi v˜oimalik teha, kuna see

muudab t¨u¨ubiavaldise semantikat (operaator $: k¨aitub nendel kolmel juhul

erinevalt).

4.2

Baast¨

u¨

ubid

Fumontrixis on sisseehitatud t¨aisarvut¨u¨up Int (piiramatu suurusega t¨ais-

arvud, vastab Haskelli t¨u¨ubile Integer). Funktsioonit¨u¨ubi noolt ei vaadel-

da Fumontrixis eraldi konstruktorina, funktsioonit¨u¨ubi konstruktsioon t

1

->

t

2

on eraldi konstruktsioon, mitte infiksoperaatori kasutus. See v¨aldib m˜o-

ningaid probleeme. Vastasel korral oleks n¨aiteks v˜oimalik konstruktor (A

->) monaadiks defineerida ja selle juhu arvestamine teeks monaadiliste v¨a¨ar-

tuste pol¨umorfismi semantika keeruliseks.

20

---

Lihtsuse huvides on esialgu keelest v¨alja j¨aetud ujukomaarvud ning m¨argi-

ja stringit¨u¨ubid. Vajadusel saab t¨aisarvut¨u¨upi kasutada m¨argit¨u¨ubina, kuju-

tades m¨arki t¨aisarvuna, mis vastab selle Unicode’i koodile. Stringid oleks siis

lihtsalt t¨aisarvude listid.

4.3

T¨

u¨

ubikonstruktorid

Fumontrixis on t¨u¨ubikonstruktoreid v˜oimalik sisse tuua data-deklaratsiooni-

ga (algebralised andmet¨u¨ubid), exists-n¨aidisega (olemasolukvantoriga seo-

tud konstruktor) v˜oi forall-avaldisega (¨uldisuskvantoriga seotud konstruk-

tor).

Nende konstruktorite semantika on ¨uhesugune. Konstruktorile seatakse

vastavusse unikaalne identifikaator (UID), mis on t¨aisarv alates 1-st. K˜oigi

skoobis eksisteerivate konstruktorite (sh nende, mis on teise samanimelise

konstruktori t˜ottu varjatud) UID-d on erinevad.

Lisaks sellele on keelde sisse ehitatud t¨u¨ubikonstruktor ST (ST-monaadi

jaoks), mille UID on negatiivne (−2). Kui tulevikus lisanduvad keelde muud

sisse ehitatud t¨u¨ubikonstruktorid, siis need on samuti negatiivse UID-ga. UID

−1 on reserveeritud IO-konstruktori jaoks, mida praegu keeles ei ole.

4.4

Universaalselt kvantifitseeritud t¨

u¨

ubid

Fumontrixis on olemas universaalselt kvantifitseeritud t¨u¨ubid (vt [4], peat¨ukk

4) kujul forall C : k . t[C] ja forall c C : k . t[C]. ¨

Uldisuskvanto-

rid v˜oivad esineda suvalise t¨u¨ubikomponendi ¨umber, mitte ainult tipmisel

tasemel.

Universaalset t¨u¨upi v¨a¨artuse loomiseks tuleb kasutada forall-avaldist,

mis toob sisse uue muutuja, mis on skoobis selle avaldise piires. N¨aiteks

f = forall A . \ x : A .

let

ys = (x :: x :: Nil) : List A

in

head ys;

¨

Uldisuskvantoriga seotavat muutujat saab skoopi tuua ka GHC-s:

f :: forall a. a -> a

f x =

let

ys :: [a]

ys = [x,x]

21

---

in

head ys

Nendes n¨aidetes muutujad A ja a on skoobis funktsiooni f definitsiooni kehas

ning parameeter x on seal monomorfset t¨u¨upi A v˜oi a, samuti on monomorfset

t¨u¨upi ys, millele annotatsioon on lisatud.

GHC-s on vaja t¨u¨ubiparameetri nime skoopi toomiseks vaja tingimata

kasutada t¨u¨ubisignatuuri (ja seega tuleb deklareerida ka tagastusv¨a¨artuse

t¨u¨up). Kui viimases n¨aites signatuur ¨ara j¨atta, siis GHC seda enam ei akt-

septeeri (isegi, kui n¨aidisele x annotatsioon lisada (x :: a)), kuna muutuja

a ei ole siis skoobis (ning samuti ei sobi signatuuri [a] pol¨umorfne inter-

pretatsioon forall a. [a]). Fumontrixis piisab ainult argumentide t¨u¨upide

deklareerimisest, tagastusv¨a¨artuse t¨u¨upi pole vaja deklareerida.

Fumontrixis ¨uldisuskvantori ilmutatult avamiseks kasutatavat operaato-

rit vaatlesime juba jaotises 4.1. Pol¨umorfse funktsioonirakendamise k¨aigus

toimub ka automaatne ¨uldisuskvantorite avamine, kuid ainult funktsiooni ja

argumendi tipmisel tasemel. Seda vaatleme l¨ahemalt jaotises 6.4.

4.5

Eksistentsiaalsed t¨

u¨

ubid

Fumontrixis on olemas eksistentsiaalsed t¨u¨ubid (vt [4], peat¨ukk 5) kujul

exists C : k . t[C] ja exists c C : k . t[C].

Eksistentsiaalset t¨u¨upi v¨a¨artuse loomiseks tuleb kasutada pakkimisfunkt-

siooni, mis on s¨untaktiliselt samal kujul nagu tulemuseks olevat eksistent-

siaalset t¨u¨upi t¨ahistav t¨u¨ubiavaldis. Pakkimisfunktsiooni t¨u¨ubiks (t¨u¨ubiklas-

siga juhul) on

forall c C : k . t[C] -> (exists c C : k . t[C]).

Eksistentsiaalset t¨u¨upi v¨a¨artust v˜oib vaadelda kui paari t¨u¨ubiparameet-

rist C ja t¨u¨upi t[C] v¨a¨artusest. Fumontrixi semantikas on t¨u¨ubiparameetri

asemel t¨u¨ubiklassi c eksemplari v¨a¨artus t¨u¨ubi C jaoks. Seega eksistentsiaalne

t¨u¨up on paar kahest v¨a¨artusest. Parameetrilise (ilma t¨u¨ubiklassita) kvantifit-

seerimise korral on eksemplari v¨a¨artuse asemel ¨uhikt¨u¨ubi element, mis infot

ei sisalda.

Eksistentsiaalset t¨u¨upi v¨a¨artusi automaatselt ei avata, seega ainuke v˜oi-

malus sealt info k¨attesaamiseks on kasutada exists-n¨aidist

exists c C : k . p, mis lisab konteksti uue t¨u¨ubikonstruktori C ning muu-

dab selle klassi c esindajaks, lisades C jaoks klassi c eksemplari, mis on v˜ordne

eksistentsiaalse v¨a¨artuse sees olnud eksemplariga. Eksistentsiaalse t¨u¨ubi sees

olnud v¨a¨artuse jaoks kasutatakse n¨aidist p.

Erinevalt GHC-st on v˜oimalik olemasolukvantoreid kasutada suvalise t¨u¨u-

bikomponendi ¨umber (GHC-s ainult seoses algebraliste andmet¨u¨upidega, vt

22

---