Slægt (typeteori)
Slægt i typeteori ( engelsk type [1] ) er typen af en typekonstruktør , eller mere formelt typen af en højere ordens typeoperator . Kønssystemet er naturligt repræsenteret som en forælder (overordnet) simpelthen indtastet lambda-regning , udstyret med en primitiv type, betegnet med " *" (læs " type "), der danner en slags monomorfe datatyper .
Mere tydeligt er en slægt en type typer eller en metatype - ligesom et sæt værdier danner en type , danner et sæt typer en slægt [2] . Samtidig adskiller forekomsten af typer i mere generelle typer (som undertyper) sig fra typens tilhørsforhold til en slægt - opdelingen af forskellige typer i slægter sker på et mere abstrakt niveau. For eksempel er typerne " naturlig ", " heltal " og " virkelig " undertyper af den mere generelle type " tal "; alle fire typer repræsenterer umiddelbare værdier og tilhører derfor slægten " *". Andre slægter er dannet ud fra forskellige operationer på typer , ligesom aritmetikken skelner mellem tal og operationer på tal .
Det ville syntaktisk være naturligt at tænke på alle polymorfe typer som typekonstruktører ; og følgelig er alle monomorfe konstruktører nullær type . Men alle nul-konstruktører, det vil sige alle monomorfe typer, tilhører faktisk den samme slægt, nemlig " *".
Fordi højere ordens typeoperatorer er ualmindelige i de fleste programmeringssprog , bruges køn i programmeringspraksis til at skelne datatyper fra konstruktørtyper , der bruges til at implementere parametrisk polymorfi . Køn optræder eksplicit eller implicit i sprog med komplette typesystemer , såsom Haskell og Scala [3] .
Eksempler
- (læs " type " ) er en slægt af alle monomorfe typer, betragtet som nullære typekonstruktører , også kaldet egentlige typer . Funktionstyper i funktionelle sprog hører også til denne slægt .
- er slægten for alle unære type konstruktører . For eksempel er listetype -konstruktøren list.
- — en slags konstruktører af binær karrytype . For eksempel en partypekonstruktør eller en funktionel typekonstruktør (ikke at forveksle med resultatet af at anvende denne konstruktør, dvs. med selve den funktionelle type, som tilhører slægten " *").
- - en slags typeoperatorer af højere orden , det vil sige operatorer, der modtager unære typekonstruktører ved input og genererer typer selv ved output [4] .
Generisk slutning i Haskell
Haskell giver polymorfe typer, men tillader ikke polymorfe slægter [5] . For eksempel i denne definition af en polymorf algebraisk type
datatræ z = Blad | _ Fork ( træ z ) ( træ z )zkan være af ethvert køn, inklusive “ ”, “ ” osv. Som standard udleder Haskell altid kønnet “ ”, medmindre andet er angivet (se nedenfor). Derfor vil typekonsistenskontrollen afvise følgende forsøg på at bruge type : Tree
type FunnyTree = Træ [] -- fejlfordi typen []er af slægten " ", som ikke er det forventede køn for , som altid er " ". z
Operatører af højere orden er dog tilladt. For eksempel,
data App unt z = Z ( unt z )hører til " " slægten , det vil sige at den skal være en unær konstruktør , men her tager den en type som argument og returnerer en anden type. unt
Se også
- Fω system
- Ren type system
Noter
- ↑ Der er ingen veletableret oversættelse af udtrykket " art " i russisksproget litteratur . Der er sådanne oversættelsesmuligheder som " type ", " sort ", " type "
- ↑ Pierce, 2012 , kapitel 29. Typeoperatører og typer.
- ↑ Generisk af højere slags . Hentet 30. september 2017. Arkiveret fra originalen 10. juni 2012.
- ↑ Pierce, 2012 , kapitel 32. Udvidet eksempel: Rent funktionelle objekter.
- ↑ Haskell dokumentation bruger den samme pil til både funktionstyper og slægter
Litteratur
- Luca Cardelli Typisk programmering( (engelsk)) // IFIP State-of-the-Art-rapporter. - New York: Springer-Verlag, 1991. -Vol. Formel beskrivelse af programmeringskoncepter. —S. 431–507.
- Luca Cardelli , Peter Wegner. Om forståelse af typer, dataabstraktion og polymorfi. -ACM Computing Surveys, 1985. -S. 471-523. —ISSN 0360-0300.
- Pierce, Benjamin C. Typer og programmeringssprog . - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Oversættelse til russisk: Pierce B. Skriver på programmeringssprog. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .
| Datatyper | |
|---|---|
| Ufortolkelig | |
| Numerisk | |
| Tekst | |
| Reference | |
| Sammensatte | |
| abstrakt | |
| Andet | |
| relaterede emner | |