Polymorf rekursion

Inom datavetenskap hänvisar polymorf rekursion (även kallad Milner – Mycroft typability eller Milner – Mycroft calculus ) till en rekursiv parametriskt polymorf funktion där typparametern ändras med varje rekursiv anrop som görs, istället för att förbli konstant . Typinferens för polymorf rekursion är ekvivalent med semi-unifiering och är därför obestämbar och kräver användning av en semi-algoritm eller annoteringar av programmerare .

Exempel

Kapslade datatyper

Tänk på följande kapslade datatyp:

         
  

         data  Kapslad  a  =  a  :<:  (  Kapslad  [  a  ])  |  Epsilon  infixr  5  :<:  kapslade  =  1  :<:  [  2  ,  3  ,  4  ]  :<:  [[  5  ,  6  ],[  7  ],[  8  ,  9  ]]  :<:  Epsilon

En längdfunktion definierad över denna datatyp kommer att vara polymorfiskt rekursiv, eftersom typen av argument ändras från Nested a till Nested [a] i det rekursiva anropet:

     
      0
         längd  ::  Kapslad  a  ->  Int  längd  Epsilon  =  längd  (  _  :<:  xs  )  =  1  +  längd  xs

Observera att Haskell normalt härleder typsignaturen för en funktion som är så enkel som denna, men här kan den inte utelämnas utan att ett typfel utlöses.

Högre rankade typer

Ansökningar

Programanalys

I typbaserad programanalys är polymorf rekursion ofta väsentlig för att få hög precision i analysen. Anmärkningsvärda exempel på system som använder polymorf rekursion inkluderar Dussart, Henglein och Mossins bindningstidsanalys och det Tofte–Talpin- regionbaserade minneshanteringssystemet . Eftersom dessa system antar att uttrycken redan har skrivits in i ett underliggande typsystem (inte nödvändigt med användning av polymorf rekursion), kan slutsatser göras avgörbara igen.

Datastrukturer, felsökning, graflösningar

Funktionella programmeringsdatastrukturer använder ofta polymorf rekursion för att förenkla typfelkontroller och lösa problem med otäcka "mitten" temporära lösningar som slukar minne i mer traditionella datastrukturer som träd. I de två citaten som följer ger Okasaki (sid. 144–146) ett CONS-exempel i Haskell där det polymorfa typen automatiskt flaggar programmeringsfel. Den rekursiva aspekten är att typdefinitionen säkerställer att den yttersta konstruktorn har ett enda element, den andra ett par, den tredje ett par par etc. rekursivt, vilket sätter ett automatiskt felsökningsmönster i datatypen. Roberts (sid. 171) ger ett relaterat exempel i Java där en klass används för att representera en stackram. Exemplet som ges är en lösning på Tower of Hanoi- problemet där en stack simulerar polymorf rekursion med en början, temporär och avslutande kapslad stacksubstitutionsstruktur.

Se även

Högre rankad polymorfism

Anteckningar

Vidare läsning

Meertens, Lambert (1983). "Inkrementell polymorf typkontroll i B" (PDF) . ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas .
Mycroft, Alan (1984). "Polymorfa typscheman och rekursiva definitioner". Internationellt symposium om programmering . Internationellt symposium om programmering, Toulouse, Frankrike . Föreläsningsanteckningar i datavetenskap. Vol. 167. s. 217–228. doi : 10.1007/3-540-12925-1_41 . ISBN 978-3-540-12925-7 .
Henglein, Fritz (1993). "Typ slutledning med polymorf rekursion". ACM-transaktioner på programmeringsspråk och system . 15 (2): 253–289. CiteSeerX 10.1.1.42.3091 . doi : 10.1145/169701.169692 . S2CID 17411856 .
Kfoury, AJ; Tiuryn, J.; Urzyczyn, P. (april 1993). "Typrekonstruktion i närvaro av polymorf rekursion". ACM-transaktioner på programmeringsspråk och system . 15 (2): 290–311. doi : 10.1145/169701.169687 . ISSN 0164-0925 . S2CID 18059949 .
Michael I. Schwartzbach (juni 1995). "Inferens av polymorf typ" . Teknisk rapport BRICS-LS-95-3 .
Emms, Martin; Leiß, Hans (1996). "Utöka typkontrollen för SML genom polymorf rekursion - ett korrekthetsbevis" . Teknisk rapport 96-101 .
Richard Bird och Lambert Meertens (1998). "Inkapslade datatyper" .
C. Vasconcellos, L. Figueiredo, C. Camarao (2003). " Praktisk typinferens för polymorfisk rekursion: en implementering i Haskell ^{[ död länk] "} . Journal of Universal Computer Science .
L. Figueiredo, C. Camarao. " Typinferens för polymorfa rekursiva definitioner: en specifikation i Haskell" .
Hallett, J.J; Kfoury, AJ (juli 2005). "Programmeringsexempel som behöver polymorf rekursion" . Elektroniska anteckningar i teoretisk datavetenskap . 136 : 57–102. doi : 10.1016/j.entcs.2005.06.014 . ISSN 1571-0661 .

externa länkar

Standard ML med polymorf rekursion av Hans Leiß, Münchens universitet