Kvantitatiivne tüübiteooria
.. ehk lisame muutujatele kogused
Tehniliselt, igale muutujal ja parameetrile on lisatud arv, mitu korda teda peab arvutamiseks kasutama.
- null -- ei tohi arvutuseks kasutada
- üks -- peab kasutama täpselt üks kord
- suva -- saab kasutada suvaline arv kordi
Selliste arvudega saab piiratud resursside üle järge pidada. Mida üks "resurss" tähendab on API looja otsustada -- tüübiteooria on siin lihtsalt vahend.
Motivatsioon
null
Resurss on juba kasutatud või allokeeritud mingi muu tegevuse jaoks. Saame mingist resursist rääkida ehk koodis on olemas seosed selle resursiga -- aga "kasutada" neid ei saa. Programmi töö ajaks võime null resursid programmist kustutada.
Näited:
- programmi korrektsuse tõestused, sertifikaadid
- tüübid
suva
Lõpmatu resurss, mille üle pole vaja arvet pidada. Kõik "tavalised" väärtused, mida saab luua, kopeerida, kustutada jne. Kõik matemaatilised ja algebralised objektid, mis eksisteerivad loogika põhjal -- sõltumata kontekstist.
üks
Mingis kontekstis unikaalne resurss.
Näited:
- fail, võrguühendus, veebiteenuse seanss
- IO terminal, ülisuur massiiv, riistvaraseade
Reeglid
null
Null arvuga parameetrit/muutujat võib
- lihtsalt mitte kasutada
- kasutada mõne muu funktsiooni null arvuga argumendi avaldises
suva
Suva arvuga parameetrit/muutujat võib kasutada ilma piiranguteta, sealhulgas funktsiooni null ja üks arvuga parameetri väärtusena.
Kusjuures, kui funktsiooni f : (1 _ : Int) -> Int üks arvuga parameetriks anda suva-arvuga väärtus, näiteks konstant 1, siis tulemus f 1 on suva-arvuga väärtus.
üks
Üks arvuga parameetri/muutuja saab ja peab üks kord kasutama. Ehk kas paigutada
- üks-arvuga muutujasse,
- tagastada või
- anda edasi ühele funktsioonile, mis võtab üks-arvuga argumendi.
Lisaks ühele kasutuskorrale võib üks arvuga parameetrit/muutujat kasutada nagu null arvuga parameetrit/muutujat.
Kuigi tagastustüübil süntaktiliselt arvu ei ole, muudab üks-arvuga argument ka funktsiooni tulemuse arvuks ühe -- seda nimetatakse lineaarsuseks.
Lineaarne tähendab (selles kontekstis) seda, et näiteks mingi väärtuse x-ga tehakse kõigepealt teisendus f, siis g ja siis h. Ehk h (g (f x)). See välistab muuhulgas selle, et väärtust x ja f x tulemust peaks korraga mälus hoidma.
Idris-e tüübisüsteem on selline, et üks-arvuga funktsiooni defineerimisel on lineaarsus tagatud.
Lineaarsust saab "rikkuda" kasutades mustrisobitust. Tüübi või liidese loojale antud teatud võimalus lineaarsusest kõrvale hiilida aga funktsioonide implementeerija peab järgima ranget distsipliini.
Mustrisobituse puhul on tähtis läbi mõelda, milliseid andmestruktuure on mõtet lineaarseks teha. Näiteks Bool-i pole mõtet, kuna mustrisobitusega saame True ja False juhud, kus algne tõeväärtus on "ära kasutatud". Saab kasutada ka trikki, kus uue andmetüübi konstruktor on tehtud privaatseks, mistõttu saab seda kasutada vaid näiteks mingi liidese loomiseks.
Enamasti on tarvis n.n. lineaarse paari andmetüüpi, et tagastada lineaarne resurss ja mingi muu mittelineaarne väärtus.
data L : Type -> Type -> Type where
(#) : (1 _ : a) -> b -> L a b
- Konstrueerimine: lineaarset resrurssi saab panna esimeseks komponendiks, aga siis on terve paar lineaarne.
- Mustrisobitusel: kui kogu paar peab olema lineaarne, siis selle esimene komponent on lineaarne.
Lineaarsete resursside modelleerimisel kasutatakse sageli liideseid, et peita destruktiivsed ja ebaturvalised tegevused puhta lineaarse liidese taha. Näiteks massiivi liides
interface Array arr where write : (1 a : arr) -> Nat -> Double -> arr read : (1 a : arr) -> Nat -> L arr Double size : (1 a : arr) -> L arr Nat withArray : Nat -> ((1 a : arr) -> L arr c) -> c