Computerprogramma's nemen een steeds belangrijkere plaats in binnen de hedendaagse maatschappij. Dat programma's fouten bevatten is eerder regel dan uitzondering; dit geldt zowel voor kleine applicaties als voor grootschalige softwareprojecten. De consequenties van een foutief programma hangen voornamelijk af van het toepassingsgebied. In de meeste gevallen zal een fout slechts irritatie opwekken bij de gebruiker, bijvoorbeeld omdat een computerprogramma onverwachts stopt, of omdat een bepaalde internetpagina niet getoond kan worden. In andere gevallen kan een foutief programma een grotere impact hebben. Te denken valt aan beveiligingsproblemen van een bedrijfsnetwerk, veroorzaakt door falende software, of aan de gevolgen van een fout in de computerprogrammatuur voor het besturen van een vliegtuig. Het ontwerpen van betrouwbare en foutloze computerprogramma's is één van de grootste uitdagingen voor de software-industrie.
Om de kwaliteit van een programma te kunnen garanderen is het belangrijk om in een vroeg stadium programmeerfouten te detecteren. Dit kan door een programma gedurende het ontwikkelingsproces uitvoerig te testen. Echter, zelfs de meest zorgvuldige testprocedure kan onmogelijk alle fouten aan het licht brengen. Een aanvullende methode om fouten op te sporen is de programmacode automatisch te laten analyseren. Deze controle vindt plaats zonder dat het geanalyseerde programma wordt uitgevoerd, en staat bekend als statische analyse. Dit soort analyses hebben twee belangrijke voordelen ten opzichte van het testen van software. Ten eerste vindt er een snelle terugkoppeling plaats naar de ontwerper van het programma. De vroegtijdige rapportage van fouten zorgt ervoor dat deze direct en efficiënt hersteld kunnen worden. Een bijkomend voordeel is dat de programmeur geconfronteerd wordt met zijn fouten, en niet de gebruiker. Ten tweede kan een analyse het optreden van bepaalde foutsituaties categorisch uitsluiten, wat de kwaliteit van de programmatuur ten goede komt.
Een moderne compiler (vertaler) biedt vele geavanceerde programma-analyses aan om vroegtijdig fouten in programma's te rapporteren. Het genereren van efficiënt executeerbare code is traditioneel een belangrijk aandachtsveld voor vertalerbouwers. Vaak wordt echter minder aandacht geschonken aan de presentatie van foutmeldingen. Het toevoegen van duidelijke en behulpzame foutmeldingen aan een compiler is niet alleen veel werk, maar is mede afhankelijk van factoren zoals de programmeerstijl en de deskundigheid van de programmeur. Met name voor de meer geavanceerde analyses geldt dat de foutmeldingen vaak cryptisch van aard zijn. Een gevolg hiervan is dat het voor een programmeur dikwijls onduidelijk is waarom een programma als incorrect wordt beschouwd, en hoe de gemaakte fout hersteld kan worden.
Ter illustratie van het probleem bekijken we de werking van een geautomatiseerde spelling- en grammaticacontrole voor een stuk Nederlandse tekst. Hoe praktisch zou zo'n toepassing zijn als enkel wordt vermeld of de tekst in zijn geheel goed dan wel fout is? Het is wenselijk dat de locatie van een gevonden fout zo nauwkeurig mogelijk wordt vermeld, al kan deze niet altijd eenduidig worden aangewezen. De toepassing wordt pas echt gebruiksvriendelijk als ook wordt aangegeven hoe een gemaakte fout verbeterd zou kunnen worden, eventueel met verwijzingen naar het Groene Boekje. Een soortgelijke functionaliteit is ook wenselijk voor de fouten die een vertaler rapporteert.
Welke programma-analyses kunnen worden toegepast hangt voornamelijk af van de gebruikte programmeertaal. De bekendste familie van programmeertalen heeft een imperatief karakter. Een programma dat geschreven is in zo'n taal bestaat uit een serie van instructies die na elkaar moeten worden uitgevoerd. Functionele programmeertalen bieden een alternatief waarbij een programma wordt beschreven door een verzameling van (wiskundige) functies. Deze talen zijn gebaseerd op de principes van de lambda-calculus. Recente functionele programmeertalen zijn onder andere ML en Haskell.
Karakteristiek voor deze laatste twee talen is dat ze impliciet getypeerd zijn. Een type beschrijft de waarden die een expressie aan kan nemen, zoals "een getal", "een lijst met getallen", "een paar van twee karakters" of "een functie". De programmeur hoeft niet langer voor iedere expressie het type op te schrijven, maar kan vertrouwen op een krachtig mechanisme om automatisch de types af te leiden (te infereren). Tijdens het infereren van de ontbrekende types kunnen inconsistenties in een programma worden ontdekt, en deze worden vervolgens gerapporteerd aan de programmeur. Als er geen fout gevonden wordt, dan zijn alle functies in een programma gegarandeerd op een juiste manier toegepast. Door het controleren van de types kan een significant deel van de fouten worden geëlimineerd.
Het interpreteren van typeringsfoutmeldingen wordt in het algemeen als lastig ervaren, en vergt enige training. Voor de ervaren programmeur is dit geen probleem: in sommige gevallen zal er zelfs nauwelijks naar de foutmelding gekeken worden. Voor beginnende programmeurs is de situatie anders: zij zullen voornamelijk het gevoel krijgen te worden tegengewerkt door het type-inferentieproces aangezien de foutmeldingen niet voldoende duidelijk maken wat er fout is, en hoe dit verbeterd kan worden. Deze onduidelijkheid belemmert het aanleren en waarderen van een functionele programmeertaal. Dit proefschrift beschrijft een aantal technieken om betere typeringsfoutmeldingen te genereren voor een programmeertaal zoals Haskell.
Waarom is het lastig om duidelijke typeringsfoutmeldingen te rapporteren? Omdat het niet verplicht is alle types op te schrijven kan er gemakkelijk een mismatch ontstaan tussen de types verwacht door de programmeur en de types afgeleid door de compiler. Dit soort verschillen kan elders in het programma problemen veroorzaken. Daarnaast ondersteunt Haskell hogere-orde functies (functies kunnen als argument meegegeven worden aan functies) en polymorfie (een functie kan worden gebruikt met verschillende types). Beide concepten zijn een extra uitdaging voor het type-inferentiemechanisme.
Het rapporteren van duidelijke foutmeldingen komt feitelijk neer op het bijhouden van voldoende informatie en het op een handige manier organiseren van deze informatie. Foutmeldingen van traditionele inferentie-algoritmen hebben te lijden onder de mechanische wijze waarop de algoritmen te werk gaan. Het is beter om van deze benadering af te stappen en een programma in z'n geheel te bekijken zoals een expert dat zou doen. Een dergelijke globale analyse kan gebruik maken van een aantal heuristieken die de kennis van een deskundige vastleggen. Deze heuristieken kunnen onder meer bereiken dat veelgemaakte fouten worden herkend, en dat zij op een inzichtelijke manier worden gemeld aan de programmeur.
Het bovenstaande doel hebben we bereikt door gebruik te maken van constraints. Deze aanpak is ook voor andere programma-analyses uiterst succesvol gebleken. Een constraintverzameling beschrijft nauwkeurig de relaties tussen de types in een programma, en levert een natuurlijke splitsing op van de specificatie van de analyse (het verzamelen van de constraints) en de implementatie (het oplossen van de constraints). Deze splitsing heeft als pluspunt dat diverse oplossingsmethoden voor een constraintverzameling naast elkaar kunnen bestaan. Meerdere oplossingsmethoden zijn ondergebracht in het Top framework voor type-inferentie met goede foutmeldingen.
Het Top framework stelt vertalerbouwers in staat om een compiler op eenvoudige wijze uit te breiden met type-inferentie, daarbij gebruikmakend van allerlei technieken voor het genereren van goede foutmeldingen. De naam van dit framework staat enerzijds voor "Typing Our Programs" en anderzijds voor het symbool top uit de wiskunde, dat een foutsituatie representeert. Een uitgangspunt bij het ontwerp van Top is dat het inferentieproces kan worden afgestemd op de wensen en de deskundigheid van een programmeur. Deze flexibiliteit is noodzakelijk aangezien de gewenste informatie bij een foutmelding nogal persoonlijk is. Eén algoritme voor type-inferentie dat optimaal functioneert voor iedereen bestaat om deze reden niet. Top is gebaseerd op constraints, en maakt de aanname dat iedere constraint zijn eigen informatie met zich meedraagt. Deze informatie beschrijft bijvoorbeeld waarom de constraint is gegenereerd, en waar hij vandaan komt uit het oorspronkelijke programma. Verder kan de informatie van een constraint heuristieken aansturen, of een foutmelding aandragen.
Naast het verzamelen en het oplossen van constraints onderscheidt het framework nog een extra fase: het ordenen van de verzamelde constraints alvorens deze worden opgelost. De volgorde waarin constraints worden afgehandeld is niet relevant voor de oplossing die voor een verzameling gevonden wordt, maar beïnvloedt wel in sterke mate het moment waarop een inconsistentie wordt ontdekt, en welke fout er wordt gerapporteerd. Dit geldt in het bijzonder als de constraints één voor één bekeken worden. Een globale oplossingsstrategie heeft hier minder last van. Een ordening komt tot stand door eerst een constraintboom op te bouwen en deze vervolgens af te breken met een boomwandeling naar keuze. Hiermee kunnen klassieke algoritmen uit de literatuur (zoals W [11] en M [36]) worden nagebootst, en kan er geëxperimenteerd worden met variaties op deze algoritmen.
Het Top framework biedt naast een standaard oplossingsmethode ook een gespecialiseerde methode die het mogelijk maakt om zeer gedetailleerd een inconsistentie in een constraintverzameling uit te leggen. Hierbij wordt gebruik gemaakt van een typeringsgraaf. Dit is een geavanceerde datastructuur voor het representeren van substituties, met als kenmerkende eigenschap dat een substitutie zich ook in een inconsistente toestand kan bevinden. Met deze datastructuur kan een programma globaal worden geïnspecteerd, en kunnen heuristieken worden ingezet ter verbetering van de foutmeldingen. Hoewel deze oplossingsmethode meer rekentijd vergt dan de standaardmethode, kan de analyse nog steeds binnen redelijke tijd worden voltooid.
Tenslotte biedt Top de mogelijkheid om door middel van een eenvoudig te gebruiken scriptingtaal de foutmeldingen van buitenaf te beïnvloeden, en deze in te richten naar eigen smaak. Met behulp van directieven kan het type-inferentieproces worden gestuurd. Deze technologie is met name waardevol gebleken in de context van domeinspecifieke programmeertalen. Zonder een compiler aan te hoeven passen kunnen foutmeldingen worden uitgedrukt in termen van concepten uit het probleemdomein in plaats van die uit de onderliggende programmeertaal. Een collectie van directieven is speciaal ontworpen om het negatieve effect dat overloading en typeklassen hebben op foutmeldingen te beperken. Ook voor andere programma-analyses zou een dergelijke scriptingtaal van waarde kunnen zijn.
De Helium compiler [26] is ontwikkeld aan de Universiteit Utrecht met als doel om precieze, gebruikersvriendelijke foutmeldingen te genereren. De compiler maakt gebruik van de technologieën uit het Top framework, en is inmiddels al enkele malen ingezet tijdens de introductiecursus Functioneel Programmeren aan de Universiteit Utrecht. Helium ondersteunt bijna de volledige Haskell 98 standaard [49], wat aantoont dat de concepten uit Top daadwerkelijk toegepast kunnen worden op een volwassen programmeertaal. Tevens ondersteunt de compiler de faciliteit om zelf directieven te definiëren. Er zijn twee artikelen in het Nederlands verschenen die de ondersteunende rol van Helium binnen het programmeeronderwijs toelichten [25, 24].
| [11] | L. Damas and R. Milner. Principal type schemes for functional programs. In POPL'82: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 207-212. ACM Press, 1982. |
| [24] | B. Heeren and D. Leijen. Functioneel programmeren met Helium. In NIOC 2004 Proceedings, pages 73-82. Passage, November 2004. |
| [25] | B. Heeren and D. Leijen. Gebruiksvriendelijke compiler voor het onderwijs. Informatie, 46(8):46-50, October 2004. |
| [26] | B. Heeren, D. Leijen, and A. van IJzendoorn. Helium, for learning Haskell. In Haskell'03: Proceedings of the ACM SIGPLAN Workshop on Haskell, pages 62-71. ACM Press, 2003. |
| [36] | O. Lee and K. Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):707-723, July 1998. |
| [49] | S. Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003. |