Tyyppipäätelmä

Type inference ( eng. type inference ) - ohjelmoinnissa kääntäjän kyky päätellä loogisesti itse lausekkeen arvon tyyppi . Tyyppipäättelymekanismi otettiin ensimmäisen kerran käyttöön ML -kielessä , jossa kääntäjä päättelee aina yleisimmän polymorfisen tyypin mille tahansa lausekkeelle. Tämä ei ainoastaan vähennä lähdekoodin kokoa ja lisää sen tiiviyttä, vaan lisää usein koodin uudelleenkäyttöä [1] .

Tyyppipäättely on ominaista toiminnallisille ohjelmointikielille , vaikka se on ajan myötä osittain toteutettu oliokielillä ( C# , D , Visual Basic .NET , Nim , C++11 , Vala , Java [a] ), missä se rajoittuu kykyyn jättää pois tunnisteen tyyppi määritelmästä alustuksen yhteydessä (katso syntaktinen sokeri ). Esimerkiksi:

var s = "Hei, maailma!" ; // Muuttujan s (merkkijonosta) tyyppi johdetaan alustuksesta

Algoritmit

Hindley-Milner-algoritmi

Hindley-Milner-algoritmi on lauseketyyppinen päättelymekanismi, joka on toteutettu Hindley-Milner-tyyppiseen järjestelmään perustuvissa ohjelmointikielissä , kuten ML (tämän perheen ensimmäinen kieli), Standard ML , OCaml , Haskell , F# , Fortress ja Boo . Nemerlen kieli käyttää tätä algoritmia useilla tarvittavilla muutoksilla [2] .

Tyyppipäätelmämekanismi perustuu kykyyn päätellä automaattisesti, kokonaan tai osittain, jonkin lausekkeen arvioimalla saadun lausekkeen tyyppi. Koska tämä prosessi suoritetaan systemaattisesti ohjelman käännöksen aikana, kääntäjä voi usein päätellä muuttujan tai funktion tyypin määrittelemättä nimenomaisesti näiden objektien tyyppejä. Monissa tapauksissa eksplisiittiset tyyppiilmoitukset voidaan jättää pois - tämä voidaan tehdä melko yksinkertaisille objekteille tai kielille, joilla on yksinkertainen syntaksi. Esimerkiksi Haskell-kielellä on varsin tehokas tyyppipäättelymekanismi, joten tässä ohjelmointikielessä ei ole tarpeen määritellä funktiotyyppejä. Ohjelmoija voi määrittää funktion tyypin nimenomaisesti rajoittaakseen sen käytön tiettyihin tietotyyppeihin tai jäsennellympään lähdekoodin muotoiluun.

Saadakseen tietoa lausekkeen tyypin oikeasta päättelystä ilman nimenomaista ilmoitusta tämän lausekkeen tyypistä kääntäjä joko kerää tällaiset tiedot sisällytettyjen alilauseketyyppien (muuttujat, funktiot) eksplisiittisistä ilmoituksista. tutkitussa lausekkeessa tai käyttää implisiittistä tietoa atomiarvojen tyypeistä. Tällainen algoritmi ei aina auta määrittämään lausekkeen tyyppiä, etenkään tapauksissa, joissa käytetään korkeamman asteen funktioita ja melko monimutkaista parametrista polymorfismia . Siksi monimutkaisissa tapauksissa, kun on tarpeen välttää epäselvyyksiä, on suositeltavaa määrittää selkeästi lausekkeiden tyyppi.

Tyypitysmalli itsessään perustuu lauseketyypin päättelyalgoritmiin, jonka lähteenä on H. Curryn ja R. Facen vuonna 1958 ehdottamassa tyypitetyssä λ-laskennassa käytetty lauseketyypin johtamismekanismi. Lisäksi Roger Hindley vuonna 1969 laajensi itse algoritmia ja osoitti, että se johtaa yleisimmän ilmaisutyypin. Vuonna 1978 Robin Milner todisti R. Hindleystä riippumatta vastaavan algoritmin ominaisuudet. Ja lopuksi, vuonna 1985 , Louis Damas vihdoin osoitti, että Milnerin algoritmi on valmis ja sitä voidaan käyttää polymorfisille tyypeille. Tässä suhteessa Hindley-Milner-algoritmia kutsutaan joskus myös Damas-Milner-algoritmiksi .

Tyyppijärjestelmä on määritelty Hindley-Milner-mallissa seuraavasti:

Primitiiviset tyypit ovat lauseketyyppejä. $v$
Parametrityypin muuttujat α ovat ilmaisutyyppejä.
Jos ja ovat lauseketyyppejä, tyyppi on lauseketyyppi. $\sigma _{{1}}$ $\sigma _{{2}}$ $\sigma _{{1}}\rightarrow \sigma _{{2}}$
Symboli on eräänlainen ilmaisu. $\bot$

Lausekkeet, joiden tyypit arvioidaan, määritellään melko tavallisella tavalla:

Vakiot ovat ilmaisuja.
Muuttujat ovat lausekkeita.
Jos ja ovat lausekkeita, niin ( ) on lauseke. $e_{{1}}$ $e_{{2}}$ $e_{{1}}e_{{2}}$
If on muuttuja ja on lauseke, niin on lauseke. $v$ $e$ $\lambda ve$

Tyypin sanotaan olevan tyypin esiintymä, kun tapahtuu muunnos , joka: $\sigma _{{1}}$ $\sigma _{{2}}$ $\rho$

$\sigma _{{1}}=\rho (\sigma _{{2}})$

Tässä tapauksessa oletetaan yleensä, että tyyppimuunnoksilla on rajoituksia, joita ovat seuraavat: $\rho$

$\rho (\sigma _{{1}}\rightarrow \sigma _{{2}})=\rho (\sigma _{{1}})\rightarrow \rho (\sigma _{{2}})$
$\rho (v) = v$

Tyyppipäättelyalgoritmi itsessään koostuu kahdesta vaiheesta - yhtälöjärjestelmän muodostamisesta ja näiden yhtälöiden myöhemmästä ratkaisusta.

Yhtälöjärjestelmän rakentaminen

Yhtälöjärjestelmän rakentaminen perustuu seuraaviin sääntöihin:

$\Gamma v=\tau$ - jos sidonta on . $v:\tau$ $\Gamma$
$\Gamma (ge)=\tau$ - jos , missä ja . $\tau _{{1}}=\tau _{{2}}\rightarrow \tau$ $\tau _{1}=\Gamma g$ $\tau _{2}=\Gamma e$
${\displaystyle \Gamma (\lambda ve)=\tau \rightarrow \tau _{e))$ - siinä tapauksessa , missä se on lisätyllä sidoksella . $\tau _{e}=\Gamma 'e$ $\gamma '$ $\Gamma$ $v:\tau$

Näissä säännöissä symboli on joukko assosiaatioita muuttujien ja niiden tyyppien välillä: $\Gamma$

$\Gamma =v_{{1}}:A_{{1}},v_{{2}}:A_{{2}},\ldots ,v_{{n}}:A_{{n}}$

Yhtälöjärjestelmän ratkaiseminen

Rakennetun yhtälöjärjestelmän ratkaisu perustuu yhdistämisalgoritmiin . Tämä on melko yksinkertainen algoritmi. On olemassa funktio , joka ottaa syötteeksi tyyppiyhtälön ja palauttaa korvauksen, joka tekee yhtälön vasemmasta ja oikeasta puolesta saman ("yhdistää" ne). Substituutio on yksinkertaisesti muuttujatyyppien projektio itse tyypeille. Sellaiset substituutiot voidaan laskea eri tavoilla, jotka riippuvat Hindley-Milner-algoritmin erityisestä toteutuksesta. $u$

Katso myös

Muistiinpanot

Kommentit

↑ tuki lisätty Java SE 10 :een

Lähteet

↑ Andrew W. Appel. Standard ML:n kritiikki. — Princetonin yliopisto, tarkistettu versio CS-TR-364-92:sta, 1992.
↑ Michal Moskal. Tyyppi Inference with Deferral . – 2005.

Linkit

Hindley - Milner-algoritmin käyttöönotto Perlissä
Roger Hindleyn arkistoitu sähköpostiviesti selittää tyyppipäätelmien historian
Michael Schwartzbachin Polymorphic Type Inference , antaa yleiskatsauksen polymorfisen tyypin päättelystä.
Toiminnallisten ohjelmien päätyyppikaaviot. Uudelleen ladattu kopio Damasin ja Milnerin paperista, jossa kuvattiin todenperäisyyttä ja täydellisyyttä.
Opetusohjelma ja täydellinen toteutus Standard ML :ssä Opetusohjelma sisältää osan tyyppijärjestelmien loogisesta historiasta sekä yksityiskohtaisen kuvauksen algoritmista sellaisena kuin se on toteutettu. Jotkut alkuperäisen Damas Milner -paperin kirjoitusvirheet on korjattu.
Luca Cardellin Basic Typechecking -paperi, kuvaa algoritmia, sisältää toteutuksen Modula-2 :ssa
Hindley-Milner-tyyppisen päätelmän toteutus Scalassa , Andrew Forrest (haettu 30. heinäkuuta 2009)
Hindley-Milnerin toteutus Perl 5:ssä, Nikita Borisov (linkki ei saatavilla) . Käyttöpäivä: 12. maaliskuuta 2009. Arkistoitu alkuperäisestä 18. helmikuuta 2007. (määrätön)
Mikä on Hindley-Milner? (ja miksi se on siistiä?) Selittää Hindley-Milner, esimerkkejä Scalassa
http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ Hindley-Milnerin kirjoitusmalli ja esimerkki sen toteutuksesta Haskellissa