Functional Techniques for Representing and Specifying Software

All software is represented as source code in a programming language. Th e programming language defines the meaning or semantics of the code, for example, its operational behaviour. Computational source code is often accompanied by additional specifications that define how the source code should be interpreted or provide additional information about the softw are’s semantics. They make it possible for programmers to express and ve rify that their software has the intended semantics and to express inter -component semantic assumptions. Good representations and specifications of software components are crucial for efficiently producing software t hat is reliable, efficient and secure, and for preserving these qualitie s during the software’s evolution.Many types of software compone nts and their desired semantic properties can be challenging to represen t and specify. In this work, I contribute novel functional techniques fo r the representation and specification of four types of software compone nts:<UL> Ad hoc polymorphic functions: functions whose behaviour depends on the t ypes of their arguments or result. I present instance arguments: a type system extension for representing ad hoc polymorphic functions in the de pendently-typed programming language Agda. Compared to existing proposal s, instance arguments do not introduce an additional structuring concept and ad hoc polymorphic functions using them are fully first-class. Furt hermore, they avoid introducing a separate, powerful form of type-level computation and existing Agda libraries using records do not need modifi cations to be used with them. My implementation has been part of Agda si nce version 2.3.0 and I demonstrate a variety of applications of instanc e arguments Context-free grammars: a standard way to define the syntax of formal lan guages. I present a technique for representing context-free grammars in an embedded domain-specific language (EDSL). It avoids the restrictions of existing parser combinator libraries using a novel explicit represent ation of recursion based on advanced type system techniques in the Haske ll programming language. As a byproduct, grammars are decoupled from set s of semantic actions. On the flip side, the approach requires the gramm ar author to provide a type- and value-level encoding of the grammar’s d omain and I can provide only a limited form of constructs like many. I d emonstrate the approach with five grammar algorithms, including a pretty -printer, a reachability analysis, a translation of quantified recursive constructs to standard ones, and an implementation of the left-corner g rammartransform. This work forms the basis of my grammar-combinators parsing library. Meta-programs: programs that generate or manipulate other programs. I pr esent a novel set of meta-programming primitives for use in a dependentl y-typed functional language. The meta-programs’ types provide strong and precise guarantees about the meta-programs’ termination, correctness an d completeness. The system supports type-safe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, meta -programs are written in the same style as normal programs and use the l anguage’s standard functional computational model. I formalise the new m eta-programming primitives, implement them as an extension of Agda , and provide evidence of usefulness by means of two compelling applicat ions in the fields of datatype-generic programming and proof tactics. Effect polymorphic software: programs that support arbitrary implementat ions of effectful APIs and only produce effects through those implementa tions. Static effectful APIs and global mutable state in object-oriented programming languages make it hard to modularly control effects. Object -capability (OC) languages solve this by enforcing that effects can only be triggered by components that hold a reference to the object represen ting the capability to do so. I study this encapsulation of effects thro ugh a formal translation to a typed functional calculus with higher-rank ed polymorphism (I use a subset of Haskell for presentation). Based on a n informal view of effect-polymorphism as the fundamental feature of OC languages, I translate an OC calculus to effect-polymorphic Haskell code , i.e. computations that are universally quantified over the monad in wh ich they produce effects. The types of my translations assert the object -capability property and I can show and exploit this using Reynolds’ par ametricity theorem. An important new insight is that current OC language s and formalisations leave one effect implicitly available to allcod e, without a capability: the allocation of new mutable state; adding a c apability for it has important theoretical and practical advantages. My work establishes a new link between object-capability languages and the well-studied fields of functional programming and denotational semantics .</UL>status: publishe