Coherente impliciete resolutie

Type-gestuurde resolutie is een mechanisme binnen programmeertalen dat programmacode automatisch samenstelt met behulp van type-informatie. Enerzijds maakt deze resolutie een verscheidenheid aan krachtige impliciete programmeertaalconcepten mogelijk, zoals type classes in Haskell, implicits in Scala en traits in Rust. Met deze taalconcepten kan de programmeur code weglaten die door resolutie afgeleid wordt, waardoor programma’s compacter en makkelijker te lezen worden. Anderzijds kan onzorgvuldig ontworpen resolutie semantische dubbelzinnigheid in de programmeertaal introduceren en redeneertechnieken zoals “equational reasoning” bemoeilijken.

Gelukkig zijn er restricties die opgelegd kunnen worden om het resolutieme- chanisme te behoeden voor onvoorspelbaar en contra-intuïtief gedrag. Deze restricties kunnen variëren afhankelijk van het ontwerp van het mechanisme en resulteren in verschillende correcte taalconcepten. De correctheid van resolutie wordt formeel uitgedrukt onder de vorm van twee eigenschapen: coherentie, die semantisch eenduidigheid waarborgt, en stabiliteit, die equational reasoning waarborgt.

Dit werk stelt technieken voor om te redeneren over calculi die impliciet programmeren ondersteunen, een taak die danig bemoeilijkt wordt door de aanwezigheid van deze taalconcepten, en past ze toe op drie calculi om hun correctheid vast te stellen. Bovendien identificeren we aandachtspunten bij het ontwerp en de implementatie van type-gestuurde resolutie.