I typeteori er en typekonstruktør en polymorf-typet formel sprogkonstruktion , der konstruerer nye typer ud fra gamle.
Eksempler på typiske typekonstruktører er produkttyper , funktionstyper og lister . Primitive typer er repræsenteret af nularitetstypekonstruktører . Nye typer kan konstrueres ved rekursivt at sammensætte typekonstruktører.
Den enkelt indtastede lambdaregning kan opfattes som et sprog med en enkelt type konstruktør, funktionstypen konstruktør. Karryning gør det muligt at behandle produkttyper i den indtastede lambdaregning som inline.
I det væsentlige er en typekonstruktør en n-ary type operator ( eng. type operator , operator over types), der tager nul eller flere typer som input og returnerer en anden type. Når der anvendes currying n , kan en -ær type operator repræsenteres ved successive anvendelser af unære type operatorer. Derfor kan typeoperatorer opfattes som blot en maskinskrevet lambdaregning , der har en enkelt type, normalt betegnet " *" (læs " type "), som er typen af alle typer i det underliggende sprog, som i dette tilfælde kan kaldes karakteristiske typer for at skelne dem fra typetypeoperatorer i deres egen calculus- genera af typer .
Men at bruge typeoperatorer som begrundelse for en simpelt indtastet lambdaregning er mere end blot en formalisering – det gør højere ordens typeoperatorer mulige (se Genus (typeteori) #Eksempler , polymorfi i højere slægter ). Typeoperatorerne afbildes til den anden akse i lambda-terningen , hvilket resulterer i en enkelt indtastet lambda-regning med typeoperatorer, λ ω . Kombinationen af typeoperatorer med den polymorfe lambdaregning ( system F ) genererer systemet Fω .
Typekonstruktører er meget brugt i typefuld programmering .
I programmeringssprog i ML -familien er en typekonstruktør repræsenteret af en funktion over typer - dvs. en funktion, der tager nogle typer som input og returnerer andre typer. Optimering af compilere udfører disse funktioner statisk, dvs. på kompileringstidspunktet (se f.eks. MLton ).
De klassiske dialekter af ML ( Standard ML , OCaml ) bruger tuplen notation for konstruktører af -ary type . Curried type konstruktører er mulige i Haskell . Klassiske dialekter af ML bruger postfix-syntaks (for eksempel " ”), når de konstruerer nye typer , mens Haskell bruger præfikssyntaks (“ ”). int listList Int
I moderne implementeringer af Standard ML defineres primitive typer såsom char, int, word, real, i standardbiblioteksmoduler ( SML Basis ) som nullære typekonstruktører (se ML's cifferkontrol for detaljer ). Sådanne klassiske aggregattyper som arrays og lister er implementeret på samme måde, men er allerede unære typekonstruktører vector(arrays af uforanderlige elementer), array(arrays af mutable elementer) og list.
I Standard ML er der to forskellige konstruktioner til at definere typekonstruktører - typeog datatype. Den første definerer et alias for en eksisterende typekonstruktør eller deres sammensætning, den anden introducerer en ny algebraisk datatype med sine egne konstruktører . Nydefinerede typekonstruktører kan tage et hvilket som helst antal argumenter. En typevariabel bruges som argument til typekonstruktøren . Typer parametriseret med et eller flere argumenter kaldes polymorfe ; typer uden argumenter er monomorfe.
datatype t0 = T af int * reel (* 0 argumenter *) type ' a t1 = ' a * int (* 1 argument *) datatype ( ' a , ' b ) t2 = A | B af typen ' a * ' b (* 2 argumenter *) ( ' a , ' b , ' c ) t3 = ' a * ( ' b -> ' c ) (* 3 argumenter *)Der er fire typekonstruktører defineret her: t0, t1, t2og t3. For at oprette objekter af typer 'a t1og , 'a t2skal du kalde deres konstruktører T og A.B
Et eksempel på sammensætning af typekonstruktører, der viser konstruktionen af nye typer:
type t4 = t0 t1Her bruges typen som den faktiske værdi af typevariablen 'a for typekonstruktøren . Den resulterende type er en tupel af to elementer, hvoraf den anden er et heltal, og den første blev konstrueret ved at anvende konstruktøren til en tupel af et heltal og et reelt tal. t1t0 T
Mere komplekst eksempel:
skriv ' a t5 = ( ' a , ' a , ' a ) t3 t1Typeobjekter t5vil være tupler af to elementer, hvoraf det første er et specialtilfælde af typen t3, hvor alle tre argumenter skal være identiske, og det andet er et heltal.
Haskell har allerede tre konstruktioner til at definere typekonstruktører - type, dataog newtype.
Konstruktionerne typeog databruges på samme måde i typeStandard ML , dog er der følgende forskelle: datatype
Eksempel:
dataPoint a = Pt a a _Faktisk er typekonstruktører og værdikonstruktører på alle sprog i ML -familien i forskellige navnerum, så den samme identifikator kan bruges i sådanne tilfælde:
data Punkt a = Punkt a aBrug af en algebraisk type har en vis ydeevne overhead, da værdikonstruktøren anvendes dynamisk. Udskiftning af den med et typealias (defineret via type) forbedrer effektiviteten, men reducerer typesikkerheden (fordi det bliver umuligt at kontrollere de unikke egenskaber af den overbyggede type, der indsnævrer dens anvendelse i forhold til den underliggende type). For at løse dette dilemma tilføjede Haskell en konstruktion newtype:
nytype Punkt a = Punkt ( a , a )En type defineret på denne måde kan have én og kun én værdikonstruktør med præcis én parameter. I kildekoden bruges sådanne typer identisk med dem, der er defineret via data, hvilket giver typesikkerhed. Den eksisterer dog ikke som en separat enhed i den eksekverbare kode newtype, i stedet bruges typen af dens konstruktørparameter. I dette tilfælde vil den eksekverbare kode for operationer med Point avære lige så effektiv som koden for operationer med tuples (a, a).
| Datatyper | |
|---|---|
| Ufortolkelig | |
| Numerisk | |
| Tekst | |
| Reference | |
| Sammensatte | |
| abstrakt | |
| Andet | |
| relaterede emner | |