Relational Parametricity for Computational Effects

Mathematically, a computer program may be thought of as a function that maps possible inputvalues 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 programto be used for many different types of input and output, rather than for justa single type. Christopher Strachey coined the term parametric polymorphism to describe polymorphic programs that apply the same uniform algorithm acrossall types of input. In 1983, John Reynolds proposed that Strachey's notionof parametricity could be modeled by a mathematical property asserting thatpolymorphic programs should preserve certain relations between data of different types. This notion of relational parametricity has since proved itself tobe 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 theassumption that programs are functions. The goal of the proposed researchis to study a generalized notion of relational parametricity that appliesto programs that perform effects.Our research will build on a simple metalanguage for parametric polymorphism with effects recently proposed by the principal investigator. The metalanguagewill 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 ofdifferent evaluation mechanisms for polymorphism, allowing the transfer ofthe reasoning principles to realistic programming mechanisms. Finally, weshall study instances of our metalanguage and logic in the context ofparticular computational effects of interest, such as probabilistic choiceand so-called continuations (jumping mechanisms).