Kvantitatiivne tüübiteooria pärineb prantsuse loogik Jean-Yves Girard’i lineaarsel loogikal (aastast 1987), kus implikatsiooni eeldust peab (vaikimisi) järelduse näitamiseks täpselt üks kord kasutama.
Kvantitatiivne tüübiteooria on Idrise omadus, kus lineaarne loogika on pandud kokku kõrgmat järku funktsioonidega. Idrise parameetritele ja kohalikele muutujatele lisatakse arvud, mitu korda seda kasutama peab. Funktsiooni defineerimisel saame märkida, millise arvuga on parameeter.
Abstraktses mõttes tähendab see seda, et Idrises on võimalik modelleerida arvutusi piiratud resurssidega. Näiteks on piiratud resurss mälu, internetiühendus, failid, konsool jne. Kõik, mida ei saa või ei peaks saama kopeerida. Viimasel ajal populaarseks muutunud Rust-i mälu laenamise mudel põhineb samuti sarnasel teoorial.
Siiani oleme Idrises vaadanud juhte, kus (vaikimisi) on arvuks suva. See tähendab, et muutujat/parameetrit saab kasutada suvaline arv kordi. Selline arv sobib väikese mahuga andmetele, mida pole liiga kulukas vajadusel kopeerida või siis ära visata, kui tuleb välja, et siiski ei läinud vaja.
Järgnevalt vaatame arvu null ja üks.
Idrises tähendab arv 0, et selle arvuga muutuja seest andmeid lugeda ei tohi. Ehk, kuigi tüübikontrolli ajal saame sellest rääkida, siis programmi käivitamise ajaks on kõik arvuga 0 muutujad asendatud ()-ga. Näiteks saame teha funktsiooni const mis võtab kaks argumenti ja tagastab neist esimese. Kuna teist argumenti ei kasutata, saame sellele panna arvu 0.
| 1const : a -> (0 y : b) -> a 2const x y = x |
Arv null on kui (liidese) spetsifikatsioon, et mingit parameetrit ei ole põhimõtteliselt vaja ja et seda tegelikult ei kasutata. Näiteks aitab see eemaldada programmist tõestusi, mis on vajalikud tüübikontrolliks kuid mitte programmi täitmise ajal. Näiteks on Idrise standardteegis funktsioon, mis tagastab mittetühja listi pea.
| 1head : (l : List a) -> {0 _ : NonEmpty l} -> a |
Sellise näite puhul annab arv null võimaluse usaldusväärselt eemaldada täitmise ajal mittevajaliku arvutuse kõik esinemsikohad. Nii et me saame kindlad olla, et seda ei hakatagi arvutama.
Ekspltsiitselt nimetamata tüübiparameetri (näiteks a tüübis a -> a) arv on null.
Seetõttu saame me, näiteks, kindlad olla, et funktsioon tüübiga a -> a rakendatuna väärtusele 5 tagastab viie, kuna funktsioon ei saa (implitiitse) arvu null tõttu sõltuda tüübi a väärtusest.
Muu arvu puhul me sellist garantiid ei oma. Näiteks funktsioon evil_id käitub muude tüüpide puhul nagu identsusfunktsioon aga täisarvude puhul liidab alati parameetrile kahe. Kui parameertile a panna arv 0, siis ei saa erinevaid tüüpe eristada ja funktsioonil ei jää muud üle kui tagastada parameeter.
| 1evil_id : {a: Type} -> a -> a 2evil_id {a=Int} x = x+2 3evil_id {a=_} x = x |
Idrises on arv 1. Selle arvuga muutujat peab kasutama täpselt üks kord. Lisaks üks kord kasutamisele võib seda muutujat kasutada null-arvuga kohtades. Näiteks saame teha funktsiooni const mis võtab kaks argumenti ja tagastab neist esimese. Kuna esimest argumenti kasutatakse täpselt üks kord, saame sellele panna arvu 1.
| 1const' : (1 x: a) -> b -> a 2const' x y = x |
Kohe, kui vähemalt üks funktsiooni argument on arvuga üks, loetakse, et see funktsioon peab olema lineaarne. Ehk funktsiooni argumendiga seotud resurss peab mingis teoreetilises mõttes jõudma tagastusväärtusse täpselt üks kord. Lineaarsus peaks välistama juhu, kus väärtust saab kopeerida. Idrises on võimatu kirjutada järgneva funktsiooni defintisioon.
| 1double : (1 x: a) -> (a, a) 2double x = ?v6imatu |
Parameetri arvu saab kirjutada tüübideklaratsiooni. Kohaliku muutuja arvu seadmiseks võib selle kirjutada let-is muutuja ette. Vaikimisi püüab Idris õige arvu tuletada.
| 1const'' : (1 x: a) -> (0 y: b) -> a 2const'' x y = 3 let 1 x' = x 4 0 y' = y 5 x'' = x' 6 in 7 x'' |
Arvu üks on mõistlik kasutada liidestes ja abstraktsete funktsioonides, kuna lineaarse väärtuse mustrisobitus loeb selle ainsa kasutuskorrana. Kui aga mustri juhtudes arvuga üks komponenti ei ole, siis saame lineaarsusest mööda hiilida. Näiteks naturaalarvude puhul järgnevalt.
| 1doubleNat : (1 x: Nat) -> (Nat, Nat) 2doubleNat 0 = ( 0, 0) 3doubleNat (S k) = (S k, S k) |
Idrise standardteegis kasutatakse lineaarseid tüüpe programmide mugavamaks kirjutamiseks, et lubada vajadusel kasutada sisendit-väljundit, erindeid, seisundeid jne. Vaata moodulit Control.App.
Siinkohas võib olla ka huvitav teada, kuidas on implementeeridut (lineaarne) IO keeles Idris. Nimelt on defineeritud abstraktne andmetüüp data %World = %MkWorld, mille definitsioon on kasutajate eest varjatud. Tähtis on, et kasutaja ei saa oma suva järgi %World-tüüpi väärtust luua. Seda andmesktruktuuri kasutatakse kui seisundit, ehk iga sisendi-väljundi funktsioon võtab lineaarselt sisse %World-i ja tagastab %World-i. Tänu lineaarsusele ei pea me %World andmestruktuuris midagi hoidma vaid saame kõrvalefekti lihtsalt arvutis ära teha. Lineaarsus garanteerib, et kood ei kasuta vana maailma väärtust — nii otseses kui abstraktses mõttes. Sellest tuleb ka Philip Wadleri kuulsa artikli “Linear types can change the world!” (sõnamängu) mõte.
Kokkuvõtteks. Lineaarsed tüübid sobivad hästi kasutusjuhtudeks, kus soovitakse vältida andmete tahtmatut kopeerimist või on vaja mälu kindlasti õigeaegselt vabastada.
Lisaks Idris 2-le on lineaarseid tüüpe võimalik kasutada Haskellis läbi GHC eksperimentaalse laienduse LinearTypes. Sel juhul saab kasutada funktsioonitüübi süntaksit a %1 -> b ning a %Many -> b.
Paljudes keeltes on lineaarsuse asemel kasutatud veidi nõrgem omadus afiinsus. See tähendab, et resurssi võib kasutada maksimaalselt üks kord. Ehk resurss võib jääda kasutamata.
Programmeerimiskeel Clean (https://clean-lang.org/) on Haskelli sarnane laisk programmeerimiskeel, kus sisend-väljund on monaadide asemel lahendatud unikaalsete (afiinsete) tüüpide funktsioonide abil.
Keeles Swift (versioonist 5.9+) on võimalik kasutada afiinseid tüüpe märkides struktuur ~Copyable-abil mitte-kopeeritavaks ning parameetrid consuming-argumentideks.
Keeles Rust kasutatakse (mälu) omamise jälgimiseks afiinset tüübisüsteemi kus väärtuste kloonimiseks (duplitseerimiseks) peab seda ekspltsiitselt käskima. See tähendab ka seda, et resursi omandisuhteid (kas laenatud väärtus või omatav väärtus) tuleb funktsioonikutsetes spetsifitseerida.
Keeles C++ on konventsioon kasutada unique_ptr-t afiinsust aga seda kompilaator ei kontrolli.
Programmeerimiskeeltes, kus kompilaator peab oskama automaatselt resurssidest aru saada, lineaarne loogika enamasti Idrisest keerulisemaks ei lähe. Idrises on kolm arvu ning vajadust ühest suurematest diskreetsetest arvudest puudub. Vajadusel saame teha vektori pikkusega n elementi, kus iga element on lineaarne resurss.
Iris raamistikus (https://iris-project.org/), mis on mõeldud programmide korrektsuse tõestamiseks, on resursside algebra palju keerulisem. Kasutusel on näiteks arvud 2−n iga naturaalarvu n kohta — tähendab, et resurssi saab alati jagada kaheks. See mudel võimaldab modelleerida eksklusiivse (s.t. võime lugeda ja muuta) omandi jagamise osaliseks (kõik võivad vaid lugeda) omandiks ning selle uuesti kokku panemist eksklusiivseks omandiks (võime jälle muuta).