Abstraction, Composition, and Resolvable Ambiguity in Programming Language Implementation
Tid: Ti 2024-10-08 kl 13.00
Plats: Ka-Sal A (Östen Mäkitalo), Kistagången 16, Kista
Videolänk: https://kth-se.zoom.us/j/66561560361
Språk: Engelska
Ämnesområde: Datalogi
Respondent: Viktor Palmkvist , Programvaruteknik och datorsystem, SCS
Opponent: Associate Professor Jeremy Yallop, University of Cambridge
Handledare: David Broman, Programvaruteknik och datorsystem, SCS; Associate Professor Philipp Haller, Teoretisk datalogi, TCS; Assistant Professor Elias Castegren, Division of Computing Science, Department of Information Technology, Uppsala University
QC 20240916
Abstract
Att implementera ett programmeringsspråk är en omfattande utmaning. Detta är särskilt relevant för domänspecifika språk, där implementationsarbetet är än mer disproportionerligt gentemot den allmänna nyttan. Å andra sidan kan ett domänspecifikt språk ge stora produktivitetsvinster inom dess avsedda domän. För att uppnå sådan potential med en rimlig mängd arbete krävs bättre implementationsmetoder. Som väl är så tenderar implementationstekniska framsteg för domänspecifika språk även gynna generella programmeringsspråk och vice versa; denna avhandling är således relevant för båda.
Allmänt tenderar programmering att åstadkomma ökad produktivitet via abstraktion; något som avgränsar implementationsdetaljer till någon liten del av ett program eller utelämnar dem helt och hållet. Denna avhandling arbetar med abstraktioner inom tre områden: återanvändning av implementationsarbete mellan flera programspråksimplementationer, tvetydighet i programspråkssyntax, och automatisering av implementationsval för datastrukturer.
Inom det första området introducerar vi syncons, små användardefinierade språkkonstruktioner som beskriver syntax, namnbindningssemantik, och körsemantik. Den sistnämnda ges i form av makroexpansion till ett annat språk, som även det definieras m.h.a syncons. Ett språk konstrueras sedan genom att återanvända syncons från tidigare språk och konstruera nya i mån av behov.
Inom det andra området ger vi en formell definition av lösbar tvetydighet, vilket innebär att en programmerare kan skriva om ett tvetydigt program till en entydig form. Klassen språk där alla tvetydigheter är lösbara är strikt större än klassen entydiga språk, vilket ökar designfrihet; en språkdesigner behöver inte göra godtyckliga val för att åstadkomma en entydig grammatik, vilket typiskt sett krävs av moderna parsningsmetoder. Detta är användbart i ett flertal situationer; i denna avhandling fokuserar vi på tre fall: syntaktisk sammansättning, intuitiva grammatiker, och nya språkkonstruktioner som saknar allmänt kända konventioner. Vi tillhandahåller två metoder som stödjer lösbar tvetydighet: en som utökar kontextfria grammatiker och använder sig egen parser, och en som kan användas i en mer konventionell parser. Den förstnämnda är mer uttrycksfull, men språk definierade i den andra innehåller enbart lösbara tvetydigheter, vilket vi bevisar i Coq. Båda tillhandahåller en automatisk metod som finner alla entydiga former av tvetydiga program.
Inom det tredje området tillhandahåller vi en design där en användare kan definiera nya abstrakta typer, konkreta representationer, abstrakta operationer, och konkreta operationsimplementationer på ett utbyggbart sätt. Exempelvis kan nya bibliotek lägga till representationer, operationer, och operationsimplementationer till tidigare definierade abstrakta typer. Vi stödjer också representationsbyten, där en abstrakt typ kan använda olika representationer i olika delar av ett program. Vi tillhandahåller också en uppsättning automatiska lösare som väljer implementationer, antingen genom att prioritera optimalitet eller snabb analysis, plus en möjlighet att återanvända en tidigare lösning, även om programet ändrats något sedan dess.
Sammantaget bidrar denna avhandling till att ge större kontroll över abstraktionsnivåer i programmeringsspråk och deras implementationer, dels genom att höja abstraktionsnivån där det är fördelaktigt, men också genom att kräva detaljer och specificitet där det är önskvärt.