Computer Laboratory

Work in Progress, Drafts and Notes

•   (updated, April 2012) Mathematical Structures for Data Types with Restricted Parametericity
  
  Dominic Orchard and Alan Mycroft. Accepted for presentation at TFP 2012. [PDF]
  Based on a previous draft called "Structures on Subcategories in Haskell"
  

  Show abstract >>>

  Functional programming continues to adopt concepts from category theory to provide abstraction mechanisms for structuring programs. For example, many parametrically polymorphic data types are instances of functors and monads. Other parametric data types have their polymorphism restricted for implementation efficiency e.g. unboxed arrays require primitive element types Int, Float, etc. Traditionally, mathematical abstractions in Haskell are endofunctor-based, however such data types do not fit this model. This paper instead interprets restricted polymorphism as subcategory specification. Notions of functors, monads and comonads are redefined over (full and non-full ) subcategories, providing non-endofunctors (with distinct source and target categories), relative monads and relative comonads. These structures not only provide a more accurate model of restricted polymorphism but can also be defined within Haskell itself using GHC’s new constraint kinds extension.

•   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.

•   Coeffects: typing context-dependent computations using comonads
  
  Tomas Petricek, Dominic Orchard, and Alan Mycroft. Unpublished work in progress (Dec 2011).[submitted version] [version with appendices]
  

  Show details >>>

  Effect systems are a well-known static analysis technique for tracking effects by augmenting typing judgments with effect information. The monadic approach to structuring effects can be unified with the effect systems approach as shown by Wadler and Thiemann. In this paper we study coeffect systems which capture properties of context-dependent computations. We show the construction of a comonadic coeffect system via a tagged comonad structure. Examples and some theory discussion included.

Publications

•  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 fa- miliar 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 fam- ilies, 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. DOI
  [PDF + corrections]

  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
  [On SpringerLink]

Other

• (new, Feb 2012) The four Rs of programming language design

  Dominic Orchard
  Short essay included (non peer-reviewed) in addendum to ONWARD '11 Proceedings of the 10th SIGPLAN symposium on New ideas, new paradigms, and reflections on programming and software. 

Talks

• 27^th April 2012 - The Unreasonable Effectivness of (High School) Mathematics, 5^th Annual Jesus College Graduate Conference, Cambridge
• 23^rd Februrary 2012 - Coeffect systems: capturing context-dependence, University of Strathclyde, Mathematically Structured Programming Group Seminar, Glasgow (slides on request)
• 27^th October 2011 - The Four Rs of Programming Language Design, Onward! Essay Presentation, SPLASH 2011, Portland, Oregon, USA.
• 7^th October 2011 - Coeffect Systems and Typing - (with Tomas Petricek), CPRG Seminar, Computer Laboratory, Cambridge [slides]
• 7^th September 2011 - Efficient and Correct Stencil Computations via Pattern Matching and Type Checking - IFIP Working Conference on DSLs, DSL 2011, Bordeaux, France [slides]
• 2^nd September 2011 - Efficient and Correct Stencil Computations via Pattern Matching and Type Checking - CPRG Seminar, Computer Laboratory, Cambridge
• 2^nd June 2011 - Programming with Comonads and Codo Notation - Tallinn University of Technology, Institute of Cybernetics, Estonia [slides]
• 20^th May 2011 - When Monads and Comonads Overlap - CPRG Seminar, Computer Laboratory, Cambridge
• 13^th May 2011 - Programming with Comonads and Codo Notation - CPRG Seminar, Computer Laboratory, Cambridge
• 26^th November 2010 - repeat lecture - Mathematically Structuring Programming Languages - Research Students Lecture Course, Cambridge, UK. [slides, notes, and examples]
• 20^th August 2010 - Rethinking Language Design for Parallelization, Intel Labs, Santa Clara, California, USA [slides]
• 2^nd June 2010 - Programming with monads combined with comonads - ICFP PC Workshop 2010, Microsoft Research, Cambridge, UK [slides]
• 14^th May 2010 - lecture - Mathematically Structuring Programming Languages - Research Students Lecture Course, Cambridge, UK. [slides, notes, and examples]
• 21^st April 2010 - Haskell Type Constraints Unleashed - FLOPS 2010, Sendai, Japan (given as a video talk due to continued airflight restrictions in the UK at the time) [slides, video (277.6MB MPEG4), streaming video @ Vimeo]
• 17^th February 2010 - Haskell Type Constraints Unleashed - Fun in the Afternoon, Standard Chartered Bank, London [slides]
• 12^th February 2010 - Haskell Type Constraints Unleashed - CPRG Seminar, Computer Laboratory, Cambridge
• 19^th January 2010 - Ypnos: Declarative, Parallel Structured Grid Programming, DAMP '10, Madrid, Spain [slides]
• 20^th November 2009 - Ypnos: Declarative, Parallel Structured Grid Programming, CPRG Seminar, Computer Laboratory, Cambridge [slides]
• 1^st May 2009 - Programming Language Design, Jesus College Graduate Symposium '09 [slides]
• 7^th April 2009 - Lucian: Dataflow and Object Orientation - BCTCS '09, University of Warwick, UK [slides]
• 13^th March 2009 - Interoperation of Lucid's Dataflow paradigm and Object-orientation with a Coalgebraic Semantics - CPRG Seminar, Computer Laboratory, Cambridge

Teaching

I gave a lecture entitled "Mathematically Structuring Programming Languages" as part of the "Current Research Topics" course at the Cambridge Computer Laboratory in May, 2010 and again in November, 2010, as part of a series of talks given by students in the CPRG (lectures note, slides, errata, and examples).

I have supervised, or am currently supervising, the following courses:

• Semantics (Michaelmas and Lent Term, 2009-2012)
• Concepts in Programming Languages (Easter term, 2010-2011)
• Optimising Compilers (Michaelmas term, 2008-2009)

  Extra explanatory notes for the constraint based analysis.

• Comparative Architectures (Lent Term, 2009)

I have supervised Part II (final year) projects from 2009-2012. Please get in touch if you're interested in me supervising your Part II project.
Previous projects supervised:

• Parallelisation of Java for Graphics Processors - Peter Calvert (2009-2010)
• Reconsidering Lucid - a modern approach - Jonas Kaiser (2009-2010)

Academic

I received my MEng in Computer Science in July 2008 from the Department of Computer Science, Universiy of Warwick.