|
| EPSRC Reference: |
EP/E016146/1 |
| Title: |
Relational Parametricity for Computational Effects |
| Principal Investigator: |
Dr AK Simpson |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Lab. for Foundations of Computer Science |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research |
| Starts: |
01 October 2006 |
Ends: |
30 September 2007 |
Value (£): |
51,766
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
Mathematically, a computer program may be thought of as a function that maps possible input
values to the associated output values computed by the program. However, this is too simplistic.
In reality, programs perform additional non-functional behaviour . For example,
they modify the store, make nondeterministic choices, cause errors, etc.
Collectively, such non-functional behaviours are called "computational effects".
Polymorphism is an important device in programming that allows a program
to be used for many different types of input and output, rather than for just
a single type. Christopher Strachey coined the term "parametric polymorphism"
to describe polymorphic programs that apply the same uniform algorithm across
all types of input. In 1983, John Reynolds proposed that Strachey's notion
of parametricity could be modeled by a mathematical property asserting that
polymorphic programs should preserve certain relations between data of different
types. This notion of "relational parametricity" has since proved itself to
be very useful. In particular, it provides a powerful and useful principle
for proving behavioural equivalences of programs.
The notion of relational parametricity, as formulated by Reynolds, relies on the
assumption that programs are functions. The goal of the proposed research
is to study a generalized notion of relational parametricity that applies
to programs that perform effects.
Our research will build on a simple "metalanguage" for parametric polymorphism
with effects recently proposed by the principal investigator. The metalanguage
will be used as the basis for developing principles for reasoning about parametricity
in the presence of effects. Such principles will be presented in a formal logic.
The metalanguage will also be used as a target language for the translation of
different evaluation mechanisms for polymorphism, allowing the transfer of
the reasoning principles to realistic programming mechanisms. Finally, we
shall study instances of our metalanguage and logic in the context of
particular computational effects of interest, such as probabilistic choice
and so-called continuations (jumping mechanisms).
|
| Final Report Summary |
Mathematically, a computer program may be thought of as a function that maps possible input values to the associated output values computed by the program. However, this is too simplistic. In reality, programs perform additional non-functional behaviour . For example, they modify the store, make nondeterministic choices, cause errors, etc. Collectively, such non-functional behaviours are called "computational effects".
Polymorphism is an important device in programming that allows a program to be used for many different types of input and output, rather than for just a single type. Christopher Strachey coined the term "parametric polymorphism" to describe polymorphic programs that apply the same uniform algorithm across all types of input. In 1983, John Reynolds proposed that Strachey's notion of parametricity could be modeled by a mathematical property asserting that polymorphic programs should preserve certain relations between data of different types. This notion of "relational parametricity" has since proved itself to be very useful. In particular, it provides a powerful and useful principle for proving behavioural equivalences of programs.
The notion of relational parametricity, as formulated by Reynolds, relies on the assumption that programs are functions. The goal of this research project was to study a generalized notion of relational parametricity that applies to programs that perform effects.
Our research developed a simple "metalanguage" for parametric polymorphism with effects proposed by the principal investigator. The metalanguage was used as the basis for developing principles for reasoning about parametricity in the presence of effects. Such principles were presented by developing a formal logic embodying them. The metalanguage can be used as a target language for the translation of different evaluation mechanisms for polymorphism, allowing, in principle, the transfer of such reasoning principles to realistic programming mechanisms. Finally, we studied instances of our metalanguage and logic in the context of particular computational effects of interest, in particular so-called continuations (control mechanisms).
|
| Further Information: |
|
| Organisation Website: |
http://www.ed.ac.uk |
|
|