Computer Laboratory

News

June 2013
Leaf Petersen, Neal Glew, and I have had our paper Automatic SIMD Vectorization for Haskell accepted to ICFP 2013. Pre-print version to appear soon (or e-mail me).

April 2013
Submitted a paper to ICFP 2013 with Leaf Petersen and Neal Glew on SIMD vectorisation of GHC core.

Coeffects: unified static analysis of context-dependence (pdf), with Tomas Petricek and Alan Mycroft, accepted to ICALP 2013.

I am on the PC of IFL 2013, this year hosted at Radboud University, Nijmegen.

March 2013
A Notation For Comonads (pdf), with Alan Mycroft, accepted for publication in the post-proceeedings of IFL 2012.

Publications

•   (Jue, 2013) Automatic SIMD Vectorization for Haskell
  
  Leaf Petersen, Dominic Orchard, Neal Glew.
  ICFP 2013 (to appear)
  

  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.

•   (updated, May 2013) Coeffects: Unified static analysis of context-dependence
  
  Tomas Petricek, Dominic Orchard, and Alan Mycroft.
  (to appear) 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.
  (to appear) 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
  [On SpringerLink]

Old drafts and notes (to 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.

Articles

• The Unreasonable Effectiveness of (Basic Secondary School) Mathematics
  Dominic Orchard, Jesus College Annual Report 2012, (p.27-28) [PDF] (PDF version has corrupted figure on p.28)

Talks

• 13^th November 2012 - Programs in context - Intelligent and Adaptive Systems Research Group, Department of Computer Science, University of Warwick [slides]
• 5^th November 2012 - Programs in context - Digital Technology Group Seminar, Computer Laboratory, Cambridge
• 30^st August 2012 - A Notation for Comonads - Implementation and Application of Functional Languages 2012 (IFL'12), Oxford, UK [slides] [video].
• 22^nd June 2012 - A Notation for Comonads, Context, and Intensional Programming - Algebra of Programming informal seminar, Department of Computer Science, Oxford, UK
• 13^th June 2012 - Mathematical Structures for Data Types with Restricted Parametericity, Trends in Functional Programming 2012, St. Andrews, Scotland [slides]
• 8^th June 2012 - Mathematical Structures for Data Types with Restricted Parametericity, CPRG Seminar, Computer Laboratory, Cambridge
• 27^th April 2012 - The Unreasonable Effectivness of (High School) Mathematics, 5^th Annual Jesus College Graduate Conference, Cambridge [slides] [video]
• 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]
• 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 supervise Part II (final year) projects. I have written down some proposals for potential projects. Please get in touch if you are interested in me supervising your Part II project.
Previous projects supervised:

• Implementing the Codo Syntax for Comonads in GHC (2012-13)
• GPU accelerating the Ypnos programming language (2012-13)
• VisualLucid IDE - A visual approach to dataflow programming (2011-12)
• Accessing Standard ML Constructs From Java Across Language Domains (2011-12)
• Parallelisation of Java for Graphics Processors - Peter Calvert (2009-10)
• Reconsidering Lucid - a modern approach - Jonas Kaiser (2009-10)

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

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

  • Extra explanatory notes for the constraint based analysis.
  • I also contributed to the current supervision material.

• Comparative Architectures (Lent Term, 2009)

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 lectures given by students in the CPRG (lectures note, slides, errata, and examples).

Academic

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