Et typesystem er et sæt regler i programmeringssprog, der tildeler egenskaber, kaldet typer , til de forskellige konstruktioner, der udgør et program , såsom variabler , udtryk , funktioner eller moduler . Typesystemets hovedrolle er at reducere antallet af fejl i programmer [1] ved at definere grænseflader mellem forskellige dele af programmet og derefter kontrollere konsistensen af disse deles interaktion. Denne kontrol kan ske statisk ( på kompileringstidspunktet ) eller dynamisk ( ved kørsel) og også være en kombination af begge.
Ifølge Pierce er typesystemet en afgørlig syntaktisk metode til at bevise fraværet af visse programadfærd ved at klassificere konstruktioner i henhold til den slags beregnede værdier [2] .
Et eksempel på et simpelt typesystem kan ses i C -sproget . Dele af et C-program skrives som funktionsdefinitioner . Funktioner kalder hinanden. En funktions grænseflade angiver navnet på funktionen og en liste over værdier, der sendes til dens krop. Den kaldende funktion postulerer navnet på den funktion, den ønsker at kalde, og navnene på de variable, der indeholder de værdier, den ønsker at videregive. Under programafvikling placeres værdier i et midlertidigt lager, og derefter sendes eksekveringen til kroppen af den kaldte funktion. Den kaldede funktionskode tilgår og bruger værdierne. Hvis instruktionerne i en funktions krop er skrevet med den antagelse, at en heltalsværdi skal sendes til dem til behandling, men den kaldende kode bestod et flydende kommatal, så vil den kaldte funktion evaluere det forkerte resultat. C-kompileren kontrollerer de definerede typer for hver variabel, der overføres, mod de typer, der er defineret for hver variabel i grænsefladen til den kaldte funktion. Hvis typerne ikke stemmer overens, genererer compileren en kompileringsfejl.
Teknisk set tildeler typesystemet en type til hver beregnet værdi og forsøger derefter, ved at holde styr på rækkefølgen af disse beregninger, at kontrollere eller bevise, at der ikke er nogen typetilpasningsfejl . Det specifikke typesystem kan bestemme, hvad der forårsager en fejl, men normalt er målet at forhindre operationer, der antager bestemte egenskaber ved deres parametre, i at modtage parametre, som disse operationer ikke giver mening - at forhindre logiske fejl . Derudover forhindrer det også hukommelsesadressefejl .
Typesystemer er normalt defineret som en del af programmeringssprog og indbygget i deres tolke og compilere. Sprogets typesystem kan dog udvides med specielle værktøjer , der udfører yderligere kontroller baseret på den originale skrivesyntaks i sproget.
Compileren kan også bruge en statisk værditype til at optimere lagring og til at vælge en algoritmisk implementering af operationer på den værdi. For eksempel er en type i mange C-compilere repræsenteret af float 32 bit i henhold til IEEE-specifikationen for enkeltpræcisions flydende kommaoperationer . Baseret på dette vil et særligt sæt mikroprocessorinstruktioner blive brugt til værdier af denne type (addition, multiplikation og andre operationer).
Antallet af restriktioner, der pålægges typer, og hvordan de beregnes, bestemmer sprogets indtastning. Derudover, i tilfælde af type polymorfi , kan sproget også specificere for hver type driften af forskellige specifikke algoritmer. Studiet af typesystemer er teorien om typer , selvom et bestemt typesystem i et programmeringssprog i praksis er baseret på funktionerne i computerarkitekturen, implementeringen af compileren og det generelle billede af sproget.
Den formelle begrundelse for typesystemer er typeteori . Et programmeringssprog inkluderer et typesystem til at udføre typekontrol på kompileringstidspunktet eller ved kørselstidspunktet , der kræver eksplicitte typeerklæringer eller udleder dem alene. Mark Manasse formulerede problemet som følger [3] :
Hovedproblemet, som typeteori løser, er at sikre, at programmer giver mening. Hovedproblemet med typeteori er, at meningsfulde programmer muligvis ikke opfører sig efter hensigten. Konsekvensen af denne spænding er søgen efter mere kraftfulde typesystemer.
Originaltekst (engelsk)[ Visskjule] Det grundlæggende problem, som en typeteori behandler, er at sikre, at programmer har mening. Det grundlæggende forårsaget af en typeteori er, at meningsfulde programmer måske ikke tilskrives problembetydninger. Jagten på systemer af rigere type er resultatet af denne spænding. — Mark Massey [3]Typetildelingsoperationen, kaldet typing, giver mening til strenge af bit , såsom en værdi i computerhukommelsen , eller objekter , såsom en variabel . Computeren har ingen mulighed for at skelne f.eks. en adresse i hukommelsen fra en kodeinstruktion eller et tegn fra et heltal eller et flydende tal , da bitstrengene, der repræsenterer disse forskellige betydninger, ikke har nogen åbenlyse funktioner, der gør det muligt at lave antagelser om deres betydning. Tildeling af typebits til strenge giver denne forståelighed, hvilket gør den programmerbare hardware til et tegnsystem bestående af den hardware og software.
Processen med typekontrol og begrænsning - typekontrol eller typekontrol - kan udføres enten på kompileringstidspunktet statisk typning) eller ved runtime (dynamisk typning). Mellemløsninger er også mulige (jf . sekventiel indtastning ).
Hvis sprogspecifikationen kræver, at indtastningsreglerne er strengt implementeret (dvs. kun tillader i en eller anden grad de automatiske typekonverteringer, der ikke mister information), kaldes et sådant sprog stærkt indtastet ; ) , ellers svagt skrevet . Disse vilkår er betingede og bruges ikke i formelle begrundelser.
Et sprog kaldes indtastet, hvis specifikationen af hver operation definerer de datatyper, som denne operation kan anvendes på, hvilket betyder, at den ikke kan anvendes på andre typer [4] . For eksempel er de data, som " denne citerede tekst " repræsenterer , af typen " строка". I de fleste programmeringssprog giver det ikke mening at dividere et tal med en streng, og de fleste moderne sprog vil afvise et program, der forsøger at udføre en sådan operation. På nogle sprog vil en meningsløs operation blive opdaget under kompilering ( statisk skrivning ), og afvist af compileren. I andre vil det blive opdaget under kørsel ( dynamisk indtastning ), hvilket medfører en undtagelse .
Et særligt tilfælde af maskinskrevne sprog er enkelttypesprog ( eng. single-type language ), det vil sige sprog med en enkelt type. Disse er normalt script- eller markupsprog , såsom REXX og SGML , hvis eneste datatype er tegnstrengen, der bruges til at repræsentere både tegn- og numeriske data.
Utypede sprog, i modsætning til maskinskrevne, giver dig mulighed for at udføre enhver operation på alle data, som i dem er repræsenteret af kæder af bits af vilkårlig længde [4] . De fleste assemblersprog er utypelige . Eksempler på utypede sprog på højt niveau er BCPL , BLISS , Forth , Refal .
I praksis kan få sprog betragtes som maskinskrevne i form af typeteori (at tillade eller afvise alle operationer), de fleste moderne sprog tilbyder kun en vis grad af maskinskrivning [4] . Mange industrisprog giver muligheden for at omgå eller bryde typesystemet, hvilket udligner typesikkerhed for bedre kontrol over programudførelse ( indtastning af ordspil ).
Udtrykket "polymorfi" refererer til kodes evne til at køre på værdier af mange forskellige typer, eller evnen af forskellige forekomster af den samme datastruktur til at indeholde elementer af forskellige typer. Nogle typesystemer tillader polymorfi potentielt at forbedre genbrug af kode : i sprog med polymorfi behøver programmører kun at implementere datastrukturer såsom en liste eller et associativt array én gang og behøver ikke at udvikle en implementering for hver type element, de planlægger. at opbevare strukturer. Af denne grund omtaler nogle dataloger nogle gange brugen af visse former for polymorfi som " generisk programmering ". Begrundelserne for polymorfi fra et typeteoretisk synspunkt er praktisk talt de samme som for abstraktion , modularitet , og i nogle tilfælde data subtyping .
Der er udviklet en række specialtypesystemer til brug under visse forhold med visse data, samt til statisk analyse af programmer. For det meste er de baseret på ideerne om formel typeteori og bruges kun som en del af forskningssystemer.
Eksistentielle typer, dvs. typer defineret af en eksistentiel kvantifier (eksistenskvantifier) , er en indkapslingsmekanisme på typeniveau : det er en sammensat type, der skjuler implementeringen af en type i sin sammensætning.
Begrebet en eksistentiel type bruges ofte i forbindelse med begrebet en registreringstype til at repræsentere moduler og abstrakte datatyper på grund af deres formål med at adskille implementering fra grænseflade. For eksempel T = ∃X { a: X; f: (X → int); }beskriver en type en modulgrænseflade (familier af moduler med samme signatur), der har en dataværdi af typen Xog en funktion, der tager en parameter af nøjagtig samme type Xog returnerer et heltal. Implementeringen kan være anderledes:
Begge typer er undertyper af den mere generelle eksistentielle type Tog svarer til konkret implementerede typer, så enhver værdi, der hører til en af dem, hører også til type T. Hvis t er en værdi af type T, så t.f(t.a)består den typekontrol, uanset hvilken abstrakt type den tilhører X. Dette giver fleksibilitet til at vælge de typer, der er passende for en bestemt implementering, da eksterne brugere kun får adgang til værdierne af grænsefladetypen (eksistentiel) og er isoleret fra disse variationer.
Generelt kan typekonsistenskontrollen ikke afgøre, hvilken eksistentiel type et givent modul tilhører. I eksemplet ovenfor intT { a: int; f: (int → int); }kunne den også have type ∃X { a: X; f: (int → int); }. Den enkleste løsning er eksplicit at specificere for hvert modul den underforståede type i det, for eksempel:
Selvom abstrakte datatyper og moduler har været brugt i programmeringssprog i lang tid, blev en formel model af eksistentielle typer først bygget i 1988 [5] . Teorien er en andenordens type lambdaregning svarende til System F , men med eksistentiel kvantificering i stedet for universel kvantificering .
Eksistentielle typer er eksplicit tilgængelige som en eksperimentel udvidelse af Haskell-sproget , hvor de er en speciel syntaks, der giver dig mulighed for at bruge en typevariabel i en algebraisk typedefinition uden at flytte den ind i signaturen af en typekonstruktør , dvs. uden at øge dens aritet [ 6] . Java-sproget giver en begrænset form for eksistentielle typer gennem jokertegnet . I sprog, der implementerer klassisk ML - stil lad-polymorfi , kan eksistentielle typer simuleres ved hjælp af såkaldte " typeindekserede værdier " [7] .
Mange statiske typesystemer, såsom dem i C og Java, kræver en typedeklaration : programmøren skal udtrykkeligt tildele en specifik type til hver variabel. Andre, såsom Hindley-Milner-typesystemet, der bruges i ML og Haskell , gør typeinferens : compileren udleder typerne af variabler baseret på, hvordan programmøren bruger disse variable.
For en funktion f(x,y), der udfører addition xog y, kan compileren for eksempel udlede, at xog yskal være tal - da additionsoperationen kun er defineret for tal. Derfor signalerer kald af en funktion et sted i programmet ffor andre parametre end numeriske (for eksempel for en streng eller en liste) en fejl.
Numeriske og strengkonstanter og udtryk udtrykker normalt ofte en type i en bestemt kontekst. For eksempel kan et udtryk 3.14betyde et reelt tal , mens det [1,2,3]kan være en liste over heltal - normalt en matrix .
Generelt er typeslutning mulig, hvis den grundlæggende kan afgøres i typeteori. Desuden, selvom inferens er uafgørlig for en given typeteori, er inferens ofte mulig for mange rigtige programmer. Haskell - typesystemet , som er en variation af Hindley-Milner -systemet , er en begrænsning af Fω-systemet til såkaldte førsterangs polymorfe typer, hvorpå det kan afgøres. Mange Haskell-kompilere giver polymorfi med vilkårlig rangering som en udvidelse, men dette gør typeinferens uafgørlig, så eksplicit typeerklæring er påkrævet. Typekonsistenskontrol kan dog stadig afgøres, og for programmer med førsterangs polymorfi kan typer stadig udledes.
Nogle sprog, såsom C# , har et samlet typesystem [8] . Det betyder, at alle typer sprog, op til de primitive , er nedarvet fra et enkelt rodobjekt (i tilfælde af C#, fra klassen Object). Java har flere primitive typer, der ikke er objekter. Sammen med disse leverer Java også wrapper-objekttyper, så udvikleren kan bruge de primitive eller objekttyper, som de finder passende.
Typekonsistenskontrolmekanismen i et statisk skrevet sprog kontrollerer, at ethvert udtryk stemmer overens med den type, der forventes af konteksten, hvori det forekommer. I en typetildelingssætning skal den type , der er udledt for udtrykket , matche den type, der er erklæret eller udledt for variablen . Overensstemmelsesnotationen, kaldet kompatibilitet , er specifik for hvert sprog. x := eex
Hvis eog xer af samme type, og tildeling er tilladt for den type, så er udtrykket lovligt. Derfor forenkles spørgsmålet om kompatibilitet mellem to typer i de simpleste typesystemer til spørgsmålet om deres lighed ( ækvivalens ). Forskellige sprog har dog forskellige kriterier for at bestemme typekompatibiliteten af to udtryk. Disse teorier om ækvivalens varierer mellem to yderpunkter: strukturelle typesystemer , hvor to typer er ækvivalente, hvis de beskriver den samme interne struktur af en værdi ; og nominative typesystemer , hvor syntaktisk forskellige typer aldrig er ækvivalente ( dvs. to typer er kun lige, hvis deres identifikatorer er ens) .
På sprog med undertyper er kompatibilitetsreglerne mere komplekse. Hvis f.eks. er en undertype af , så kan en værdi af type bruges i en kontekst, der forventer en værdi af type , selvom det modsatte ikke er sandt. Som med ækvivalens varierer undertypeforhold på tværs af sprog, og mange variationer af reglerne er mulige. Tilstedeværelsen af parametrisk eller situationel polymorfi i et sprog kan også påvirke typekompatibilitet. ABAB
Nogle programmører foretrækker statiske systemer, andre foretrækker dynamiske . Statisk indtastede sprog signalerer typekonsistensfejl på kompileringstidspunktet , kan generere mere effektivt eksekverbar kode, og for sådanne sprog er mere relevant færdiggørelse i IDE'er mulig . Tilhængere af dynamisk maskinskrivning hævder, at de er bedre egnede til hurtig prototyping , og at typematchningsfejl kun er en lille brøkdel af de potentielle fejl i programmer [9] [10] . På den anden side, i statisk indtastede sprog, er eksplicit typedeklaration normalt ikke påkrævet, hvis sproget understøtter typeinferens , og nogle dynamisk indtastede sprog udfører runtime-optimeringer [11] [12] , ofte gennem brug af delvis type slutning [13] .
| Datatyper | |
|---|---|
| Ufortolkelig | |
| Numerisk | |
| Tekst | |
| Reference | |
| Sammensatte | |
| abstrakt | |
| Andet | |
| relaterede emner | |