Recent Changes - Search:
FP /

Strongly Typed Generic Libraries

A revised version of this project was granted in 2011: Strongly Typed Libraries for Programs and Proofs.

Below is the old work page for the VR application sent to VR 2010-04-13.

Summary

Our long term goal is to create systems (theories, programming languages, libraries and tools) which make it easy to develop reusable software components with matching specifications. The main goal of this research project is to improve the understanding, implementation and theory of strongly typed, generic programming. We work towards two sub-goals: 1) Efficient generic libraries: benchmarking and efficient compilation 2) Correct generic libraries: specification-driven development and parametricity.

Currently, Haskell is the language with the best support for generic programming but C++ is the language which has the most efficient generic libraries. We will employ partial evaluation, deforestation and specialisation techniques to improve the Haskell side. We will also use advanced type system features to enable optimised compilation of generic libraries.

We will extend verification tools available for non-generic code to also work for generic library code. Property-based testing (QuickCheck), parametricity results ("free theorems") and higher-order logic (Agda) will enable computer-aided proving of (partial) correctness results for generic code.

The scientific contributions will be in the form of software prototypes, conference talks/papers, journal papers and doctoral training. We aim to go beyond state-of-the-art when it comes to expressivity, efficiency and correctness of generic programming and we hope to improve the software technology field in general.

Populärvetenskaplig beskrivning

En viktig gren av forskningen inom datavetenskap handlar om att utveckla system som gör det enkelt att konstruera korrekt och återanvändbar programvara. Detta projekt handlar om system (programspråk, verktyg, teorier) som gör det möjligt att skriva program som fungerar likartat för många olika datastrukturer: generiska program. Eftersom generiska program fungerar för många olika datastrukturer, som t ex listor, databaser och släktträd, så kan de användas och återanvändas som byggstenar vid all slags programvarukonstruktion.

Ett enkelt exempel är ett program som räknar antalet element i en datastruktur. Utan generisk programmering måste man skriva en version för varje struktur (en för tabeller, en för sökträd, en för matriser, osv) medan ett generiskt program direkt fungerar för alla dessa.

Det finns flera skäl att använda generisk programmering. Generiska 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 minskar risken för fel vid omskrivningen. Vissa program är naturligt generiska; 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 generiska program följer också generiska specifikationer. Om man kan verifiera att ett generiskt program är korrekt (stämmer med sin specifikation) så har man ett flexibelt bevis eller test som kan återanvändas gång på gång för olika datastrukturer.

Mitt applikationsområde är exekverbara, överblickbara högnivåmodeller för komplexa system. Vi har hittills mest fokuserat på att modellera komplexa system inom dataområdet (logiska ramverk, lingvistik, programspråk, hårdvara) men i samarbetet med Potsdams Institut för Klimatforskning (PIK) har vi börjat arbeta med komplexa system i interaktionen mellan klimat, ekonomi och samhälle. PIK har under flera år arbetat med simuleringar av komplexa system och har under senare år börjat använda generisk funktionell programmering som ett verktyg för att experimentera med och kommunicera de högnivåmodeller som behövs för att överblicka komplexa system. Dessa högnivåmodeller översätts senare i flera steg till effektiv programkod som klarar att köra tunga simuleringar inom rimlig tid. (Dessa simuleringar ger underlag till politiska beslut inom klimatområdet.) PIK tog kontakt med Chalmers för att fördjupa sin kompetens inom högnivåmodellering med hjälp av moderna programspråk (som Haskell och C++) och vi har under åren som gått haft flera kontakter där starkt typade generiska programbibliotek har utkristalliserats som det forskningsområde där Chalmers bäst kan komplettera PIK.

Inom projektet kommer vi arbeta med följande delprojekt:

1) Effektiva generiska bibliotek. I nuläget är C++ det språk som har mest effektiva generiska programbibliotek medan Haskell är det språk som har bäst stöd för generisk programmering. Vi kommer att använda tekniker från C++ för att förbättra Haskellsidan. Vi kommer också att utnyttja resultat från typteori och kompilatorkonstruktion för att få effektiva generiska program.

2) Korrekta generiska bibliotek. QuickCheck är ett framgångsrikt koncept för att specifikation och automatisk testning av programkod, men det är inte direkt applicerbart på generiska program. Agda är ett verktyg baserat på typteori och funktionell programmering som möjliggör samtidig utveckling av program och specifikationer. Vi kommer att utforska olika tekniker för att utveckla korrekta generiska programbibliotek.

På Chalmers leds projektet av Patrik Jansson (inom gruppen Funktionell Programmering). Jansson har forskat om generisk programmering sedan 1995 i olika konstellationer och det internationella kontaktnätet är mycket starkt. Den lokala forskningsmiljön inom D&IT-institutionen är världsledande även inom flera närliggande områden - automatisk testning (Hughes, Claessen), domänspecifika språk (Sheeran, Claessen), typteori (Coquand), språkteknologi (Ranta).