Functional Polytypic Programming

(Funktionell polytypisk programmering)

Patrik Jansson

Akademisk avhandling för avläggande av teknisk doktorsexamen
vid institutionen för datavetenskap, Chalmers tekniska högskola

Avhandlingen finns tillgänglig som (PDF), som en komprimerad PostScript-fil (.ps.gz) och för utlåning från Chalmers bibliotek.
[This information is also available in english.]

Sammanfattning

Många algoritmer måste implementeras gång på gång för olika datatyper, antingen för att datatyperna ändras under programutvecklingen, eller för att samma algoritm används för flera olika datatyper i samma program. Exempel på sådana algoritmer är likhetstest, datakompression, och mönstermatchning och att konstruera sådana algoritmer kallas polytypisk programmering. Avhandlingen introducerar polytypisk programmering för funktionella programspråk, visar hur man kan uttrycka och bevisa egenskaper hos polytypiska algoritmer, definierar den polytypiska språkutvidgningen PolyP, och presenterar ett antal exempel på användningen av polytypisk programmering. Bland exemplen finns två större polytypiska tillämpningar: omskrivningssystem och datakonvertering, samt programbiblioteket PolyLib vilket innehåller ett antal grundläggande polytypiska algoritmer

PolyP är en utvidgning av ett funktionellt programspråk (en delmängd av Haskell) med en språkkonstruktion som gör det möjligt att definiera polytypiska funktioner med induktion över användardefinierade datatypers struktur. Program i det utvidgade språket översätts till Haskell.

Den första tillämpningen är ett ramverk för polytypisk programmering på termer. Vi visar att ett gränssnitt på fyra funktioner är tillräckligt för att definiera polytypiska funktioner för mönstermatchning, unifiering och omskrivningssystem. I detta ramverk specificerar vi en funktion för omskrivning, och transformerar den till en effektiv och korrekt implementation.

Den andra större tillämpningen beskriver och visar korrektheten hos ett antal funktioner för polytypisk datakonvertering. Vi behandlar utskrift och inläsning, kompression och dekompression av data med struktur. Konverteringfunktionerna uttrycks i ett domänspecifikt språk för datakonvertering inbäddat i Haskell (språket implementeras som en klasshierarki).

PolyLib innehåller kraftfulla rekursionsoperatorer som katamorfismer (cata), avbildningar (map) och genomlöpningar (thread) tillsammans med polytypiska versioner av ett antal standardfunktioner inom funktionell programmering: sum, length, zip, (==), (<=), osv. Avhandlingen inkluderar både specifikationen av programbiblioteket och en implementation i PolyP.

Nyckelord: Programspråk, Funktionell programmering, Algebraisk datatyp, Polytypisk programmering, Generisk programmering

Disputation

Avhandlingen försvaras vid en offentlig disputation klockan 10.15, 9 juni 2000 i Hörsalen, Matematiskt Centrum, Eklandagatan 86, Göteborg. Fakultetsopponent är professor Mark Jones, Oregon Graduate Institute, USA. Avhandlingen försvaras på engelska.

Bibliografiska data

@PhdThesis{jansson-phdthesis,
  author =	 {Jansson, Patrik},
  title =	 {Functional Polytypic Programming},
  school =	 {Computing Science, Chalmers University of Technology
                  and Göteborg University, Sweden},
  month =	 may,
  isbn =	 {91-7197-895-X},
  year =	 2000
}

Material till pressmeddelande

Jag forskar inom datavetenskap på programspråk som gör det möjligt att beskriva algoritmer som fungerar likartat för många olika datastrukturer: polytypiska algoritmer. Ett enkelt exempel är ett program som räknar antalet element i en datastruktur. Utan polytypisk programmering måste man skriva en version för varje struktur (en för listor, en för binära sökträd, en för matriser osv.) medan en polytypisk algoritm direkt fungerar för alla dessa.

Det finns många fördelar med polytypisk programmering. Eftersom polytypiska algoritmer direkt kan användas på många olika datastrukturer så kan de användas och återanvändas som byggstenar i konstruktionen av alla slags program. Polytypiska program är flexibla i den meningen att de anpassar sig när datatyper förändras. Denna flexibilitet minskar behovet av tidskrävande och tråkiga omskrivningar, och eliminerar risken för fel vid omskrivningen. Vissa algoritmer är naturligt polytypiska: att genomlöpa en datastruktur och utföra samma transformation på alla delar, att skriva ut, läsa in, komprimera eller dekomprimera datastrukturer, att testa om två strukturer är lika, eller vilken som är större, att fläta samman två strukturer till en, osv. Med polytypiska algoritmer följer också polytypiska bevis. Om man bevisar att en polytypisk algoritm är korrekt så har man ett flexibelt bevis som kan återanvändas gång på gång för olika datastrukturer.

Avhandlingen beskriver polytypisk programmering, det polytypiska programspråket PolyP, ett programbibliotek med grundläggande polytypiska algoritmer: PolyLib, några större polytypiska algoritmer (inklusive alla de ovan nämnda) och flera polytypiska bevis för egenskaper hos t ex genomlöpningar, utskrift och inläsning av datastrukturer.

Mer information finns på www.cse.chalmers.se/~patrikj/poly/.

Last modified: Fri May 26 12:17:36 MET DST 2000 by

Patrik Jansson / NOpatrikjSP@AMchalmers.se