PhD Dissertation

• Programming contextual computations
  Dominic Orchard, University of Cambridge, 2014, Technical Report PDF
  
  Show abstract >>>

  Modern computer programs are executed in a variety of different contexts: on servers, handheld devices, graphics cards, and across distributed environments, to name a few. Understanding a program's contextual requirements is therefore vital for its correct execution. This dissertation studies contextual computations, ranging from application-level notions of context to lower- level notions of context prevalent in common programming tasks. It makes contributions in three areas: mathematically structuring contextual computations, analysing contextual program properties, and designing languages to facilitate contextual programming.

  Firstly, existing work which mathematically structures contextual computations using comonads (in programming and semantics) is analysed and extended. Comonads are shown to exhibit a shape preservation property which restricts their applicability to a subset of contextual computations. Subsequently, novel generalisations of comonads are developed, including the notion of an indexed comonad, relaxing shape-preservation restrictions.

  Secondly, a general class of static analyses called coeffect systems is introduced to describe the propagation of contextual requirements throughout a program. Indexed comonads, with some additional structure, are shown to provide a semantics for languages whose contextual properties are captured by a coeffect analysis.

  Finally, language constructs are presented to ease the programming of contextual computations. The benefits of these language features, the mathematical structuring, and coeffect systems are demonstrated by a language for container programming which guarantees optimisations and safety invariants.

  
  Abstract appears in PhD Abstracts, Graham Hutton, Journal of Functional Programming, 2015, 25(7).

Drafts

• Complexity bounds for container functors and comonads
  Dominic Orchard [PDF]
  To appear in special issue of Information and Computation based on an extended abstract from DICE 2015 (Workshop on Developments in Implicit Computational Complexity)

  Show abstract >>>

  Common category theory notions are useful for abstracting both semantics and programs, simplifying definitions and aiding reasoning. We argue that categorical descriptions can also be used to reason about program complexity. We calculate complexity bounds from the axioms of abstract category theory structures commonly used in programming and semantics, which imply opportunities for optimisations. We study functors and comonads in the context of programming with (finite) containers. Due to the abstract interface provided by the language of category theory, the inferred implicit complexity bounds and subsequent optimisations they imply are implementation agnostic (machine free).

Publications

• Combining Effects and Coeffects via Grading
  
  Marco Gaboardi, Shinya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu
  ICFP 2016, [preprint PDF]
  

  Show abstract >>>

  Effects and coeffects are two general, complementary aspects of program behaviour. They roughly correspond to computations which change the execution context (effects) versus computations which make demands on the context (coeffects). Effectful features include partiality, non-determinism, input-output, state, and exceptions. Coeffectful features include resource demands, variable access, notions of linearity, and data input requirements. The effectful or coeffectful behaviour of a program can be captured and described via type-based analyses, with fine grained information provided by monoidal effect annotations and semiring coeffects. Various recent work has proposed models for such typed calculi in terms of graded (strong) monads for effects and graded (monoidal) comonads for coeffects. Effects and coeffects have been studied separately so far, but in practice many computations are both effectful and coeffectful, e.g., possibly throwing exceptions but with resource requirements. To remedy this, we introduce a new general calculus with a combined effect-coeffect system. This can describe both the changes and requirements that a program has on its context, as well as interactions between these effectful and coeffectful features of computation. The effect-coeffect system has a denotational model in terms of effect-graded monads and coeffect-graded comonads where interaction is expressed via the novel concept of graded distributive laws. This graded semantics unifies the syntactic type theory with the denotational model. We show that our calculus can be instantiated to describe in a natural way various different kinds of interaction between a program and its evaluation context.

• Effect Systems Revisited — Control-Flow Algebra and Semantics
  
  Alan Mycroft, Dominic Orchard, Tomas Petricek
  "Semantics, Logic, and Calculi", 2016 Festschrift for Hanne and Flemming Nielson, LNCS 9560 [PDF] [Springer]

  Show abstract >>>

  Effect systems were originally conceived as an inference-based program analysis to capture program behaviour—as a set of (representations of) effects. Two orthogonal developments have since happened. First, motivated by static analysis, effects were generalised to values in an algebra, to better model control flow (e.g. for may/must analyses and concurrency). Second, motivated by semantic questions, the syntactic notion of set- (or semilattice-) based effect system was linked to the semantic notion of monads and more recently to graded monads which give a more precise semantic account of effects. We give a lightweight tutorial explanation of the concepts involved in these two threads and then unify them via the notion of an effect-directed semantics for a control-flow algebra of effects. For the case of effectful programming with sequencing, alternation and parallelism—illustrated with music—we identify a form of graded joinads as the appropriate structure for unifying effect analysis and semantics.

• Effects as sessions, sessions as effects
  
  Dominic Orchard, Nobuko Yoshida
  POPL 2016 [preprint PDF] [Artifact page].

  Show abstract >>>

  Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the lambda- calculus and its variants, the latter for the pi-calculus. In this paper we explore their relative expressive power. Firstly, we give an embedding from PCF, augmented with a parameterised effect system, into a session-typed pi-calculus (session calculus), showing that session types are powerful enough to express effects. Secondly, we give a reverse embedding, from the session calculus back into PCF, by instantiating PCF with concurrency primitives and its effect system with a session-like effect algebra; effect systems are powerful enough to express sessions. The embedding of session types into an effect system is leveraged to give a new implementation of session types in Haskell, via an effect system encoding. The correctness of this implementation follows from the second embedding result. We also discuss various extensions to our embeddings.

• Evolving Fortran types with inferred units-of-measure
  
  Dominic Orchard, Andrew Rice, Oleg Oshmyan.
  ICCS 2015 and selected for the special issue of the Journal of Computational Science. [pre-print PDF,Elsevier version].

  Show abstract >>>

  Dimensional analysis is a well known technique for checking the consistency of equations involving physical quantities, constituting a kind of type system. Various type systems for dimensional analysis, and its refinement to units-of-measure, have been proposed. In this paper, we detail the design and implementation of a units-of-measure system for Fortran, provided as a pre-processor. Our system is designed to aid adding units to existing code base: units may be polymorphic and can be inferred. Furthermore, we introduce a technique for reporting to the user a set of critical variables which should be explicitly annotated with units to get the maximum amount of unit information with the minimal number of explicit declarations. This aids adoption of our type system to existing code bases, of which there are many in computational science projects.

• Using session types as an effect system
  
  Dominic Orchard, Nobuko Yoshida.
  PLACES 2015 [pdf]

  Show abstract >>>

  Side effects are a core part of practical programming. However, they are often hard to reason about, particularly in a concurrent setting. We propose a foundation for reasoning about concurrent side effects using sessions. We show that session types are expressive enough to encode an effect system for stateful processes. This is formalised via an effect-preserving encoding of a simple imperative language with an effect system into the π-calculus with sessions and session types (into which we encode effect specifications). We demonstrate how this technique can be used to reason about, specify, and control the scope of concurrent side effects.

• Embedding effect systems in Haskell
  
  Dominic Orchard, Tomas Petricek.
  Haskell Symposium 2014 [PDF]
  

  Show abstract >>>

  Monads are now an everyday tool in functional programming for abstracting and delimiting effects. The link between monads and effect systems is well-known, but monads provide a much more coarse-grained view of effects. Whilst effect systems capture fine-grained information about the effects, monads provide only a binary view: effectful or pure.
  
  Recent theoretical work has unified fine-grained effect systems with monads using a monad-like structure indexed by a monoid of effect annotations (called parametric effect monads). This aligns the power of monads with the power of effect systems.
  
  This paper leverages recent advances in Haskell's type system (as provided by GHC) to embed this approach in Haskell, providing user-programmable effect systems. We explore a number of practical examples that make Haskell even better and safer for effectful programming. Along the way, we relate the examples to other concepts, such as Haskell's implicit parameters and coeffects.

• Temporal semantics for a live coding language
  
  Sam Aaron, Dominic Orchard, Alan Blackwell.
  Workshop on Functional Art and Music (FARM) 2014 [PDF]
  

  Show abstract >>>

  Sonic Pi is a music live coding language that has been designed for educational use as a first programming language. However, it is not straightforward to achieve the necessary simplicity of a first language in a music live coding setting, for reasons largely related to the manipulation of time. The original version of Sonic Pi used a 'sleep' function for managing time, blocking computation for a specified time period. However, while this approach was conceptually simple, it resulted in badly timed music, especially when multiple musical threads were executing concurrently. This paper describes an alternative programming approach for timing (implemented in Sonic Pi v2.0) which maintains syntactic compatibility with v1.0, yet provides accurate timing via interaction between real time and a "virtual time". We provide a formal specification of the temporal behaviour of Sonic Pi, motivated in relation to other recent approaches to the semantics of time in live coding and general computation. We then define a monadic model of the Sonic Pi temporal semantics which is sound with respect to this specification, using Haskell as a metalanguage.

• Coeffects: A calculus of context-dependent computation
  
  Tomas Petricek, Dominic Orchard, Alan Mycroft.
  ICFP 2014 [PDF]
  

  Show abstract >>>

  The notion of context in functional languages no longer refers just to variables in scope. Context can capture additional properties of the variables (usage patterns in linear logics; caching requirements in dataflow languages) as well as additional resources or properties of the execution environment (rebindable resources; platform version in a cross-platform application). The recently introduced notion of coeffects captures the latter, whole-context properties, but it failed to capture fine-grained per-variable properties. We remedy this by developing a generalized coeffect system with annotations indexed by a coeffect shape. By instantiating a concrete shape, our system captures previously studied flat (whole-context) coeffects, but also structural (per-variable) coeffects, making it more practically useful. We show that the structural system enjoys desirable syntactic properties and we give its categorical semantics using extended notions of indexed comonad. The examples presented in this paper are based on analysis of established language features (liveness, linear logics, dataflow, dynamic scoping) and we argue that such context-aware properties will also be useful for future development of langua

• A computational science agenda for programming language research
  
  Dominic Orchard, Andrew Rice.
  ICCS (International Conference on Computational Science) 2014 [preprint PDF]
  

  Show abstract >>>

  Scientific models are often expressed as large and complicated programs. These programs embody numerous assumptions made by the developer (e.g., for differential equations, the discretization strategy and resolution). The complexity and pervasiveness of these assumptions means that often the only true description of the model is the software itself. This has led various researchers to call for scientists to publish their source code along with their papers. We argue that this is unlikely to be beneficial since it is almost impossible to separate implementation assumptions from the original scientific intent. Instead we advocate higher-level abstractions in programming languages, coupled with lightweight verification techniques such as specification and type systems. In this position paper, we suggest several novel techniques and outline an evolutionary approach to applying these to existing and future models. One-dimensional heat flow is used as an example throughout.

• The semantic marriage of monads and effects (extended abstract)
  
  Dominic Orchard, Tomas Petricek, Alan Mycroft, 2013, [arXiv:1401.5391] (local PDF)
• Upgrading Fortran source code using automatic refactoring
  
  Dominic Orchard, Andrew Rice.
  WRT'13 (ACM Workshop on Refactoring Tools 2013, colocated with SPLASH 2013) [PDF]
  

  Show abstract >>>

  Many of the computer models used in scientific research have been developed in Fortran over many years. This evolutionary process means these models inevitably utilise deprecated features and idioms of the language that impede software maintenance. To mitigate this, we built CamFort, an open-source automated refactoring tool for upgrading Fortran source code. We describe functionality in CamFort for removing equivalence statements and common blocks, and for deriving structured data types, and we give examples of how these transformations can benefit codebase robustness.

• Automatic SIMD Vectorization for Haskell
  
  Leaf Petersen, Dominic Orchard, Neal Glew.
  Proceedings of ICFP 2013 (Boston, MA, USA) [PDF]
  

  Show abstract >>>

  Expressing algorithms using immutable arrays greatly simplifies the challenges of automatic SIMD vectorization, since several important classes of dependency violations cannot occur. The Haskell programming language provides libraries for programming with immutable arrays, and compiler support for optimizing them to eliminate the overhead of intermediate temporary arrays. We de- scribe an implementation of automatic SIMD vectorization in a Haskell compiler which gives significant vector speedups for a range of programs written in a natural programming style. We compare performance with that of programs compiled by the Glasgow Haskell Compiler.

• Coeffects: Unified static analysis of context-dependence
  
  Tomas Petricek, Dominic Orchard, and Alan Mycroft.
  Proceedings of ICALP'13 (Riga, Latvia) [PDF]
  

  Show abstract >>>

  Monadic effect systems provide a unified way of tracking effects of computations, but there is no unified mechanism for tracking how computations rely on the environment in which they are executed. This is becoming an important problem for modern software -- we need to track where distributed computations run, which resources a program uses and how they use other capabilities of the environment. We consider three examples of context-dependence analysis: liveness analysis, tracking the use of implicit parameters, and calculating caching requirements for dataflow programs. Informed by these cases, we present a unified calculus for tracking context dependence in functional languages together with a categorical semantics based on indexed comonads. We believe that indexed comonads are the right foundation for constructing context-aware languages and type systems and that following an approach akin to monads can lead to a widespread use of the concept.

• A Notation for Comonads
  
  Dominic Orchard and Alan Mycroft.
  LNCS post-proceedings of IFL 2012. [PDF] [code]
  

  Show abstract >>>

  The category-theoretic concept of a monad occurs widely as a design pattern for functional programming with effects. The utility and ubiquity of monads is such that some languages provide syntactic sugar for this pattern, further encouraging its use. We argue that comonads, the dual of monads, similarly provide a useful design pattern, capturing notions of context dependence. However, comonads remain relatively under-used compared to monads-due to a lack of knowledge of the design pattern along with the lack of accompanying simplifying syntax. We propose a lightweight syntax for comonads in Haskell, analogous to the do-notation for monads, and provide examples of its use. Via our notation, we also provide a tutorial on programming with comonads.

• The four Rs of programming language design
  Dominic Orchard
  Addendum to ONWARD '11 Proceedings of the 10th SIGPLAN symposium on New ideas, new paradigms, and reflections on programming and software.
  [PDF] [@ACM DL]
• Efficient and Correct Stencil Computation via Pattern Matching and Static Typing
  
  Dominic Orchard and Alan Mycroft
  IFIP Working Conference on Domain-Specific Languages, Bordeaux, September 2011 (DSL 2011')
  [PDF at the arXiv] [implementation]

  Show abstract >>>

  Stencil computations, involving operations over the elements of an array, are a common programming pattern in scientific computing, games, and image processing. As a programming pattern, stencil computations are highly regular and amenable to optimisation and parallelisation. However, general-purpose languages obscure this regular pattern from the compiler, and even the programmer, preventing optimisation and obfuscating (in)correctness. This paper furthers our work on the Ypnos domain-specific language for stencil computations embedded in Haskell. Ypnos allows declarative, abstract specification of stencil computations, exposing the structure of a problem to the compiler and to the programmer via specialised syntax. In this paper we show the decidable safety guarantee that well-formed, well-typed Ypnos programs cannot index outside of array boundaries. Thus indexing in Ypnos is safe and run-time bounds checking can be eliminated. Program information is encoded as types, using the advanced type-system features of the Glasgow Haskell Compiler, with the safe-indexing invariant enforced at compile time via type checking.

• Haskell Type Constraints Unleashed
  
  Dominic Orchard and Tom Schrijvers
  10^th International Symposium on Functional and Logic Programming, FLOPS 2010, Sendai, Japan, April 2010
  [On SpringerLink] [Author's Copy with corrections] | [Accompanying technical report] | [Prototype implementation]

  Show abstract >>>

  The popular Glasgow Haskell Compiler extends the Haskell 98 type system with several powerful features, leading to an expressive lan- guage of type terms. In contrast, constraints over types have received much less attention, creating an imbalance in the expressivity of the type system. In this paper, we rectify the imbalance, transferring familiar type-level constructs, synonyms and families, to the language of constraints, providing a symmetrical set of features at the type-level and constraint-level. We introduce constraint synonyms and constraint families, and illustrate their increased expressivity for improving the utility of polymorphic EDSLs in Haskell, amongst other examples. We provide a discussion of the semantics of the new features relative to existing type system features and similar proposals, including details of termination.

• Ypnos : Declarative Parallel Structured Grid Programming
  
  Dominic Orchard, Max Bolingbroke, and Alan Mycroft
  5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, DAMP '10. Madrid, Spain, 2010.
  [PDF + corrections] [ACM Portal]

  Show abstract >>>

  A fully automatic, compiler-driven approach to parallelisation can result in unpredictable time and space costs for compiled code. On the other hand, a fully manual approach to parallelisation can be long, tedious, prone to errors, hard to debug, and often architecture-specific. We present a declarative domain-specific language, Ypnos, for expressing structured grid computations which encourages manual specification of causally sequential operations but then allows a simple, predictable, static analysis to generate optimised, parallel implementations. We introduce the language and provide some discussion on the theoretical aspects of the language semantics, particularly the structuring of computations around the category theoretic notion of a comonad.

• muCell - Interdisciplinary Research in Modelling and Simulation of Cell Spatial Behaviour
  
  Dominic Orchard, Jonathan Gover, Lewis Herrington, James Lohr, Duncan Stead, Cathy Young, Sara Kalvala
  Reinvention: a Journal of Undergraduate Research, Volume 2, Issue 1, April 2009
  [Online version] | [PDF version] | [Shortened PDF version]
• Integrating Lucid's Declarative Dataflow Paradigm into Object-Orientation
  
  Dominic Orchard and Steve Matthews
  Mathematics in Computer Science, 2(1), November 2008
  [PDF - author's copy]   [On SpringerLink]

Articles

• Units-of-Measure Correctness in Fortran Programs
  
  Mistral Contrastin, Andrew Rice, Matthew Danish, Dominic Orchard, Computing in Science & Engineering 1521-9615/16, 2016 [PDF] [CiSE]
• Book review: Computational Semantics with Functional Programming by Jan van Eijck and Christina Unger
  
  Dominic Orchard, Journal of Functional Programming (April, 2014) [preprint PDF] [JFP online]
• The Unreasonable Effectiveness of (Basic Secondary School) Mathematics
  
  Dominic Orchard, Jesus College Annual Report 2012, (p.27-28) [magainze PDF] (has corrupted figure on p.28) [article PDF]

Old drafts and notes (some may be resurrected someday)

• Categorical Programming for Data Types with Restricted Parametericity
  
  Dominic Orchard and Alan Mycroft.
  (Rejected from the TFP 2012 post-proceedings) [Draft PDF].
  (An earlier version appeared in the pre-proceedings of TFP 2012 as "Mathematical Structures for Data Types with Restricted Parametricity".)
  

  Show abstract >>>

  Many concepts from category theory have proven useful as tools for program abstraction, particularly in functional programming. For example, many parametric data types admit operations defining a functor and related structures such as a monad. However, some parametric data types whose operations are restricted in their parametricity are not amenable to traditional category-theoretic abstractions in Haskell, despite appearing to satisfy the mathematical definitions. This paper explains the limitations of various traditional category-theoretic approaches in Haskell, giving a precise account of their category-theoretic meaning and the categorical implications of restricted parametricity arising from ad-hoc polymorphism provided by type classes in Haskell. Following from this analysis, we generalise Haskell's notions of functors, monads and comonads, making use of GHC's new constraint kinds extension, providing techniques for structuring programs with both unrestricted and restricted polymorphism.

• Should I use a Monad or a Comonad?
  
  Dominic Orchard. Unpublished work in progress (Dec 2011). [draft]
  

  Show details >>>

  Shall we be pure or impure? Today we will be pure- but how? This paper explores and formalises the situations in which both a monad and a comonad can be used to structure a particular notion of computation. Various example are considered, and discussion on chosing between a monad and a comonad is provided.