Typ variabel

En typvariabel ( typvariabel ) i programmeringsspråk och typteori  är en variabel som kan ta ett värde från en uppsättning datatyper .

En typvariabel används i en algebraisk datatypsdefinition på samma sätt som en parameter används i en funktionsdefinition , men används för att skicka en datatyp utan att skicka själva data. Grekiska tecken används traditionellt som identifierare för typvariabler i typteorin (även om många programmeringsspråk använder det latinska alfabetet och tillåter längre namn).

Exempel

I följande definition av den polymorfa typen " lista " i Standard ML är identifieraren 'a(uttalas "alfa") en variabel av typen [2] :

datatyp 'a list = noll | :: av 'a * 'en lista

När du använder denna polymorfa typ ersätts en specifik typ i typvariabeln, så att många monomorfa typer kan bildas i programmet: string list, int list, int list listoch så vidare. Med denna substitution ersätts varje referens till en typvariabel med samma typ. Den resulterande typinformationen används för att verifiera och optimera programmet, varefter det vanligtvis raderas, så att samma målkod behandlar objekt av initialt olika typer (men det finns undantag från denna regel, särskilt i MLton ).

Om en polymorf typ parametriseras av flera typvariabler, kan de typer som ersätts med dem vara antingen olika eller identiska, men substitutionsregeln respekteras. Om den här typen till exempel är:

datatyp ( 'a , 'b ) t = Singel av 'a | Dubbel av 'a * 'a | Par av 'a * 'b

instansiera så här:

typ t_ir = ( int , real ) t

då Single(4), Double(4,5)och Pair(4,5.0)kommer att vara giltiga värden av typen t_ir, och ett försök att konstruera ett värde Single(5.0)kommer att resultera i ett skrivfel eftersom parametern 'ahar värdet " int".

Länkning och kvantifiering

Omfattningen av varje typvariabel är knuten till ett specifikt sammanhang [3] [4] . I följande exempel används identifieraren 'aoberoende i två signaturer, vilket innebär att den inte kräver likhet av faktiska inline-typer mellan definitioner:

val foo : 'a -> 'a val bar : 'a -> 'a

Detta blir tydligt när du använder explicit bindning ( explicit scoping eller explicit bounding ) typvariabel:

val foo : [ 'a ] 'a -> 'a val bar : [ 'a ] 'a -> 'a

En bindning begränsar omfattningen av en given typvariabel.

I klassiska dialekter av ML är explicit bindning av typvariabler en valfri funktion och de flesta implementeringar stöds inte eftersom onödig bindning i dem är implicit i typdeduktion , vilket blir möjligt på grund av begränsningarna i tidiga versioner av Hindley-Milner-systemet . I hela systemet F skrivs denna deklaration som . En sådan notation kallas prenex normalform . Den stora bokstaven i denna post betyder funktionen för typlagret ( typnivåfunktion ), vars parameter är typvariabeln. Efter att ha ersatt en specifik typ i denna variabel returnerar denna funktion en monomorf värdenivåfunktion ( värdenivåfunktion ). En prenex är en explicit bindning av en typvariabel med prefix till en typsignatur. Tidiga versioner av Hindley-Milner-systemet tillät endast prenex-formen, det vill säga de krävde att en typvariabel instansierades med ett specifikt värde innan ett funktionsanrop behövdes. Denna begränsning kallas prenex-polymorfism  - den förenklar inte bara mekanismen för typmatchning avsevärt , utan gör det också möjligt att sluta sig till alla eller nästan alla (beroende på dialekt) typer i programmet.

Den enklaste bindningen av typvariabler kallas deras kvantifiering . Två fall sticker ut:

  • verkan av en typvariabel sträcker sig till hela typdefinitionen: ['a, 'b] 'a -> 'b -> 'a, matematiskt skrivs en sådan typ genom den universella kvantifieraren - - därför kallas en sådan typvariabel "universellt kvantifierad", och hela typen kallas "universellt polymorf";
  • effekten av en typvariabel sträcker sig bara till en del av typdefinitionen: ['a] 'a -> (['b] 'b -> 'a), matematiskt skrivs en sådan typ genom den existentiella kvantifieraren - - därför kallas en sådan variabel "existentiellt kvantifierad", och hela typen kallas "existentiell".

Att "förvandla" en universellt polymorf typ till en existentiell typ ger inte i alla fall en praktisk typ eller märkbara skillnader från universell polymorfism, men i vissa fall höjer användningen av existentiella typer den parametriska polymorfismen till en förstklassig nivå, d.v.s. tillåter polymorfa funktioner att skickas utan bindning som parametrar till andra funktioner (se första klass polymorfism ). Ett klassiskt exempel är den heterogena listimplementeringen (se wikibok). Explicit anteckning av typer i detta fall blir obligatorisk, eftersom typinferens för polymorfism över rang 2 är algoritmiskt obestämbar [5] .

I praktiken ger universellt polymorfa typer en generalisering av datatypen , och existentiella typer - abstraktionen av datatypen [6] .

Haskell särskiljer flera lägen (tillgängliga som språktillägg): läget Rank2Types tillåter endast vissa former av existentiella typer som öppnar polymorfism inte högre än rang 2, för vilken typinferens fortfarande kan avgöras; läget RankNTypes tillåter att den universella kvantifieraren ( forall a) flyttas in i funktionstyper som är en del av mer komplexa signaturer [7] , läget ImpredicativeTypes tillåter godtyckliga existentiella typer [8] .

OKaml implementerar stöd för existentiell kvantifiering genom en lösning som kallas "lokalt abstrakta typer" [ 9 ] .

Standard ML -specifikationen definierar en speciell kvantifiering för vissa inbyggda operationer. Dess syntax är inte reglerad och skiljer sig i språkimplementationer (oftast är den helt enkelt dold). Till exempel kan signaturen för den inbyggda tilläggsoperationen förenklas enligt följande:

val + : [ int , ord , verklig ] 'a * 'a -> 'a

Denna semantik implementerar en primitiv form av ad-hoc polymorfism  - kombinerar flera fysiskt olika additionsoperationer under en enda identifierare " +". Utvecklarna av OCaml övergav denna lösning genom att helt ta bort ad-hoc polymorfism från språket ( generaliserade algebraiska datatyper dök upp i senare versioner ).

I slutet av 1980 -talet dök Hindley-Milner- förlängningen upp , som gav möjligheten att vid behov begränsa värdeintervallet för vilken typvariabel som helst i nydefinierade typer av typklasser . En typklass begränsar de tillåtna skrivkontexterna mer strikt , vilket gör att en typvariabel endast kan instansieras av typer som tillhör en explicit specificerad klass.

Denna förlängning implementerades först i kärnan av Haskell-språket , till exempel har jämlikhetsjämförelseoperatorn följande signatur i sig :

( == ) :: ( Ekv a ) => a -> a -> Bool

Projektet för nästa generations språk - efterföljaren ML [1]  - vägrar behovet av typinferens , och förlitar sig på explicit (manifest) typannotering (inklusive explicit bindning av typvariabler), som ger direkt stöd för hela systemet F med första- klasspolymorfism och ett antal förlängningar, inklusive hierarkier av subtyper och existentiella typer [1] .

Specialtypvariabler

Huvudklassen av typvariabler som används i alla språk i ML -familjen är applikativa typvariabler som kan ta värden från uppsättningen av alla typer som är tillåtna på ett visst språk. I klassiska dialekter betecknas de syntaktisk som " 'a" (en alfanumerisk identifierare, som alltid börjar med en enda apostrof ); i Haskell som " a" (en alfanumerisk identifierare som alltid börjar med en liten bokstav).

Genom MLs historia har dessutom speciella underklasser av typvariabler urskiljts.

Variabler av en typ som kan kontrolleras för likhet (eller variabler av jämförbar typ, likhetstypvariabler ) - kan ta värden från uppsättningen av alla typer som kan kontrolleras för likhet ( engelska  likhetstyper ). Deras användning gör att jämlikhetsjämförelsen kan tillämpas på objekt av polymorfa typer. De betecknas som " ''a" (alfanumerisk identifierare, börjar alltid med två apostrofer ). Intressant nog var ett av de ursprungliga målen för vilka typklasser utvecklades just generaliseringen av sådana typvariabler från Standard ML [10] . De har upprepade gånger kritiserats på grund av den betydande (och utan tvekan motiverade) kompliceringen av definitionen av språket och implementeringen av kompilatorer (halva sidorna i definitionen innehåller en eller annan ändring av dem) [11] . I princip är det inte tillrådligt att kontrollera komplexa abstrakta datatyper för jämlikhet, eftersom sådana kontroller kan ta avsevärd tid. Därför togs stödet för variabler av en typ som tillåter jämställdhetstestning bort från senare språk i ML- familjen. Haskell använder istället typklassen Eq a .

Imperativa typvariabler gav en ad hoc-lösning på typsäkerhetsproblemet i samband med biverkningar på ett språk med parametrisk polymorfism . Detta problem uppstår inte i rena språk ( Haskell , Clean ), men för orena språk ( Standard ML , OCaml ) utgör referenspolymorfism ett hot om skrivfel [3] [4] . Variabler av imperativ typ var en del av SML'90-definitionen, men upphörde att ha sin egen betydelse efter att " värdebegränsningen " myntades , som blev en del av den reviderade SML'97-definitionen. Syntaktisk stöd för variabler av imperativtyp i SML'97 bibehölls för bakåtkompatibilitet med tidigare skriven kod, men moderna implementeringar behandlar dem identiskt med applikativa. Betecknas med " '_a" (en alfanumerisk identifierare, som alltid börjar med en apostrof och ett understreck) [3] .

Variabler av svag typ användes i SML/NJ-kompilatorn som ett alternativ till imperativa typvariabler, vilket gav mycket mer kraft (mer exakt, mindre restriktioner). Betecknas med " '1a", " '2a" och så vidare (en alfanumerisk identifierare, som alltid börjar med en apostrof och ett nummer). Siffran omedelbart efter apostrof indikerade gradationen av "svaghet" för typvariabeln. Precis som variabler av imperativtyp behandlas de nu identiskt med applikativa. [3]

Anteckningar

  1. ↑ 1 2 3 ML2000, 1999 .
  2. ↑ Här, för explicit bindning ( explicit bindning ) en typvariabel, används den nuvarande syntaxen som antogs i det efterföljande ML- projektet [1] : ['a]. Eftersom Haskell betecknade denna syntax som en syntaktisk socker över typ , introducerades nyckelordetList för att deklarera typvariabler . forall
  3. ↑ 1 2 3 4 MacQueen - TypeChecking .
  4. ↑ 12 MLton - Omfattning .
  5. ↑ haskell_existentials .
  6. ↑ Cardelli, Wegner, 1985 .
  7. ↑ haskell_rankNtypes .
  8. ↑ haskell_impredicative_types .
  9. ↑ OKaml-tillägg. 7.13 Lokalt abstrakta typer
  10. ↑ Philip Wadler, Stephen Blott. Hur man gör ad hoc polymorfism mindre ad hoc . — 1988.
  11. ↑ Andrew W. Appel. En kritik av Standard ML . — Princeton University, reviderad version av CS-TR-364-92, 1992.

Litteratur

Länkar

 Datatyper
Otolkbart
Numerisk
Text
Referens
Sammansatt
abstrakt
Övrig
Relaterade ämnen