Reusability and Dependent Types
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
Publications
CACM Staff
(2012)
The beauty of simplicity
in Communications of the ACM
Gibbons J
(2011)
Just do it
GIBBONS J
(2013)
Modularising inductive families
in Progress in Informatics
Gibbons J
(2016)
Kernels, in a nutshell
in Journal of Logical and Algebraic Methods in Programming
Gibbons J
(2014)
Folding domain-specific languages
Gibbons, J
(2012)
Relating Algebraic and Coalgebraic Descriptions of Lenses
KO H
(2016)
Programming with ornaments
in Journal of Functional Programming
Ko H
(2011)
Modularising inductive families
| Description | One collection of key findings concern the structure of Dybjer's "inductive families" of datatypes, and specifically to McBride's notion of "ornaments" for relating more and less refined variants of structurally similar inductive families. Inductive families all datatypes to incorporate invariants, such as constraints on shape (size, balance) or contents (ordering); red-black trees are an example. Expressing these invariants within the datatype itself make it a type error to break the invariant, which will the type checker will guarantee to catch - rather than a mere logic error, which testing might miss. As well as preventing incorrect programs, more precise typing information also helps in constructing correct programs, by guiding the programmer or their programming tools in defining the right program in the first place. But having to introduce new datatypes just to capture new invariants is bad for reuse, because old libraries are inapplicable to the new datatypes. Ornaments show how to factor the new datatype into an old datatype plus additional information, paving the way for adapting the old library code to be reused on the new datatype. Ko's DPhil thesis "Analysis and Synthesis of Inductive Families" presents some elegant and useful results about ornaments. One such result relates to the mathematical foundations behind operations to combine ornamentations, which are needed to support refinement by multiple properties. Another is the introduction of relational algebraic ornaments, in which the properties may be defined in terms of relations rather than total functions; this lends itself very well to techniques for calculating the appropriate index structure for a particular problem, by lifting existing work on calculating programs that refine given relational specifications. A second collection of key findings concern the formal semantics of effectful coinductive functional programs: the precise treatment of computational effects such as I/O and state in otherwise pure, non-terminating but productive programs. Monads are well studied in pure, terminating functional programming; they play a big part in the design of Haskell. But ironically, given that Haskell is the foremost lazy functional programming language, our understanding of the interaction between effects and infinite data structures is much less mature. For example, we can easily write stateful Haskell programs that generate finite lists, and pure corecursive Haskell programs that generate infinite lists, but it is much trickier to write and reason about a stateful corecursive Haskell program generating an infinite list (because there is typically no final state). Pirog's DPhil thesis "Completely Iterative Monads in Semantics of Coinductive Programs" built on theoretical work by Elgot, Moss, Adamek, Milius and others on completely iterative monads, which are monads equipped with a productive corecursion scheme. His thesis presented a study that combined monads for effects with coalgebraic techniques for evolving behaviour. He introduced a formal coinductive semantics parametrised with a completely iterative monad, showing that it instantiates to a number of known approaches, based on metric spaces and final coalgebras. He also showed some results about composability of completely iterative monads; specifically, he explored coinductive resumptions, generalizing previous results by Moggi and by Hyland, Plotkin and Power. |
| Exploitation Route | Programming with ornaments would definitely benefit from some more direct language and/or library support, so there is scope for future work here. We have just submitted a paper exploring a worked example and identifying some desirable properties of that additional support. Pirog's work on the semantics of coinductive effectful programs addresses the meaning of pre-existing programs, but not directly how to construct those programs in the first place. There is work to be done in using these techniques actually to derive programs with desired behaviours from more abstract specifications of those behaviours. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | http://www.cs.ox.ac.uk/projects/rdtp/index.html |