Fetch the table of contents as a PDF file (110K).
Generic programming adds a new dimension to the parametrisation of programs by allowing programs to be dependent on the structure of the data that they manipulate. Apart from the practical advantages of improved productivity that this offers, a major potential advantage is a substantial reduction in the burden of proof -- by making programs more general we can also make them more robust and more reliable. These lectures discuss a theory of datatypes based on the algebra of relations which forms a basis for understanding datatype-generic programs. We review the notion of parametric polymorphism much exploited in conventional functional programming languages and show how it is extended to the higher-order notions of polymorphism relevant to generic programming.
These lectures will be about collection types and nested relational algebra, and the extension of this material for semi-structured data and XML.
Categorical type theory is the study of connections between formal type theory and category theory. Type theory is the mathematical study of type systems, such as those which appear in typed programming languages. By studying type systems in a systematic and formal way, we hope to improve the quality, performance and reliability of programming languages. For example, we might be able to show that if a program type checks, then it is safe, meaning that certain kinds of run time error cannot occur. Type systems can also provide frameworks for genericity, such as polymorphism. Category theory provides a very general language within which one can study mathematical objects via transformations of the objects, rather than the internal structure of the objects themselves; for example we might describe a set simply by stating that it is in bijection with another set. Here the "transformation" is a function. A category is a particular collection of objects together with a particular collection of transformations.Although categories and type systems appear to be rather different at first sight, there can be intimate connections. These lectures provide an introduction to categorical type theory which is slanted towards applications in computing science, and in particular to generic programming.
We shall assume some elementary knowledge of type systems. Although we shall review the category theory we need, it would be helpful to do some reading in advance. Suitable texts are:
(Note that there are a number of other excellent texts on the market.)
- M. Barr and C. Wells, Category Theory for Computing Science, Prentice Hall, 1990, International Series in Computer Science.
- R. L. Crole, Categories for Types, Cambridge University Press, 1993, Cambridge Mathematical Textbooks.
- S. Mac Lane, Categories for the Working Mathematician, Springer Verlag, 1971, volume 5, Graduate Texts in Mathematics.
- B. C. Pierce, Basic Category Theory for Computer Scientists, The MIT Press, Foundations of Computing Series, 1991.
This tutorial presents mathematical techniques as a toolbox for software architects, and as a foundation for application frameworks to develop architectural design environments that are independent of any Architectural Description Language (ADL). More precisely, a categorical semantics that builds on Goguen's approach to General Systems Theory and other algebraic approaches to specification, concurrency, and parallel program design, is proposed for the formalisation of concepts related to the gross modularisation of complex systems like "interconnection" (in particular connectors in the style defined by Allen and Garlan), "configuration", "instantiation", and "composition". This semantics is, essentially, ADL-independent, setting up criteria against which formalisms and tools can be evaluated according to the support that they provide for architectural design. In particular, it clarifies the role that the separation between computation and coordination plays in supporting architecture-driven approaches to software construction and evolution. It also leads to useful generalisations of the notion of connector, like higher-order connectors and the use of multiple formalisms in the definition of the glue and the roles, which allows connectors to be applied to programs or system components that can be implemented in different languages or correspond to "real-world" components. Finally we show how, based on the proposed categorical semantics, architectural notions can be put at the service of a software development method that ATX Software has been putting together for systems that need to be very agile in reacting to changes in business requirements.
A generic program is one that the programmer writes once, but which can be applied to values of many different data types. Typical examples include pretty printers, parsers, and comparison functions. We discuss both the theoretical underpinnings of the approach, and Generic Haskell, an extension of the functional programming language Haskell with which generic programs can be written. Instances of generic functions can be found in many programs such as structure editors or XML tools. These lectures discuss the library of Generic Haskell, and several applications of generic programming, such as an XML compressor, and the zipper, a data structure that is used in structure editors.
The object-oriented and the functional language communities have developed different approaches to abstraction and composition in programming. The functional approach relies on lambda abstraction and application. The object-oriented approach relies on named abstraction and implementation. We show how both approaches relate to each other, and how they can be combined in the construction of flexible component systems.Topics covered in the course:
- Functional abstraction and combinators
- Generic types and methods
- Polymorphic variants
- F-bounded polymorphism and Haskell's type classes
- Objects and classes
- Subtyping
- Abstract values
- Abstract types
- Mixin composition
- Component frameworks
Mon Tue Wed Thu Fri 09:00-09:45 RB PB RC JF RC 09:45-10:30 RH JF MO JJ RH 11:00-11:45 RH RC MO RB ws 11:45-12:30 PB RB PB RC ws 14:00-14:45 MO lab lab lab ws 14:45-15:30 MO lab lab lab ws 16:00-16:45 JJ JJ lab JF 16:45-17:30 JF RH lab PB
Bed-and-breakfast accommodation costs GBP58.50 per night for a single ensuite room, GBP38.50 per night for a standard room with a shared bathroom. Lunch, morning coffee and tea in the afternoon cost GBP16.50 per day, and the evening meal GBP17.60 per day (except on Thursday 29th, when there is a banquet costing GBP25.30).
On arrival in Oxford, just go straight to the college. The porter's lodge (on Woodstock Road, near the north-west corner) is open 24 hours a day. If you arrive by train, there is a direct bus (number 6) past college, but it only runs from the station on Sundays and in the evenings Monday to Saturday; however, there is a taxi rank at the station, or it is a 30-minute walk. If you arrive by bus (which is the most convenient method for most of the airports), the easiest thing to do is to stay on board until the last stop at the bus station, Gloucester Green; but bizarrely, there are no buses from there to college, and instead you should catch a taxi from the nearby taxi rank or take a 15-minute walk. Don't try to drive: there is no parking in Oxford, and the park-and-ride carparks on the outskirts are not recommended for overnight parking.