Typ proměnné

Proměnná typu ( proměnná typu ) v programovacích jazycích a teorii typů  je proměnná , která může nabývat hodnoty ze sady datových typů .

Proměnná typu se používá v algebraické definici datového typu stejným způsobem, jakým se parametr používá v definici funkce , ale používá se k předání datového typu bez předávání samotných dat. Řecké znaky se tradičně používají jako identifikátory pro typové proměnné v teorii typů (ačkoli mnoho programovacích jazyků používá latinku a umožňuje delší názvy).

Příklad

V následující definici polymorfního typu „ list “ ve standardním ML je identifikátor 'a(vyslovuje se „alfa“) proměnná typu [2] :

datový typ 'a list = nula | :: z 'a * ' seznamu

Při použití tohoto polymorfního typu se do proměnné typu dosadí konkrétní typ, takže v programu lze vytvořit mnoho monomorfních typů: string list, int listatd int list list. Při této substituci je každý odkaz na proměnnou typu nahrazen stejným typem. Výsledné informace o typu se používají k ověření a optimalizaci programu, poté se obvykle vymažou, takže stejný cílový kód zpracuje objekty původně různých typů (ale zejména v MLton existují výjimky z tohoto pravidla ).

Pokud je polymorfní typ parametrizován několika typovými proměnnými, pak typy do nich dosazené mohou být různé nebo identické, ale pravidlo substituce je respektováno. Pokud je tento typ například:

datový typ ( 'a , 'b ) t = Single of 'a | Dvojnásobek 'a * ' a | Dvojice 'a * ' b

vytvořit instanci takto:

zadejte t_ir = ( int , real ) t

pak Single(4), Double(4,5)a Pair(4,5.0)budou platnými hodnotami typu t_ira pokus o vytvoření hodnoty Single(5.0)bude mít za následek chybu při psaní , protože parametr 'amá hodnotu " int".

Propojení a kvantifikace

Rozsah libovolné typové proměnné je vázán na konkrétní kontext [3] [4] . V následujícím příkladu je identifikátor 'apoužit nezávisle ve dvou signaturách, což znamená, že nevyžaduje rovnost skutečně vložených typů mezi definicemi:

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

To je zřejmé při použití proměnné typu explicitní vazby ( explicitní rozsah nebo explicitní ohraničení ):

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

Vazba omezuje rozsah proměnné daného typu.

V klasických dialektech ML je explicitní vazba typových proměnných volitelnou funkcí a většina implementací není podporována jako zbytečná - vazba v nich je implicitní v dedukci typu , což je možné díky omezením raných verzí systému Hindley-Milner . V kompletním systému F se toto prohlášení zapisuje jako . Takový zápis se nazývá prenexová normální forma . Velké písmeno v tomto záznamu znamená funkci typové vrstvy ( type-level function ), jejímž parametrem je typová proměnná. Po dosazení určitého typu do této proměnné tato funkce vrátí monomorfní funkci na úrovni hodnoty ( funkce na úrovni hodnoty ). Prenex je explicitní vazba proměnné typu s předponou k podpisu typu. Dřívější verze systému Hindley-Milner umožňovaly pouze prenexovou formu, to znamená, že vyžadovaly, aby typová proměnná byla konkretizována se specifickou hodnotou, než bylo potřeba volání funkce. Toto omezení se nazývá prenexový polymorfismus  – nejenže výrazně zjednodušuje mechanismus porovnávání typů , ale také umožňuje odvodit všechny nebo téměř všechny (v závislosti na dialektu) typy v programu.

Nejjednodušší vazba typových proměnných se nazývá jejich kvantifikace . Vynikají dva případy:

  • působení typové proměnné se vztahuje na celou definici typu: ['a, 'b] 'a -> 'b -> 'a, matematicky se takový typ zapisuje přes univerzální kvantifikátor - - proto se taková typová proměnná nazývá "univerzálně kvantifikovaná" a celý typ se nazývá "univerzálně polymorfní";
  • účinek typové proměnné se rozšiřuje pouze na část definice typu: ['a] 'a -> (['b] 'b -> 'a), matematicky se takový typ zapisuje přes existenciální kvantifikátor - - proto se taková proměnná nazývá "existenciálně kvantifikovaná" a celý typ se nazývá "existenciální".

Ne ve všech případech dává "přeměna" univerzálně polymorfního typu na existenciální typ praktický typ nebo znatelné rozdíly od univerzálního polymorfismu, ale v určitých případech použití existenciálních typů pozvedá parametrický polymorfismus na prvotřídní úroveň, tzn. umožňuje předávání polymorfních funkcí bez vazby jako parametrů na jiné funkce (viz polymorfismus první třídy ). Klasickým příkladem je implementace heterogenního seznamu (viz wikibook). Explicitní anotace typů se v tomto případě stává povinným, protože typová inference pro polymorfismus nad úrovní 2 je algoritmicky nerozhodnutelná [5] .

V praxi univerzálně polymorfní typy dávají zobecnění datového typu a existenciální typy - abstrakci datového typu [6] .

Haskell rozlišuje několik režimů (dostupných jako jazyková rozšíření): režim Rank2Types dovoluje pouze některé formy existenciálních typů, které otevírají polymorfismus ne vyšší než hodnost 2, u nichž je odvození typu stále rozhodnutelné; režim RankNTypes umožňuje přesun univerzálního kvantifikátoru ( forall a) uvnitř funkčních typů , které jsou součástí složitějších signatur [7] , režim ImpredicativeTypes umožňuje libovolné existenciální typy [8] .

OCaml implementuje podporu pro existenciální kvantifikaci prostřednictvím řešení zvaného „lokálně abstraktní typy“ [ 9 ] .

Specifikace Standard ML definuje speciální kvantifikaci pro některé vestavěné operace. Jeho syntaxe není regulována a liší se v jazykových implementacích (nejčastěji je jednoduše skrytá). Podpis vestavěné operace sčítání lze například zjednodušit takto:

val + : [ int , slovo , skutečné ] 'a * 'a -> 'a

Tato sémantika implementuje primitivní formu ad-hoc polymorfismu  - kombinuje několik fyzicky odlišných operací sčítání pod jedním identifikátorem " +". Vývojáři OCaml opustili toto řešení a zcela odstranili ad-hoc polymorfismus z jazyka ( zobecněné algebraické datové typy se objevily v pozdějších verzích ).

Na konci osmdesátých let se objevilo rozšíření Hindley-Milner , které v případě potřeby umožnilo omezit rozsah hodnot pro jakoukoli proměnnou typu v nově definovaných třídách typů . Třída typu přísněji omezuje povolené kontexty psaní , což umožňuje konkretizaci proměnné typu pouze typy, které patří do explicitně určené třídy.

Toto rozšíření bylo poprvé implementováno v jádru jazyka Haskell , například operátor porovnání rovnosti má v sobě následující podpis :

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

Projekt jazyka nové generace - nástupce ML [1]  - odmítá potřebu odvozování typu , spoléhá na explicitní (manifestní) typovou anotaci (včetně explicitní vazby typových proměnných), která poskytuje přímou podporu pro plný systém F s prvním- třídní polymorfismus a řada rozšíření, včetně hierarchií podtypů a existenciálních typů [1] .

Speciální proměnné typu

Hlavní třídou typových proměnných používaných ve všech jazycích rodiny ML jsou aplikační proměnné typu, které mohou nabývat hodnot ze sady všech typů povolených v konkrétním jazyce. V klasických dialektech jsou syntakticky označovány jako „ 'a“ (alfanumerický identifikátor, vždy začínající jedním apostrofem ); v Haskellu jako " a" (alfanumerický identifikátor, vždy začínající malým písmenem).

Kromě toho se v průběhu historie ML rozlišovaly speciální podtřídy typových proměnných.

Proměnné typu, u kterých lze kontrolovat rovnost (nebo proměnné srovnatelného typu, proměnné typu rovnosti ) - mohou nabývat hodnot z množiny všech typů, u kterých lze kontrolovat rovnost ( anglicky  equality types ). Jejich použití umožňuje použít operaci porovnání rovnosti na objekty polymorfních typů. Označují se jako " ''a" (alfanumerický identifikátor, vždy začínající dvěma apostrofy ). Je zajímavé, že jedním z původních cílů, pro které byly typové třídy vyvinuty , bylo právě zobecnění takových typových proměnných ze Standardu ML [10] . Opakovaně byly kritizovány kvůli značné (a prokazatelně oprávněné) komplikaci definice jazyka a implementace překladačů (polovina stránek Definice obsahuje jejich jednu či druhou úpravu) [11] . V zásadě se nedoporučuje kontrolovat rovnost komplexních abstraktních datových typů, protože takové kontroly mohou vyžadovat značné množství času. Proto byla z pozdějších jazyků rodiny ML odstraněna podpora pro proměnné typu, který umožňuje testování rovnosti. Haskell místo toho používá třídu typu Eq a .

Imperativní typové proměnné poskytly ad hoc řešení problému bezpečnosti typu spojeného s vedlejšími účinky v jazyce s parametrickým polymorfismem . Tento problém nevzniká v čistých jazycích ( Haskell , Clean ), ale u nečistých jazyků ( Standard ML , OCaml ) referenční polymorfismus představuje hrozbu překlepů [3] [4] . Proměnné imperativního typu byly součástí definice SML'90, ale přestaly mít svůj vlastní význam poté, co bylo vytvořeno „ omezování hodnoty “ , které se stalo součástí revidované definice SML'97. Syntaktická podpora pro proměnné imperativního typu v SML'97 byla zachována pro zpětnou kompatibilitu s dříve napsaným kódem, ale moderní implementace s nimi zacházejí identicky jako s aplikačními. Značeno " '_a" (alfanumerický identifikátor, vždy začínající apostrofem a podtržítkem) [3] .

Proměnné slabého typu byly použity v kompilátoru SML/NJ jako alternativa k proměnným imperativního typu, poskytující mnohem větší výkon (přesněji méně omezení). Značeno " '1a", " '2a" atd. (alfanumerický identifikátor, vždy začínající apostrofem a číslem). Číslo bezprostředně za apostrofem označovalo gradaci „slabosti“ typové proměnné. Stejně jako proměnné imperativního typu se s nimi nyní zachází stejně jako s aplikačními. [3]

Poznámky

  1. ↑ 1 2 3 ML2000, 1999 .
  2. ↑ Zde se pro explicitní vazbu ( explicitní vazba ) typové proměnné používá aktuální syntaxe přijatá v následnickém projektu ML [1] : ['a]. Protože Haskell označil tuto syntaxi jako syntaktický cukr nad typem , Listbylo zavedeno klíčové slovo forall pro deklaraci typových proměnných .
  3. ↑ 1 2 3 4 MacQueen - TypeChecking .
  4. ↑ 12 MLton - Rozsah .
  5. ↑ haskell_existentials .
  6. ↑ Cardelli, Wegner, 1985 .
  7. ↑ haskell_rankNtypes .
  8. ↑ haskell_impredicative_types .
  9. ↑ Rozšíření OCaml. 7.13 Lokálně abstraktní typy
  10. ↑ Philip Wadler, Stephen Blott. Jak snížit ad-hoc polymorfismus ad hoc . — 1988.
  11. ↑ Andrew W. Appel. Kritika standardního ML . — Princetonská univerzita, revidovaná verze CS-TR-364-92, 1992.

Literatura

Odkazy

 Typy dat
Neinterpretovatelné
Numerický
Text
Odkaz
Kompozitní
abstraktní
jiný
související témata