Genus (typteori)
Genus i typteori ( engelsk typ [1] ) är typen av en typkonstruktör , eller mer formellt, typen av en typoperator av högre ordning . Genussystemet representeras naturligt som en förälder (överlägsen) enkelt typad lambda-kalkyl , utrustad med en primitiv typ, betecknad med " *" (läs " typ "), som bildar ett slags monomorfa datatyper .
Mer tydligt är ett släkte en typ av typer , eller en metatyp - precis som en uppsättning värden bildar en typ , bildar en uppsättning typer ett släkte [2] . Samtidigt skiljer sig förekomsten av typer i mer generella typer (som undertyper) från typens tillhörighet till ett släkte - uppdelningen av olika typer i släkten sker på en mer abstrakt nivå. Till exempel är typerna " naturligt ", " heltal " och " riktigt " undertyper av den mer allmänna typen " tal "; alla fyra typerna representerar omedelbara värden och tillhör därför släktet " *". Andra släkten bildas av olika operationer på typer , precis som aritmetiken skiljer mellan tal och operationer på tal .
Det vore syntaktisk naturligt att tänka på alla polymorfa typer som typkonstruktörer ; och följaktligen är alla monomorfa konstruktörer av nolltyp . Men alla nollkonstruktorer, det vill säga alla monomorfa typer, tillhör faktiskt samma genus, nämligen " *".
Eftersom typoperatorer av högre ordning är ovanliga i de flesta programmeringsspråk , används kön i programmeringspraktik för att skilja datatyper från konstruktortyper som används för att implementera parametrisk polymorfism . Kön förekommer explicit eller implicit i språk med kompletta typsystem , såsom Haskell och Scala [3] .
Exempel
- (läs " typ " ) är ett släkte av alla monomorfa typer, betraktade som nullära typkonstruktörer , även kallade riktiga typer . Funktionstyper i funktionella språk tillhör också detta släkte .
- är släktet för alla unära typkonstruktörer . Till exempel är listtypens konstruktor list.
- — ett slags binära konstruktörer av currytyp . Till exempel en partypkonstruktor eller en funktionell typkonstruktor (inte att förväxla med resultatet av att tillämpa denna konstruktor, det vill säga med själva funktionstypen, som tillhör släktet " *").
- - en sorts typoperatorer av högre ordning , det vill säga operatorer som tar emot unära typkonstruktörer vid ingången och själva genererar typer vid utgången [4] .
Generisk slutledning i Haskell
Haskell tillhandahåller polymorfa typer, men tillåter inte polymorfa släkten [5] . Till exempel i denna definition av en polymorf algebraisk typ
dataträd z = Blad | _ Gaffel ( Tree z ) ( Tree z )zkan vara av vilket kön som helst, inklusive " ", " ", etc. Som standard härleder Haskell alltid könet " ", om inte annat anges (se nedan). Därför kommer typkonsistenskontrollen att avvisa följande försök att använda typ : Tree
typ FunnyTree = Träd [] -- feleftersom typen []är av släktet " ", vilket inte är det förväntade könet för , vilket alltid är " ". z
Operatörer av högre ordning är dock tillåtna. Till exempel,
data App unt z = Z ( unt z )tillhör släktet " " , det vill säga det måste vara en unär konstruktor , men här tar den en typ som argument och returnerar en annan typ. unt
Se även
- Fω system
- System av ren typ
Anteckningar
- ↑ Det finns ingen väletablerad översättning av termen " snäll " i ryskspråkig litteratur . Det finns översättningsalternativ som " snäll ", " sortera ", " typ "
- ↑ Pierce, 2012 , kapitel 29. Typoperatörer och typer.
- ↑ Generisk av ett högre slag . Hämtad 30 september 2017. Arkiverad från originalet 10 juni 2012.
- ↑ Pierce, 2012 , kapitel 32. Utökat exempel: Rent funktionella objekt.
- ↑ Haskell-dokumentationen använder samma pil för både funktionstyper och släkten
Litteratur
- Luca Cardelli Typisk programmering( (engelska)) // IFIP State-of-the-Art-rapporter. - New York: Springer-Verlag, 1991. -Vol. Formell beskrivning av programmeringskoncept. —S. 431–507.
- Luca Cardelli , Peter Wegner. Om att förstå typer, dataabstraktion och polymorfism. -ACM Computing Surveys, 1985. -S. 471-523. —ISSN 0360-0300.
- Pierce, Benjamin C. Typer och programmeringsspråk . - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Översättning till ryska: Pierce B. Typer i programmeringsspråk. - Dobrosvet , 2012. - 680 sid. — ISBN 978-5-7913-0082-9 .
| Datatyper | |
|---|---|
| Otolkbart | |
| Numerisk | |
| Text | |
| Referens | |
| Sammansatt | |
| abstrakt | |
| Övrig | |
| Relaterade ämnen | |