Sistem tipova

U programskim jezicima, sistem tipova je zbirka pravila koji dodeljuje pravilno nazvani tip različitim konstrukcijama programa od koga se sastoji, kao što su promenljive, ekspresije, funkcije ili moduli. Glavna svrha sistema tipiziranja je da smanji mogućnosti za bagove u računarskim programima definisanjem sučelja između različitih delova kompjuterskog programa, i onda da proveri da li su delovi povezani na dosledan način. Ova provera se može desiti statično (pri kompiliranom vremenu), dinamično (pri rantajmu), ili kao kombinacija statičke i dinamičke provere. Sistemi tipiziranja imaju ostale svrhe takođe, kao što je omogućavanje određenih optimizacija kompilatora, dozvola za višestruku opremu, pružanje forme dokumentacije, itd.

Sistem tipiziranja sarađuje sa tipom od svake izračunate vrednosti i, proverom protoka ovih vrednosti, pokušava da osigura ili dokaže da se nijedna greška u tipiziranju neće pojaviti. Posebni sistem tipiziranja u pitanju odlučuje tačno šta čini grešku tipiziranja, ali uglavnom cilj je da se spreče operacije od kojih se očekuje određeni tip vrednosti koji koristi vrednosti za koje te operacije nemaju smisla (logičke greške); greške memorije će takođe biti sprečene. Sistemi tipiziranja su često deo programskih jezika, i ugrađeni u interpretatore i kompilatore; iako sistem tipiziranja jezika može biti nadograđen opcionim alatkama koji odrađuju dodatne vrste provere koristeći se originalnom sintaksom jezika ili gramatikom.

Pregled upotrebe

Primer jednostavnog sistema tipova se nalazu u S jeziku. Delovi S programa su definicije funkcija. Jedna funkcija je pozvana drugom funkcijom. Sučelje funkcije navodi ime funkcije i listu vrednosti koje se prosleđuju do koda funkcije. Kod pozvane funkcije navodi ime pozvanog, zajedno sa imenima promenljivih koji čuvaju vrednosti da bi ga prosledili. Tokom izvršenja, vrednosti su stavljenje u privremeno skladište, onda izvršenje skoči do koda pozvane funkcije. Kod pozvane funkcije pristupa vrednostima i koristi ih. Ako su instrukcije unutar funkcije ispisane sa pretpostavkom da primaju celobrojnu vrednost, ali pozvani kod je prosledio decimalnu vrednost, onda će netačni rezultat biti izračunat od strane pozvane funkcije. S kompilator proverava deklarisani tip za svaku poslatu promenljivu, protiv deklarisanog tipa za svaki promenljivu u sučelju pozvane funkcije. Ako tipovi nisu isti, kompilator izbacuje grešku.

Kompilator može takođe koristiti statički tip vrednosti da optimizuje skladište koje mu je potrebno i izbor algoritama za operacije nad vrednostima. U mnogim S kompilatorima decimalni tip podataka, na primer, je predstavljen u 32 bita, u saglasnosti sa IEEE 754. Oni će tako koristiti specifičnu-decimalnu-tačku skupa operacija nad tim vrednostima (adicija decimalne-tačke, množenje, itd. ).

Dubina tipa ograničenja i manir njihove procene utiče na tipiziranje jezika. Programski jezik može dalje pomagati operaciji sa različitim konkretnim algoritmima nad svakim tipom u slučaju tipa polimorfizma. Teorija tipiziranja je studija sistema tipiziranja, iako konkretni sistemi tipiziranja programskih jezika potiču od delova problema kompjuterske arhitekture, kompilatorske implementacije, i dizajna jezika. 

Osnove

Formalno, teorije tipiziranja proučavaju sisteme tipiziranja. Programski jezik mora imati događaj da bi proverio tipiziranje koristeći se sistemom tipiziranja ili pri kompilatorskom vremenu ili rantajmu, ručno zabeležen ili automatski zaključen. Kao što je Mark Manase rekao:

Dodela tipa podataka—tipiziranje— daje značenje sekvencama bitova kao što je vrednost u memoriji ili neki objekat kao što je promenljiva. Hardver računara generalne svrhe nije u mogućnosti da razlike između na primer memorijske adrese i instrukciskog koda, ili između karaktera, celog broja, ili decimalne tačke, zato što ga ne čini unutrašnju razliku između bilo koje moguće vrednosti koje bi sekvence bitova mogle da "znače"". Povezivanje sekvenci bitova sa tipom prenosi to značenje hardveru kako bi se formirao simbolični sistem sačinjen od hardvera i nekog programa.

Program potpomaže svakoj vrednost sa najmanje jednim određenim tipom, ali se takođe može startovati jednu vrednost koja je povezana sa mnogoh podtipovima. Drugi entiteti, kao što su objekti, moduli, kanali komunikacije, zavisnosti mogu se povezati sa tipiziranjem. Čak i tipiziranje se može povezati sa tipiziranjem. Implementacija sistema tipiziranja može u teoriji povezati identifikacije nazvane tip podataka (tip vrednosti), klasa (tip objektna), i vrsta (tip tipa, ili metatip). Ovo su apstrakcije kroz koje tipiziranje prolazi, nad hijerarhijom nivoa koji se nalaze u sistemu.

Kada programski jezik uključuje razrađen sistem tipiziranja, dobija fino zrnastiji set pravila od klasične provere tipiziranja, ali ovo dolazi po sa cenom da kada zaključci tipiziranja (i ostale osobine) postanu neodlučiv zadatak, i kada više pažnje mora da se posveti od strane programera da zabeleži kod ili da razmotri operacije koje se odnose na računar i funkcionisanje. Izazov je naći  dovoljno izražajan sistem tipiziranja koji zadovoljava sve vežbe programiranja  u maniru sigurnog tipiziranja.

Što je više restrikcija tipiziranja nametnuto od strane kompilatora, biće jače ukucan programski jezik. Jako ukucani jezici često zahtevaju od programera da naprave ekplicitne konverzije u kontekstu gde implicitna konverzija ne bi škodila. Paskalov sistem tipiziranja je opisan kao "prejak" zato što, na primer, veličina niza ili niske je deo tipiziranja, što čini neki programerski zadatak teškim. Haskel je takođe jako ukucan ali njegova tipiziranja su automatski zaključena tako da su eksplicitne konverzije često (ali ne i uvek) bespotrebne.

Kompilator programskog jezika može takođe implementovati zavisno tipiziranje ili efektni sistem, što omogućava još programskih specifikacija koji treba da budu potvrđeni od strane kontrolora tipiziranja. Osim jednostavnih vrednosti-tipiziranja parova, virtuelni "region" koda sarađuje sa "efektnom" komponentom opisujući šta je urađeno sa čim, i dozvoljavajući na primer da se "odbaci" izveštaj greške. Tako simbolični sistem može biti sistem tipiziranja i efekta, što čini sigurniju proveru nego samostalnu proveru. 

Da li je automatizovan od strane kompilatora ili specifikovan od strane programera, sistem tipiziranje čini ponašanje programa ilegalnim što je van pravila sistema tipiziranja. Prednosti koje su pružene od strane programera uključuju : 

• Apstrakcija (ili modularnost) – tipiziranja koja omogućuju programerima da razmišljaju na višem nivou od bita ili bajta, nedosađujući se sa nisko-nivoim implementacijama. Na primer, programeri mogu početi da razmišljaju o niski kao p zbirci karaktera vrednosti umesto kao čist niz bajtova. Visoko idalje, tipiziranja omogućavaju programerima da razmišljaju i da izraze sučelja između bilo koja dva podsistema. Ovo omogućava više nivoa lokalizacije tako da zahtevane definicije za kompatibilnost podsistema ostaju dosledne kada ta dva podsistema komuniciraju.
• Dokumentacija– U izražajnijim tipovima tipiziranja, tipiziranje može služiti kao forma dokumentacije koja razjašnjava nameru programera. Na primer, ako programer deklariše funkciju kao povrato vreme tipiziranja, ovo dokumentuje funkciju kada vremensko tipiziranje može biti ekpslicitno deklarisano dublje u kodu da bi postao celobrojni tip.

Prednosti koje pruža kompilator sistema tipiziranja uključuju:

• Optimizacija – Statični tip provere tipiziranja može pružiti korisnu komplitaorsku informaciju. Na primer, ako tip zahteva da vrednost mora biti poravnata u memoriju kao deljiv sa četiri bajta, kompilator može biti u mogućnosti da koristi efikacnije instrukcije mašina.
• Sigurnost – Sistem tipiziranja omogućuje kompilatoru da detektuje nejasnoće ili verovatno netačni kod. Na primer, možemo identifikovati ekspresiju 3 / "Hello, World" kao netačnu, kada pravila ne govore kako da podelimo ceo broj sa niskom. Jako tipiziranje pruža veću sigurnost, ali ne može garantovati kompletnu sigurnost u tipiziranju.

Sigurnostu  u tipiziranju doprinosu programskoj tačnosti, ali može garantovati samo tačnost na račun pravljenja provere tipiziranja neodlučivog zadatka. U sistemu tipiziranja sa automatskom proverom tipiziranja program se može pokazati da radi netačno iako je ukucan sigurno, i da ne pruža kompiltorske greške. Deljenje nulom je nesigurna i netačna operacija, ali kontrolor tipiziranja radi samo na kompilatorskom vremenu koji ne skenira za deljenje nulom u mnogim programskim jezicima, i onda ostaje kao rantajm greška. Da bi se dokazalo odsustvo ovih više-generalnih-nego-kucanih defekta, drugih tipova formalnih metoda, kolektivno poznatih kao programske analize, se često koriste. Alternativno, dovoljno ekspresivni sistem tipiziranja, kao u zavisnim jezicima tipiziranja, može sprečiti ovde tipove grešaka (na primer, izražavajući "tip ne-nultih borjeva" ). Kao dodatak softversko testiranje je empirični metod za pronalaženje grešaka koje kontrolor tipiziranja ne može naći.

Provera tipiziranja

Proces potvrde i sprovođenja ograničenja tipiziranja – provera tipiziranja –može se desiti ili pri kompiliranom vremenu (statička provera) ili rantajm (dinamčka provera). Ako jezička specifikacija traži jako tipiziranje pravila (tj, više ili manje dozvoljava samo one automatske konverzije tipiziranja koje ne gube informaciju), jedan može da se odnosi na proces kao jako iskucan, ako ne, onda slabo iskucan. Termini se ne koriste često bukvalno. 

Statička provera tipiziranja

Statička provera tipiziranja je proces provere sigurnosti tipiziranja programa baziranog na analizi programskog teksta (izvornog koda). Ako program prođe kontrolora tipiziranja, onda program garantuje da zadovolji neki skup karakteristika sigurnusnog tipiziranja za moguće unose.

Zbog toga što statička provera tipiziranja operiše nad tekstom programa, to dozvoljava mnogim bagovima da budu uhvaćeni ranije u ciklusu razvitka.

Za statičnu proveru tipiziranja može se smatrati kao ograničena forma verifikacije programa (videti sigurno tipiziranje). U jeziku sigurnog tipiziranja, za statičnu proveru tipiziranja se takođe može smatrati kao optimizacija. Ako kompilator može da dokaže da je program dobro otkucan, onda ne mora da emituje dinamičke provere sigurnosti, što dozvoljava binarnom kompiliranom rezultatu da radi brže.

Statička provera tipiziranja za Tjuringovu-kompletnost jezika je inherentno konzervativna. To je, ako je sistem tipiziranja i zvuk (znači da odvija sve netačne programe) i  odlučiv (znači da je moguće napisati algoritam koji odlučuje da li je program dobro otkucan), onda uvek će biti moguće da se definiše program koji je dobro otkucas ali koji ne zadovoljava kontrolora tipiziranja. Na primer, razmotriti program koji sadrži ovaj kod:

if <complex test> then <do something> else <generate type error>

Čak iako ekspresija <complex test> uvek ima vrednost true pri rantajmu, većina kontrolora tipiziranja će odbiti program kao loše ukucan, zato što je teško (ako ne i nemoguće) za statički analizator da odluči da li else grana neće biti uzeta. S druge strane, statični kontrolor tipiziranja će brzo detektovati greške tipiziranja u retko korišćenim putevima koda. Bez statičke provere tipiziranja, čak i testovi pokrivenosti koda sa 100% pokrivenošću možda neće biti u mogućnosti da pronađu ovakve greške. Testovi možda neće uspeti da detektuju ovakve greške, zato što kombinacija svih mesta gde su vrednosti kreirane i svih mesta gde je određena vrednost korišćena mora biti uzeta u obzir.

Broj korisnih i čestih karakteristika porgramskog jezika ne može biti proveren statički, kao što može daunkesting. Zbog toga, mnogi jezici će imati i statičku i dinamičku proveru tipiziranja; statički kontrolor tipiziranja proverava šta može, i dinamički provera ostatak.

Mnogi jezici sa statičkom proverom tipiziranja pružaju način da zaobiđu kontrolora tipiziranja. Neki jezici dozvoljavaju programerima da biraju između statičke i dinamičke sigurnost tipiziranja. Na primer, S# pravi razliku između "statički-ukucanih" i "dinamički-ukucanih" promenljivih; bivša korišćenja su proverena statički, dok su kasnija korišćenja  proverena dinamički. Drugi jezici dozvoljavaju korisnicima da zapišu kod koji nije sigurno-ukucan. Na primer, u S-u, programeri mogu slobodno ubaciti vrednost između bilo koja dva tipa koji imaju istu veličinu. 

Za listu jezika sa statičkom proverom tipiziranja, videti kategorija za statički ukucane jezike.

Dinamička provera tipiziranja i rantajm tip informacija

Dinamička provera tipiziranja je proces provere sigurnosti tipiziranja programa pri rantajmu. Implementacije dinmačko proverenih jezika tipiziranja uglavnom sarađuju pri svakom rantajm objektu sa "tip" tagom (tj., referenca za tipiziranje) sadržeći svoje informacije tipiziranja. Ovaj rantajm tip informacije (RTTI) se može takođe koristiti za implementovanje dinamične opreme, kasnog vezivanja, daunkestinga, refleksije, i sličnih karakteristika.

Mnogi jezici sigurnosnog tipiziranja uključuju neku formu dinamine provere tipiziranja, iako imaju statičnog kontrolora tipiziranja. Razlog za ovo je taj da mnoge korisne karakteristike ili osobine je teško ili nemoguće potrvrditi statično. Na primer, pretpostaviti da program definiše dva tipa, A i B, gde je B podtip A. Ako program pokuša da konvretuje vrednost tipa A u tip B, što je poznato kao daunkesting, onda je operacije legalna samo ako je konvertovana vrednost stvarna vrednost tipa B. Zbog toga, dinačna provera je potrebna kako bi se proverilo da li je operacija sigurna; ova zahtevnost je jedna od kritika daunkestinga.

Po definiciji, dinamična provera tipiziranja može izazvati program da ne uspe pri rantajmu. U nekim programskim jezicima, moguće je učestovati i povratiti se iz ovih padova. U drugim, greške provere tipiziranja se smatraju fatalnim.

Programski jezici koji uključuju dinamičnu proveru tipiziranja ali ne i statičnu proveru tipiziranja se često nazivaju "dinamčno-ukucani programski jezici". Za listu takvih jezika, pogledati kategoriju za dinmačno ukucane programske jezike.

Kombinovanje statične i dinamčne provere tipiziranja

Neki jezici dozvoljavaju i statično i dinamčno tipiziranje (provere tipiziranja) često zvanim mekanim tipiziranjem. Na primer, Java i neki drugi prividno statični kucani jezici podržavaju daunkesting tip za njihove podtipove, upitivanje objekta kako bi se otkrio dinamično tipiziranje, i druge operacije tipiziranja koje zavise na tip rantajm informacije. Opštije, mnogi programski jezici uključuju mehanizme za otpremu nad različitim "tipovima" podataka, kao što su razdovjeni savezi, podtipovi polimorfizma, i varijante vrste. Iako se ne interaguje sa anotacijama tipiziranja ili proverama tipiziranja, ovakvi mehanizmi su materijalno slični dinamičnim implementacijama tipiziranja. Videti programski jezici za više diskusija o interakcijama izmađu statičnog i dinamičnog tipiziranja. 

Objektima u objektno orijentisanim jezicima se obično pristupa preko referenci čiji je statički tip mete (ili tip manifestovanja) jednak ili objektnom rantajm tipu (njegovom tipu latenta) ili njegovom supertipiziranju. Ovo je pravilno po Liskovom principu supstitucije, koja kaže da sve operacije izvršene nad instancom datog tipiziranja se mogu takođe izvršiti nad instancom podtipiziranja. Ovaj koncept je takođe poznat kao stapanje. U nekim jezicima podtipiziranje može takođe posedovati kovarijantna ili kontrakovarijantna povratna tipiziranja i argumentovana tipiziranja odnosno. 

Određeni jezici, na primer Clojure, Common Lisp, ili Cython su dinamično provereni po difoltu, ali dozvoljava programima da pređu i statičnu proveru tipiziranja pružajući opcionalne anotacije. Jedan razlog za korišćenje ovakvih pomoći bi bio da se optimizuje performans kritičnih sekcija programa. Ovo je formalizovano postepenim tipiziranjem. Programsko ogruženje DrScheme, pedagoško okruženje bazirano na Lisp-u, i prethodnih jezika Racket je takođe mekano-kucan. 

S druge strane, kao u verzije 4.0, #S jezik pruža način da pokaže da promenljiva ne bi trebalo da bude statično proverena. Promenljiva čiji je tipdynamic neće biti tema statičnoj proveri tipiziranja. Stoga, program se oslanja na rantajm informaciji tipiziranja da odluči kako se promenljiva može koristiti.

Statična i dinamična provera tipiziranja u praksi

Izbor između statičnog i dinamično tipiziranja zahteva određene komprimise.

Statično tipiziranje može nači greške pri tipiziranju oslanjajući se na kompilatorsko vreme, što bi trebalo da poveća pouzdanost prinetog programa. Međutim, programeri se ne slažu oko toga koliko se često greške pri tipiziranju javljaju, što rezultuje u daljim neslaganjima oko odnosa ovih bagova koji su kodirani da će biti uhvaćeni adekvatno predstavljajući projektovana ukucavanja u kodu. Statično tipiziranja zagovara verovanje da su programi pouzdaniji kada im je dobro provereno tipiziranje, dok dinamično tipiziranje zagovara na distribuirane kodova za koje je dokazano da su pouzdani i za male bagove baza podataka.. Vrednost statičnog tipiziranja, onda , verovatno raste kao što se jačina sistema tipiziranja povećava. Zagovornici zavisno kucanih jezika kao što je Dependent ML i Epigram  su predložili da skoro svi bagovi se mogu smatrati greškama tipiziranja, ako su tipiziranja korišćena u programu dobro deklarisana od strane programera ili tačno zaključena od strane kompilatora. 

Statično tipiziranje obično rezultuje kompiliranom kodu koji se izvršava dosta brže. Kada kompilator zna tačan tip podataka koji se koristi, može da proivede optimizovan mašinski kod. Dalje, kompilatori za statično ukucane jezike mogu nači prečice asemblera mnogo lakše. Neki dinamično ukucani jezici kao što je Common Lisp dozvoljavaju opcionalne deklaracije tipiziranja za optimizaciju zbog ovog razloga. Statično tipiziranje čini ovo prožetim. Videti optimizaciju.

Suprotno, dinamično tipiziranje može dozvoliti kompilatorima da rade mnogo brže i da dozvoli interpretatorima da dinamično učitaju novi kod, pošto promene izvornog koda u dinamčno kucanim jezicima mogu rezultovati manjom proverom za rad i manje koda da se ponavlja. Ovo može takođe smanjiti izmeni-kompiliram-testiraj-debaguj krug.

Statično ukucani jezici kojima fali ukucani zaključak (kao što je S i Java) zahteva da programeri deklarišu tipiziranja koja smatraju metodom ili funkcijom za korišćenje. Ovo može služiti kao dodatna dokumentacija programa, koju kompilator neće dozvoliti programeru da ignoriše ili da dozvoli da se izostavi iz sinhronizacije. Međutim, jezik može biti statičn ukucan bez zahteva deklaracija tipiziranja (primeri uključuju Haskell, Skalu, OCaml, F# i u manjoj meri S# i S++ ), tako da eksplicitno tipiziranje deklaracije nije potreban zahtev za statično tipiziranje u svim jezicima.

Dinamično tipiziranje daje konstrukciju koju neki statični kontroleri tipiziranja ne bi odbili kao ilegalne. Na primer, eval funckije, koji izvršavaju proizvoljan podatak kao kod, postaju mogući. Eval funkcija je moguća statičnim tipiziranjem, ali zahteva napredna korišćenja algebarskih tipova podataka. Dalje, dinamično tipiziranje bolje se prilagođava prelaznom tranzicionalnom kodu i prototipiziranju, kao što je dozvoljavanje čuvaru strukture podataka (lažni objekat) da bude transparentno korišćen umesto punom pokrivenom strukturom podataka (obično za svrhe eksperimentisanja i testiranja).

Dinamično tipiziranje dozvoljava dak tipiziranje (što omogućava lakšu ponovnu upotrebu koda). Mnogi jezici sa statičnim tipiziranjem takođe imaju dak tipiziranje ili druge mehanizme kao generično programiranje koji takođe omogućava lakšu ponovnu upotrebu koda.

Dinamično tipiziranje čini mataprogramiranje lakšim za korišćenje. Na primer, S++ šabloni su tipično glomazniji za tipiziranje nego ekvivalenti Rubijevog ili Pajtonovog koda. Naprednije rantajm konstrukcije kao što su metaklase i samoispitivanje su često mnogo teže za korišćenje u statično ukucanim jezicima. U nekim jezicima, ovakve karakteristike se mogu takođe koristiti tj. da generišu nove tipove i ponašanja pri letu, baziranim na rantajm podacima. Ovakve napredne konstrukcije su često pružene dinamičnim programskim jezicima; mnogi od ovih su dinamčno ukucani, iako je nema potreba da dinamčno tipiziranje bude u odnosu da dinamično programiranim jezicima.

"Jaki" i "slabi" sistemi tipiziranja

Jezici se često kolokvijalno odnose kao "jako ukucani" ili "slabo ukucani". U stvari, ne postoji univerzalno prihvaćena definicija šta ovi termini znače. Uglavnom, postoje precizniji termini koji predstavljaju razliku između sistema tipiziranja koji su doveli ljude da ih nazovu "jakim" ili "slabim". 

Sigurnosno tipiziranje i sigurnosna memorija

Treći način kategorizovanja sistema tipiziranja programskih jezika koristi sigurnost ukucanih operacija i konverzija. Računarski naučnici smatraju jezik "sigurno-ukucanim" ako ne dozvoljava operacije ili konverzije koje krše pravila sistema tipiziranja.

Neki posmatrači koriste termin memorijski-siguran jezik (ili samo siguran jezik) da opišu jezika koji ne dozvoljavaju programima da pristupe memoriji koja nije pripisana za njihovo korišćenje. Na primer, memorijski-siguran jezik je proveriti granice niza, ili će statično garantovati (tj., pri kompiliranom vremenu pre egzekucije) da će ako taj niz izađe iz granica niza prouzrokovati kompilirano-vreme i možda rantajm greške.

Razmotriti sledeći program jezika koji je i sigurnosno-ukucan i memorijski-siguran:

var x := 5;
var y := "37";
var z := x + y;

U ovom primeru, promenljiva z će imati vrednost 42. Iako ovo možda neće biti ono što je programer planirao, to je dobro definisan rezultat. Ako je y drugačiji string, onaj koji ne bi mogao da se prebaci u broj (npr. "Hello World"), rezultat bio bio dobro definisan takođe. Imati na umu da program može biti sigurno-otkucan ili memorijski-siguran i idalje da se zaustavi pri nevladinoj operaciji; u stvari, ako program startuje operaciju koja nije sigurnosno-otkucana, gašenje programa je često jedina opcija. Sada razmotriti sličan primer u S-u:

int x = 5;
char y[] = "37";
char* z = x + y;

U ovom primeru z će pokazati na adresu memorije pet karaktera iznad y, jednako sa tri karaktera posle izvršenja nultog karaktera stringa koji je pokazan od straney. Ovo je memorija za koju se ne očekuje da će program pristupiti. Može sadržati nebitne podatke, i sigurno ne sadrži nešto korisno. Kako ovaj primer pokazuje, S nije ni memorijski-siguran niti je sigurnosno-ukucan jezik.

Uglravnom, sigurnosno-tipiziranje i memorijska-sigurnost idu jedno uz drugo. Na primer, jezik koji podržava aritmetički pokazivač i broj-do-pokazivača konverzije (kao S) nije ni memorijski-siguran niti sigurnosno-otkucan, pošto dozvoljava algebarskoj memoriji da bude pristupljeno kao da je validna memorija bilo kog tipa.

Za više informacija, videti memorijsku sigurnost.

Nivoi promenljivih provere teksta

Neki jezici dozvoljavaju različite nivoe provere kako bi primenili na različite regione koda. Primeri uključuju:

•  use strict direktiva u javaskriptu i Perlu primenjuje jaču proveru. 
•  @ operator u PHP-u potiskuje neke poruke greške
• Option Strict On u VB.NET-u dozvoljava kompilatoru da zahteva konverziju između objekata.

Dodatne alatke kao što su lint i IBM Rational Purify se mogu takođe koristiti za postizanje visokog nivoa ograničenja.

Opcioni sistemi tipiziranja

Preporučeno je, prvenstveno od strane Gilada Brahe, da izbog sistema tipiziranja bude nezavisan od izbora jezika; da sistem tipiziranja treba da bude modul koji može biti "uključen" u jezik ako je traženo. On smatra da je ovo povoljno, zato što ono što on zove obavezni sistemima tipiziranja čini jezik manje izražajnim i kod krhkim.ref>Bracha, G.: Pluggable Types</ref> Zahtevnost kojom tipiziranje ne utiče na semantiku jezika je teško ispuniti, nasleđivanje bazirano na klasi postaje nemoguće.

Opcionalno tipiziranje se odnosi na osnovno tipiziranje, ali idalje je poseban

Polimorfizam i tipiziranje

Termin "polimorfizam" se odnosi na mogućnost koda (tačnije, metode ili klase) da deluje na vrednosti višestrukog tipiziranja, ili mogućnost različitih instanci iste strukture podataka da bi se zadržali elementi različitih tipiziranja. Sistemi tipiziranja koji dozvoljavaju polimorfizam uglavno to rade da bi poboljšali potencijal za ponovno korišćenje koda: u jeziku sa polimorfizmom, programeri moraju samo da implementuju strukturu podataka kao što je lista ili asocijativni niz jednom, više nego jednom za svaki tip element koji planiraju da koriste. Zbog ovog razloka računarski naučnici neki put koriste određene forme polimorfizma, generičko programiranje. Fondacija polimorfizma teoretičkog-tipiziranja su blisko povezani sa tim apstrakcijama, modularnostima i (u nekim slučajevima) podtipiziranjima.

Dak tipiziranje

U "dak tipiziranju", izjava koja poziva metodu m nad objektnom koji se ne oslanja na deklarisan tip objekta, bilokog tipa, mora pružiti implementaciju pozvane metode, kada je pozvana, pri rantajmu.

Dak tipiziranje se razlikuje od strukturnog tipiziranja u tome, ako je "deo" (celog modula strukture) potreban za datu loklanu komputaciju je dostupan u rantajmu, dak sistem tipiziranja je zadovoljen i njegoj analizi identiteta tipiziranja. Sa druge strane, strukturni sistem tipiziranja će zahtevati analizu celog modula strukture pri kompilatorskom vremenu da otkrije identitet tipiziranja ili nezavisnost tipiziranja.

Dak tipiziranje se razlikuje od nominativnog sistema tipiziranja u brojnim aspektima. Najistaknutiji su oni za dak tipiziranje, tip informacija je odlučen prilikom rantajma (što je kontrast kompiliranom vremenu), i ime tipiziranja je irelevantno za odlučivanje identiteta tipiziranja ili zavisnosti tipiziranja; samo parcijalna struktura informacije je potrebna za to za datu tačku u izvršavanju programa.

Dak tipiziranje koristi premisu koja (odnosi se na vrednosti) "ako hoda kao patka, i kvakuće kao patka, onda je patka" (ovo je referenca koja se odnosi na dak test koja se prepisuje Džejmsu Vitkombu Rajliju). Termin je možda skovan od strane  Aleksa Martelija 2000 u poruci  za comp.lang.python grupa vesti (videti Pajton ).

Dok je jedan kontrolisani eksperiment pokazao povećanje kod poizvodnje razvojnika za dak tipiziranje u jednostavnim razvojničkim projektima, ostali kontrolisani eksperimenti nad API korišćenju su pokazali obrnuto.

Specijalizovani sistemi tipiziranja

Mnogi sistemi tipiziranja su kreirani kako bi bili specijalizovani za korišćenje u određenim okruženjima sa određenim tipovima podataka, ili za iz-benda statičnu programsku analizu. Često, ovo je bazirano na idejama iz formalne teorije tipiziranja i dostupne su samo kao prototipi sistema istraživanja.

Zavisna tipiziranja

Zavisna tipiziranja su bazirana na ideji korišćenja skalara ili vrednosti da bi se preciznije opisalo ukucavanje neke druge vrednosti. Na primer, $matrix(3,3)$ može biti tip 3×3 matrice. Možemo definisati pravila tipiziranja kao što je sledeće za množenje matrica:

gde su $k$, $m$, $n$ algebarske pozitivne celobrojne vrednosti. Varijanta ML-a koja se zove Zavisni ML je kreiran bazirajući se na sistem tipiziranja, ali zato što je provera tipiziranja za konvenzionalna zavisna tipiziranja neodlučiva, ne mogu svi programi koji ga koriste da budu provereni bez nekih vrsta ograničenja. Zavisna ML ograničenja, vrsta jednakosti može odličiti za Presburgerovu aritmetiku.

Ostali jezici kao što je Epigram čini vrednost svih ekspresija u jeziku odlučivim tako da provera tipiziranja može biti odlučiva. Međutim, uglavnom dokaz odlučivosti je neodlučiv, mnogo programi zahtevaju ručno-napisane anotacije koje možda nisu trivijalne. Pošto ovo otežava razvoj procesa, mnogo implementacije jezika pružaju lakši način u formu opcije da se isključi ovo stanje. Ovo, međutim, dolazi po ceni da kontrolor-tipiziranja ulazi u beskonačnu petlju kada nahrani programa koji ne proveravaju tipiziranje, što prouzrokuje pad kompilacije.

Linearna tipiziranja

Linearna tipiziranja, bazirana na teoriji linearne logike, su blisko povezani sa sporim tipiziranjima, su tipovima koji su dodeljeni vrednosti i imaju osobinu da imaju samo jednu referencu sve vreme. Ovo je vredno za opisivanje velike nepromenljive vrednosti kao što su fajlovi, stringovi, i tako dalje, zato što svaka operacije koja istovremeno uništava linearni objekat i stvara slični objekat (kao što je 'str = str + "a"') može biti optimizovan "ispod haube" u mutaciju. Normalno ovo nije moguće, pošto ovakve mutacije mogu izazvati neželjene efekte nad delovima programa koji drži ostale reference za objekat, što krši referentnu transparentnost. Takođe se koriste u prototipu operativnog sistema Jedinstvenost za među proces komunikacije, statično se osigurava da procesi ne mogu deliti objekte u podeljenoj memoriji kako bi sprečili trku stanja. Čisti jezik (jezik kao Haskel) koristi sistem tipiziranja da bi dobio na brzini (u odnosu na obavljanje duboke kopije) dok ostaje siguran.

Međusekcije tipiziranja

Međusekcije tipiziranja su tipiziranja koja opisuju vrednosti koje pripadaju obema ostalim datim tipiziranjima sa setovima vrednosti koji se preklapaju. Na primer, u većini implementacija S-a pripisan karakter ima opseg -128 do 127 i nepripisan karakter ima opseg od 0 do 255, tako da tipiziranje međusekcije ova dva tipiziranja će imati opseg od 0 do 127. Ovakva međusekcija tipiziranja se mođe sigurno preći u funckije koje očekuju ili pripisane ili nepripisane karaktere, zato što je kompatibilno sa oba tipiziranja. 

Međusekcijska tipiziranja su korisna za opisivanje prekoračena tipiziranja funkcije: Na primer, ako "int → int" je tip funkcija koje uzimaju celobrojni argument i vraćaju ceo broj, i "float → float" je tip funkcija koje uzimaju decimalni argument i vraćaju decimalni broj, onda međusekcija između ova dva tipiziranja se može koristiti da opiše funkcije koja odrađuje jednu ili drugu, bazirano na tipu izlaza koji je dat. Takva funkcije se može proslediti u drugu funkcije koja  očekuje "int → int" sigurnost funkcije; jednostavno neće koristiti "float → float" funkcionalnost.

U hijerarhiji podklasa, međusekcija tipiziranja i predačko tipiziranje (kao njegov roditelj) je najizvedenije tipiziranje. Međusekcija tipiziranja blizanaca je prazna.

Forsit jezik uključuje generalnu implementaciju međusekcijskog tipiziranja. Ograničena forma prefinjenog tipiziranja.

Sjedinjeno tipiziranje

Sjedinjena tipiziranja su tipiziranja koja opisuju vrednosti koje pripadaju obema tipiziranjima. Na primer, u S-i, pripisani karakter ima od -128 do 127 opseg, i nepripisan karakter ima od 0 do 255 opseg, tako da sjedinjenje ova dva tipiziranja bi imalo opšti "virtuelni" opseg od -128 do 255 koji se može delimično koristiti u zavisnosti od toga koji je član sjedinjenja korišćen. Svaka funkcija koja kontroliše sjedinjeno tipiziranje bi morala da ima posla sa celim brojevima u ovom kompletnom opsegu. Generalnije, jedine validne operacije nad sjedinjenim tipiziranjem su operacije koje su validne nad obema tipiziranjima i koje su sjedinjene. S-ov koncept "sjedinjenja" je sličan sjedinjenim tipiziranjima, ali nije sigurno ukucan, pošto ograničava operacije koje su validne u oba tipiziranja. Sjedinjena tipiziranja su bitna za programsku analizu, gde se koriste da predstave simbolične vrednosti čije pravo poreklo (tj, vrednost ili tip) nije poznato.

U hijerarhiji podklasa, sjedinjeno tipiziranje i tipiziranje predaka (kao što je roditeljsko) je tipiziranje predaka. Sjedinjenje tipiziranja polubrata njihovog čestog predka (to je, sve operacije koje su dozvoljene nad njihovim čestim predkom su dozvoljene nad sjedinjenim tipiziranjem, ali mogu takođe imati ostale validne operacije zajedničke).

Egzistencijalno tipiziranje

Egzistencijalno tipiziranje se često koristi u konekciji sa rekordnim tipiziranje da bi se predstavili moduli i apstraktni tipovi podataka, zbog njihove mogućnosti da odvoje implementacije sa njihovih sučelja. Na primer, tip  "T = ∃X { a: X; f: (X → int); }" opisuje modul sučelja koji ima člana podatka nazvan a od tipa X i funkciju nazvanu f koja uzima parametar istog tipa X i vraća ceo broj. Ovo može biti implementovano na različite načine, na primer: 

• intT = { a: int; f: (int → int); }
• floatT = { a: float; f: (float → int); }

Ova tipiziranja su oba podtipiziranja generalnijeg egzistencijalnog tipa T i odgovara konkretnim implementacijama tipiziranja, tako da bilo koja vrednost jednog od ovih tipiziranja je vrednost tipa T. Data vrednost "t" tipa "T", znamo da "t.f (t.a)" je dobro ukucano, neobraćajući pažnju šta je apstrakti tip H. Ovo daje fleksibilnost u biranju tipiziranja koje odgovaraju delimičnim implementacijama dok klienti koji koriste samo vrednost sučeljnog tipiziranja—egzistencijalno tipiziranje—su odvojeni od ovih izbora.

Uglavnom nemoguće je za kontrolora tipiziranja da zaključi koje egzistencijalno tipiziranje pripada datom modulu. U primeru iznat { a: int; f: (int → int); } može takođe imati tip ∃X { a: X; f: (int → int); }. Najjednostavnije rešenje je zapisati svaki modul sa njegovim namenjenim tipom, tj.:

• intT = { a: int; f: (int → int); } as ∃X { a: X; f: (X → int); }

Iako apstrakti tipovi podataka i modul su implementovani u programske jezike već duže vreme, to nije bilo sve do 1988 kada su Džon C. Mičel i Gordon Plotkin su utvrdili formalnu teoriju pod sloganom: "Apstraktni [podaci] tipovi imaju egzistencijalni tip". Teorija je drugog reda ukucana lambda kalkulusom sličnom Sistemu F, ali sa egzistencijalnom umesto univerzalnom kvantifikacijom.

Postepeno tipiziranje

Postepeno tipiziranje je sistem tipiziranja čije promenljive mogu biti ukucane ili prilikom kompilatorskog vremena (što je statično tipiziranje) ili prilikom rantajma (što je dinamično tipiziranje), dozvoljavajući softverskim razvojnicima da brilaju oba tipa paradigme kao prilagođavajuću, iz jednog jezika. Posebno, postebeno tipiziranje koristi specijalno tipiziranje koje se zove dinamčino da prestavi statično-nepoznata tipiziranja, i postepeno tipiziranje menja pojam jednakosti tipiziranja sa novom relacijom koja se naziva doslednost koja odnosi dinamično tipiziranje na sva ostala tipiziranja. Relacija doslednost je sumetrična ali ne tranzistivna.

Eksplicitna ili implicitna deklaracija i zaključak

Mnogi statični sistemi tipiziranja, kao što su oni u S-u i Javi, zahtevaju deklaraciju tipiziranja. Programer mora eksplicitno pomoći svakoj varijabli sa posebnim tipiziranjem. Ostali, kao što su Haskel, koriste zaključno tipiziranje: Kompilator izvodi zaključke o tipiziranjima promenljivih baziranim na tome kako programeri koriste te promenljive. Na primer, data funckija  f(x, y) koja dodaje x i y zajedno, kompilator može zaključiti da x i y moraju biti brojevi – pošto je adicija samo definisana za brojeve. Zbog toga, svaki poziv na f drugde u programu koji specifikuje ne-brojiv tip (kao što je string ili lista) kao argument bi dao grešku.

Numeričke i konstante string i ekspresije u kodu mogu i često podrazumevaju tipiziranje u određenom kontekstu. Na primer, ekspresija 3.14 može podrazumevati decimalnu tačku, dok [1, 2, 3] može podrazumevati listu celih brojeva - tipično niz.

Tip zaključka je u generalnom moguć, ako je odlučiv u teoriji tipiziranja u pitanju. Štaviše, zak iako je zaključak neodlučiv u generali za datu teoriju tipiziranja, zaključak je često moguć za velike podsetove stvarnih programa. Haskelov sistem tipiziranja, verzija Hindleja-Milnera, je restrikcija Sistema F-omega tako zvanom ranka-1 polimorfnog tipiziranja, u čijem slučaju je zaključak odlučiv. Većina Haskelovih kompilatora dozvoljavaju algebarski-rank polimorfizma kao ekstenziju, ali ovo čini tipiziranje zaključka neodlučivim. (provera tipiziranja je odlučiva, međutim, i rank-1 programi idalje imaju zaključak; polimorfni programi višeg ranka su odbijeni osim ako ne daju eksplicitne zapise)

Tipovi tipiziranja

Tipovi tipiziranja je vrsta. Vrste se pojavljuju eksplicitno u kucanom programiranju, kao što je konstruktor tipiziranja u Haskelovom jeziku.

• Primitivni tip podataka - najjednostavnija vrsta tipiziranja; npr., ceo broj i decimalni broj
  • Bulov tip podataka
  • Integralno tipiziranje - tipiziranje celih brojeva, npr. celi brojevi i prirodni brojevi 
  • – tipiziranje brojeva u decimalnoj reprezentaciji
• tipiziranje reference
• Opciono tipiziranje
  • Nulabl vrste
• Kompozitne vrste – tipiziranja komponovana poreko drugih tipiziranja: npr., nizovi ili rekordi.

  Apstraktni tip podataka

• Algebarsko tipiziranje
• Podtip
• Nasleđivanje
• Objektni tipovi; npr, tipiziranje promenljive
• Delimično tipiziranje
• Rekurzivno tipiziranje
• tipiziranja funkcije; npr., binarne funkcije
• univerzalno kvantifikovana tipiziranja, kao što je parametarsko tipiziranje 
• egzistencijalno kvantifikovana tipiziranja, kao što su moduli
• – tipiziranja koja identifikuju podsetove drugih tipiziranja
• Zavisna tipiziranja - tipiziranja koja zavise od uslova (vrednosti)
• – tipiziranje koje opisuje ili ograničava strukturu objektno-orijentisanih sistema
• Pre-definisana tipiziranja pružena za pogodnost u realnim aplikacijama, kao što je datum, vreme i novac.

Objedinjeni sistem tipiziranja

Neki jezici kao S# imaju objedinjeni sistem tipiziranja. Ovo znači da svi S# tipiovi, uključujući primitivne tipove nasleđivanja iz jednog korenog objekta. Svaki tip u S# nasleđuje klase Objekta. Java ima nekoliko primitivnih tipova koji nisu objekti. Java pruža omotač objektnog tipiziranja koji postoji zajedno sa primitivnim tipiziranjem tako da razvojnici mogu da koriste ili omotač objektnog tipiziranja ili jednostavne ne-objektna primitivna tipiziranja.

Kompatibilnost: jednakost i podtipizoranje

Kontrolor tipova za statično tipizirane jezike mora da proveri da li je tip bilo kog izraza dosledan sa tipiziranjam koje se očekuje od konteksta kod koje se taj izraz pojavljuje. Na primer, u dodeljenoj izjavi forme  x := e, zaključeno tipiziranje ekspresije e mora biti dosledan sa deklarisanim ili zaključenim tipom promenljive x. Ovaj pojam doslednosti, nazvanim kompatibilnost, je specifičan za svaki jezik.

Ako su tipiziranje e i tipiziranje x  isti i dodeljivanje dozvoljeno za to tipiziranje, onda je ovo validna ekspresija. U jednostavnim sistemima tipiziranja, dalje, pitanje da li su dva tipiziranja kompatibilna se smanjuje do te mere da li su jednaki (ili ekvivalentni). Različiti jezici, međutim, imaju različiti kriterijum kada su dva tipa ekspresija razumljiva za označavanje istog tipiziranja. Ove dve teorije jednačina tipiziranja variraju dosta, dva ekstremna slučaja strukturnog tipiziranja sistema, u kome bilo koja dva tipiziranja koja opisuju vrednosti sa istom strukturom su ekvivalentna, i nominativni sistemi tipiziranja, u kojima nijedan od dva sintaksno posebna tipa ekspresija ne označavaju isto tipiziranje (tj., tipiziranja moraju da imaju isto "ime" da bi bili jednaki).

Kod jezika sa podtipiziraem, relacija kompatibilnosti je kompleksnija. Posebno, ako je  A podtip B, onda vrednost tipa A se može koristiti u kontekstu gde je jedan od tipa B očekivan, čak i ako obrnuto nije tačno. Kao jednakost, relacija podtipa je definisana drugačije za svaki jezik programiranja, sa mnogim mogućim varijacijama. Prisustvo parametra ili ad hok polimorfizma u jeziku može takođe imati implikacije za kompatibilnost tipiziranja.

Literatura

• Inc., InfoWorld Media Group (1983). InfoWorld. InfoWorld Media Group, Inc. str. 66. 
• Cardelli, Luca; Wegner, Peter (1985). „On understanding types, data abstraction, and polymorphism”. ACM Computing Surveys. 17 (4): 471—523. S2CID 2921816. doi:10.1145/6041.6042. 
• Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8. 
• Cardelli, Luca . "Type systems". In Allen B. Tucker. CRC Handbook of Computer Science and Engineering (PDF) (2nd ed.). . CRC Press. 2004. ISBN 978-1-58488-360-9. 
• Tratt, Laurence, Dynamically Typed Languages, Advances in Computers, Vol. 77. str. 149–184, July 2009

Spoljašnje veze

• Smith, Chris, What To Know Before Debating Type Systems