Típusú változó

A típusváltozó ( típusváltozó ) a programozási nyelvekben és a típuselméletben  olyan változó , amely adattípusok halmazából vehet fel értéket .

A típusváltozót ugyanúgy használjuk az algebrai adattípus -definíciókban, mint egy paramétert a függvénydefinícióban , de egy adattípus átadására használják anélkül, hogy magát az adatot átadnák. A görög karaktereket hagyományosan a típusváltozók azonosítójaként használják a típuselméletben (bár sok programozási nyelv a latin ábécét használja, és megengedi a hosszabb neveket).

Példa

A " list " polimorf típus alábbi meghatározásában a Standard ML -ben az azonosító (ejtsd: "alpha") egy [2] típusú változó : 'a

adattípus 'a lista = nil | :: of 'a * 'egy lista

Ennek a polimorf típusnak a használatakor egy adott típust behelyettesítünk a típusváltozóba, így sok monomorf típus alakítható ki a programban: string list, int list, int list liststb. Ezzel a helyettesítéssel minden egyes típusváltozóra való hivatkozást ugyanaz a típus helyettesít. Az így kapott típusinformációkat a program ellenőrzésére és optimalizálására használják , majd általában törlik, így ugyanaz a célkód kezdetben különböző típusú objektumokat dolgoz fel (de vannak kivételek e szabály alól, különösen az MLton esetében ).

Ha egy polimorf típust több típusváltozó paraméterez, akkor a behelyettesített típusok lehetnek különbözőek vagy azonosak, de a helyettesítési szabályt betartjuk. Például, ha ez a típus:

adattípus ( 'a , 'b ) t = 'a | egyes száma ' a * ' a | duplája 'a * ' b párja

példányosítása így:

type t_ir = ( int , real ) t

akkor Single(4), Double(4,5)és Pair(4,5.0)a típus érvényes értékei lesznek t_ir, és az érték létrehozásának kísérlete gépelési hibátSingle(5.0) eredményez, mivel a paraméter értéke " ". 'aint

Összekapcsolás és számszerűsítés

Bármely típusú változó hatóköre egy adott kontextushoz van kötve [3] [4] . A következő példában az azonosítót 'aegymástól függetlenül használják két aláírásban, ami azt jelenti, hogy nem követeli meg a ténylegesen soron belüli típusok egyenlőségét a definíciók között:

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

Ez világossá válik, ha explicit kötés ( explicit hatókör vagy explicit bounding ) típusú változót használ:

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

A kötés korlátozza egy adott típusú változó hatókörét.

Az ML klasszikus dialektusaiban a típusváltozók explicit kötése opcionális szolgáltatás, és a legtöbb implementációt nem támogatják, mivel szükségtelenül szerepelnek – a kötés benne rejlik a típuslevonásban , ami a Hindley-Milner rendszer korai verzióinak korlátai miatt válik lehetővé . A teljes F rendszerben ez a deklaráció így van írva . Az ilyen jelölést prenex normál alaknak nevezzük . Ebben a bejegyzésben a nagybetű a típusréteg funkcióját jelenti ( type-level function ), amelynek paramétere a típusváltozó. Miután egy adott típust behelyettesített ebbe a változóba, ez a függvény egy monomorf értékszintű függvényt ( értékszintű függvény ) ad vissza. A prenex egy típusváltozó explicit összerendelése egy típusaláírás előtagjával. A Hindley-Milner rendszer korai változatai csak a prenex formát engedélyezték, vagyis megkövetelték, hogy egy típusváltozót egy adott értékkel példányosítsanak, mielőtt függvényhívásra lett volna szükség. Ezt a megszorítást prenex polimorfizmusnak nevezik  – ez nemcsak nagyban leegyszerűsíti a típusillesztési mechanizmust , hanem lehetővé teszi a programban található összes vagy csaknem valamennyi típusra (a nyelvjárástól függően) következtetni .

A típusváltozók legegyszerűbb összekapcsolását kvantifikációnak nevezzük . Két eset kiemelkedik:

  • egy típusváltozó működése a teljes típusdefinícióra kiterjed: ['a, 'b] 'a -> 'b -> 'a, matematikailag egy ilyen típust az univerzális kvantoron keresztül írunk - - ezért az ilyen típusú változót "univerzálisan kvantifikáltnak", a teljes típust pedig "univerzálisan polimorfnak" nevezzük;
  • egy típusváltozó hatása a típusdefiníciónak csak egy részére terjed ki: ['a] 'a -> (['b] 'b -> 'a), matematikailag egy ilyen típust az egzisztenciális kvantoron keresztül írnak le - - ezért az ilyen változót "egzisztenciálisan kvantifikáltnak", az egész típust pedig "egzisztenciálisnak" nevezik.

Egy univerzálisan polimorf típus egzisztenciális típussá „fordítása” nem minden esetben ad praktikus típust vagy észrevehető eltéréseket az univerzális polimorfizmustól, de bizonyos esetekben az egzisztenciális típusok használata emeli a parametrikus polimorfizmust első osztályú szintre, t. lehetővé teszi a polimorf függvények átadását anélkül, hogy paramétereket kötnének más függvényekhez (lásd az első osztályú polimorfizmust ). Klasszikus példa erre a heterogén lista megvalósítás (lásd a wikikönyvet). A típusok kifejezett megjegyzése ebben az esetben kötelezővé válik, mert típusú következtetés a 2. rang feletti polimorfizmusra algoritmikusan eldönthetetlen [5] .

A gyakorlatban az univerzálisan polimorf típusok az adattípus általánosítását adják, az egzisztenciális típusok pedig az adattípus absztrakcióját [6] .

Haskell több (nyelvi kiterjesztésként elérhető) módot különböztet meg: a Rank2Types mód az egzisztenciális típusoknak csak néhány olyan formáját engedi meg, amelyek a 2. rangnál nem magasabb polimorfizmust nyitják meg, amelyre a típuskövetkeztetés még eldönthető; a RankNTypes mód lehetővé teszi az univerzális kvantor ( forall a) mozgatását a bonyolultabb aláírások részét képező funkcionális típusokon belül [7] , az ImpredicativeTypes mód pedig tetszőleges egzisztenciális típusokat [8] .

Az OCaml az egzisztenciális kvantifikáció támogatását valósítja meg a "lokálisan absztrakt típusok" [ 9 ] nevű megoldáson keresztül .

A Standard ML specifikáció bizonyos beépített műveletekhez speciális kvantifikációt határoz meg. Szintaxisa nem szabályozott, és a nyelvi megvalósításokban különbözik (leggyakrabban egyszerűen rejtve van). Például a beépített összeadási művelet aláírása a következőképpen egyszerűsíthető:

val + : [ int , szó , valós ] 'a * 'a -> 'a

Ez a szemantika az ad-hoc polimorfizmus primitív formáját valósítja meg  – több fizikailag különböző összeadási műveletet kombinál egyetlen " +" azonosító alatt. Az OCaml fejlesztői elhagyták ezt a megoldást az ad-hoc polimorfizmus teljes eltávolításával a nyelvből (az általánosított algebrai adattípusok a későbbi verziókban jelentek meg ).

Az 1980 -as évek végén megjelent a Hindley-Milner kiterjesztés , amely adott esetben lehetővé tette bármely típusú változó értéktartományának korlátozását az újonnan meghatározott típus- típus osztályokban . A típusosztály szigorúbban korlátozza a megengedett gépelési környezeteket , lehetővé téve, hogy egy típusváltozót csak olyan típusok példányosítsanak, amelyek egy kifejezetten meghatározott osztályhoz tartoznak.

Ezt a kiterjesztést először a Haskell nyelv magjában valósították meg , például az egyenlőség-összehasonlító operátor a következő aláírással rendelkezik :

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

A következő generációs nyelv projektje - az utóda ML [1]  - megtagadja a típuskövetkeztetés szükségességét , explicit (manifest) típusú annotációra támaszkodva (beleértve a típusváltozók explicit kötését), amely közvetlen támogatást nyújt a teljes F rendszerhez az első- osztályú polimorfizmus és számos kiterjesztés, beleértve az altípusok és az egzisztenciális típusok [1] hierarchiáját .

Speciális típusú változók

Az ML család összes nyelvén használt típusváltozók fő osztálya az aplikatív típusú változók, amelyek értéket vehetnek az adott nyelven engedélyezett összes típus halmazából. A klasszikus dialektusokban szintaktikai jelölésük " " (egy alfanumerikus azonosító, mindig egyetlen aposztrófjal'a kezdődik ); Haskellben " " (alfanumerikus azonosító, mindig kisbetűvel kezdődik). a

Emellett az ML története során a típusváltozók speciális alosztályait is megkülönböztették.

Az egyenlőség szempontjából ellenőrizhető típusú változók (vagy hasonló típusú változók, egyenlőség típusú változók ) - értékeket vehetnek fel az egyenlőség szempontjából ellenőrizhető összes típus halmazából ( angol  egyenlőségtípusok ). Használatuk lehetővé teszi az egyenlőség-összehasonlítási művelet alkalmazását polimorf típusú objektumokra. Jelölésük " " (alfanumerikus azonosító, mindig két aposztrófjal''a kezdődik ). Érdekes módon az egyik eredeti cél, amelyre a típusosztályokat fejlesztették , éppen az ilyen típusú változók általánosítása volt a Standard ML -ből [10] . A nyelv meghatározásának és a fordítóprogramok megvalósításának jelentős (és vitathatatlanul indokolt) bonyolultsága miatt többször is kritizálták őket (a Definíció fele tartalmaz egy-egy módosítást) [11] . Elvileg nem célszerű az összetett absztrakt adattípusok egyenlőségét ellenőrizni, mivel az ilyen ellenőrzések jelentős időt vehetnek igénybe. Ezért az ML család későbbi nyelveiből eltávolították az olyan típusú változók támogatását, amelyek lehetővé teszik az egyenlőség tesztelését. A Haskell helyette a típusosztályt használja . Eq a

Az imperatív típusváltozók ad hoc megoldást adtak a mellékhatásokkal kapcsolatos típusbiztonsági problémára egy parametrikus polimorfizmussal rendelkező nyelven . Ez a probléma nem merül fel tiszta nyelvekben ( Haskell , Clean ), de a szennyezett nyelveknél ( Standard ML , OCaml ) a referenciapolimorfizmus gépelési hibákkal fenyeget [ 3] [4] . Az imperatív típusú változók az SML'90 definíció részét képezték, de megszűnt saját jelentésük, miután megalkották az " értékkorlátozást " , amely a felülvizsgált SML'97 definíció részévé vált. Az SML'97 kötelező típusú változóinak szintaktikai támogatása megmaradt a korábban írt kóddal való visszamenőleges kompatibilitás érdekében, de a modern megvalósítások ugyanúgy kezelik őket, mint az alkalmazottak. Jelölése " " (alfanumerikus azonosító, mindig aposztrófpal és aláhúzásjellel kezdődik) [3] . '_a

Az SML/NJ fordítóban gyenge típusú változókat használtak az imperatív típusú változók alternatívájaként, sokkal nagyobb teljesítményt (pontosabban kevesebb korlátozást) biztosítva. Jelölve " ", " " és így tovább (alfanumerikus azonosító, mindig aposztrófjal és számmal kezdődik ). Az aposztrófot közvetlenül követő szám a típusváltozó "gyengeségének" fokozatosságát jelezte. Az imperatív típusú változókhoz hasonlóan most is ugyanúgy kezeljük őket, mint az alkalmazó változókat. [3]'1a'2a

Jegyzetek

  1. ↑ 1 2 3 ML2000, 1999 .
  2. ↑ Itt az explicit kötéshez ( explicit kötés ) egy típusváltozót, az utód ML projektben [1] : alkalmazott jelenlegi szintaxist használjuk ['a]. Mivel Haskell ezt a szintaxist a típuson felüli szintaktikai cukornak jelölte meg , a kulcsszótList a típusváltozók deklarálására vezették be . forall
  3. ↑ 1 2 3 4 MacQueen - TypeChecking .
  4. ↑ 12 MLton - Hatáskör .
  5. ↑ haskell_existentials .
  6. ↑ Cardelli, Wegner, 1985 .
  7. ↑ haskell_rankNtypes .
  8. ↑ haskell_impredicative_types .
  9. ↑ OCaml kiterjesztések. 7.13 Lokálisan absztrakt típusok
  10. ↑ Philip Wadler, Stephen Blott. Hogyan lehet az ad-hoc polimorfizmust kevésbé ad hoc jellegűvé tenni ? – 1988.
  11. ↑ Andrew W. Appel. A Standard ML kritikája . — Princetoni Egyetem, a CS-TR-364-92 átdolgozott változata, 1992.

Irodalom

Linkek

 Adattípusok
Értelmezhetetlen
Numerikus
Szöveg
Referencia
Összetett
absztrakt
Egyéb
Kapcsolódó témák