We show that the syntactically rich notion of inductive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. Indexed containers generalize simple containers, capturing strictly positive families instead of just strictly positive types, without having to extend the core type theory. Other applications of indexed containers include data type-generic programming and reasoning about polymorphic functions. The construction presented here has been formalized using the Agda system.

Spin-exchange optical pumping (SEOP) has been widely used to produce enhancements in nuclear spin polarisation for hyperpolarised noble gases. However, some key fundamental physical processes underlying SEOP remain poorly understood, particularly in regards to how pump laser energy absorbed during SEOP is thermalised, distributed and dissipated. This study uses in situ ultra-low frequency Raman spectroscopy to probe rotational temperatures of nitrogen buffer gas during optical pumping under conditions of high resonant laser flux and binary Xe/N 2 gas mixtures. We compare two methods of collecting the Raman scattering signal from the SEOP cell: a conventional orthogonal arrangement combining intrinsic spatial filtering with the utilisation of the internal baffles of the Raman spectrometer, eliminating probe laser light and Rayleigh scattering, versus a new in-line modular design that uses ultra-narrowband notch filters to remove such unwanted contributions. We report a ~23-fold improvement in detection sensitivity using the in-line module, which leads to faster data acquisition and more accurate real-time monitoring of energy transport processes during optical pumping. The utility of this approach is demonstrated via measurements of the local internal gas temperature (which can greatly exceed the externally measured temperature) as a function of incident laser power and position within the cell.

Induction-induction is a principle for defining data types in Martin-Löf Type Theory. An inductive-inductive definition consists of a set A, together with an A-indexed family B : A → Set, where both A and B are inductively defined in such a way that the constructors for A can refer to B and vice versa. In addition, the constructors for B can refer to the constructors for A. We extend the usual initial algebra semantics for ordinary inductive data types to the inductive-inductive setting by considering dialgebras instead of ordinary algebras. This gives a new and compact formalisation of inductive-inductive definitions, which we prove is equivalent to the usual formulation with elimination rules.

We present a closed dependent type theory whose inductive types are given not by a scheme for generative declarations, but by encoding in a universe . Each inductive datatype arises by interpreting its description - a first-class value in a datatype of descriptions. Moreover, the latter itself has a description. Datatype-generic programming thus becomes ordinary programming. We show some of the resulting generic operations and deploy them in particular, useful ways on the datatype of datatype descriptions itself. Simulations in existing systems suggest that this apparently self-supporting setup is achievable without paradox or infinite regress.

It would not be too much of a stretch to imagine that dependent types will be the next big thing in programming language research. The key benefit is that by allowing types to be indexed by data, it is possible to expose more and more of the structure that lies behind the programs we write. This leads to many pay-offs, especially in refined program control and in program verification. The appearance of GADTs in Haskell has shown that there is an appetite for this kind of type discipline in the functional programming community; we believe, however, that the full benefits will only be seen with a language that is designed from the ground up around the idea of dependent types. The Epigram project has been at the fore-front of research in to dependently typed functional programming since 2004 [4]. While its initial prototype implementation proved to be as notorious as it was influential - It nonetheless provided inspiration for many features in the latest version of the Agda programming language [5], and beyond. After a long period of development hell, the Epigram team [2] are well on the way to being able to release a system that will finally put the toys that we've been working on in the hands of people who are impatient to have them, including ourselves. We hope that the real impact of Epigram 2 will, once again, be its influence on other, more mature, languages. The key motivation to Epigram remains that the solution to many of the challenges to writing programs in dependently typed languages lies with the types themselves. By explaining, using the type system, what the problem is, we can then use the system to help us find the solution - this is the power of dependent types at work. In this demonstration, I will introduce the current state of the system and will show off some of the new features, which we hope will be of interest the MSFP audience. Of the new elements, the most fundamental change is in the underlying Type Theory, which is based on Observational Type Theory (OTT) [1]. Thanks to OTT, Epigram 2 provides the ability to reason extensionally about programs, while for the first time maintaining decidable type checking. I will also demonstrate how it has been possible to extended the equality to allow certain algebraic properties, for instance the functor laws, to hold definitionally. Our Type Theory also implements a reflective approach to data types [3], we will see how we can use this to write generic programs inductively over the structure of data types.

In order to represent, compute and reason with advanced data types one must go beyond the traditional treatment of data types as being inductive types and, instead, consider them as inductive families. Strictly positive types (SPTs) form a grammar for defining inductive types and, consequently, a fundamental question in the the theory of inductive families is what constitutes a corresponding grammar for inductive families. This paper answers this question in the form of strictly positive families or SPFs. We show that these SPFs can be used to represent and compute with a variety of advanced data types, that generic programs can naturally be written over the universe of SPFs and that SPFs have a normal form in terms of indexed containers which are based upon the shapes and positions metaphor. Finally, we validate ou computational perspective by implementing SPFs in the programming language Epigram and, further, comment on how SPFs provide a meta-language for Epigram's data types.

In these lecture notes we give an overview of recent research on the relationship and interaction between two novel ideas in (functional) programming: Generic programming. Generic programming [15,22] allows programmers to explain how a single algorithm can be instantiated for a variety of datatypes, by computation over each datatype’s structure. Dependent types. Dependent types [29,38] are types containing data which enable the programmer to express properties of data concisely, covering the whole spectrum from conventional uses of types to types-as-specifications and programs-as-proofs.

Programming languages with an expressive language for defining data types often suffer from an excess in boiler-plate code and lack of re-usable, extendible libraries. Dependently typed programming languages are especially prone to such problems. With dependent types one can specify any number of relationships between data and types, to better specify the correct behaviour of programs. Thus one might begin with a single list type and extend it to lists on a known length, or ordered lists, or ordered lists of a known length. The possibilities are endless. Each of these ‘list-like’ structures will support some kind of functorial map, yet each new variant must come with a new definition of map that looks rather like all the others. Epigram is a dependently typed functional programming language which suffers from just this proliferation of types. This thesis suggests a solution to the data type proliferation problem for Epigram, combining universes and generic programming. Universes are a means to abstract over specific classes of types. Generic or polytypic programming is a technique by which functions are specialised on the structure of the type of their arguments. By using universes to abstract over the syntax of a class of data types, generic programming can be incorporated into Epigram without extending the language. Thus, functions like map can be defined once, not just for list like structures but a whole range of types. The story begins with a class of simple types which are given a purely syntactic treatment and a second, semantic, interpretation, based on the theory of containers. The syntactic and semantic views permit complimentary access to generic programming with these types. It is then shown that the generalisation of these techniques to a rich class of types, is not a difficult jump. The system that results is strong enough to allow generic programming for any data type that can be defined in Epigram.

In order to represent, compute and reason with advanced data types one must go beyond the traditional treatment of data types as being inductive types and, instead, consider them as inductive families. Strictly positive types (SPTs) form a grammar for defining inductive types and, consequently, a fundamental question in the the theory of inductive families is what constitutes a corresponding grammar for inductive families. This paper answers this question in the form of strictly positive families or SPFs. We show that these SPFs can be used to represent and compute with a variety of advanced data types, that generic programs can naturally be written over the universe of SPFs and that SPFs have a normal form in terms of indexed containers which are based upon the shapes and positions metaphor. Finally, we validate ou computational perspective by implementing SPFs in the programming language Epigram and, further, comment on how SPFs provide a meta-language for Epigram's data types.

In this paper we use the Epigram language to define the universe of regular tree types—closed under empty, unit, sum, product and least fixpoint. We then present a generic decision procedure for Epigram’s in-built equality at each type, taking a complementary approach to that of Benke, Dybjer and Jansson [7]. We also give a generic definition of map, taking our inspiration from Jansson and Jeuring [21]. Finally, we equip the regular universe with the partial derivative which can be interpreted functionally as Huet’s notion of ‘zipper’, as suggested by McBride in [27] and implemented (without the fixpoint case) in Generic Haskell by Hinze, Jeuring and Löh [18]. We aim to show through these examples that generic programming can be ordinary programming in a dependently typed language.

We begin by revisiting the idea of using a universe of types to write generic programs in a dependently typed setting by constructing a universe for Strictly Positive Types (SPTs). Here we extend this construction to cover dependent types, i.e. Strictly Positive Families (SPFs), thereby fixing a gap left open in previous work. Using the approach presented here we are able to represent all of Epigram’s datatypes within Epigram including the universe of datatypes itself.

The phenomenon of nuclear magnetic resonance (NMR) was first observed in the immediate post second-world-war period by two American physicists, working independently: Bloch at Stanford and Purcell at Harvard. Their observations were reported in 1946 in the same volume of Physical Review and led to the joint award of the 1952 Nobel Prize for Physics. Once the details of the interaction had been worked out, and the chemical specificity had been appreciated, a period of instrumentational refinement followed before NMR took its place as arguably the most powerful analytical technique available to the organic chemist. The historical development of NMR and the basis of its analytical power are described in the companion article by Dr. J. Feeney.

Abstract We begin by revisiting the idea of using a universe of types to write generic programs,in a dependently,typed setting by con- structing a universe for Strictly Positive Types (SPTs). Here we extend this construction to cover dependent types, i.e. Strictly Pos- itive Families (SPFs), thereby fixing a gap left open in previous work. Using the approach,presented here we are able to represent all of Epigram’s datatypes within Epigram including the universe of datatypes itself. Keywords Data type generic programming, dependently typed programming, Epigram

Summary Robin Milner coined the slogan well typed programs cannot go wrong, advertising the power of types in functional lan- guages like ML and Haskell to catch runtime errors. Nowadays, we can and should go further: dependently typed pro- gramming exploits the power of very expressive type systems to deliver stronger guarantees but also additional support for software development, using types to guide the development process. This is witnessed by a recent surge of language proposals with the goal to harness the power of dependent types, e.g. Haskell with GADTs (84, 85), Agda (90), Coq (18), Wmega (88), Concoqtion (83), Guru (89), Ynot (77), Epigram (68), and so on. However, expressive type systems have their price: more specific types frequently reduce the reusability of code, whose too-specific implementation type may not fit its current application. This phenomenon already shows up in the traditional Hindley-Milner style type system of ML and Haskell; it becomes even more prevalent in a dependently typed setting. Luckily, all is not lost: dependent types are expressive enough that they can talk about themselves reflectively, making meta- programming one of their potential killer applications (11), with the potential to combine expressive types and reusable software components. Based on and inspired by recent research at Nottingham on dependently typed programming (EPSRC EP/C512022/1) and container types (EPSRC EP/C511964/2) and at Oxford on datatype-generic programming (EPSRC GR/S27078/01, EP/E02128X/1) we plan to explore the potential of dependent types to deliver reusable and reliable software components. To achieve this, we intend to explore two alternative roads — reusability by structure and reusability by design — and express both within a dependently typed framework. Our programme is to build new tools extending the Epigram2 framework, investigate the underlying theory using container types, and most importantly establish novel programming patterns and libraries. We seek funding for an RA at Nottingham (Peter Morris, whose PhD laid much of the groundwork for this proposal), and two doctoral students (one each at Oxford and Strathclyde), together with appropriate support for equipment, coordination, travel, and dissimination (i.e. a workshop and a summer school)