Patricia Johann
Rutgers University
Parametric
Polymorphism, Observational Equivalence, and Monadic Computation
Abstract:
In this talk we
propose a calculus, called PolyComp, supporting polymorphism, type- and
term-level recursion, and computation (i.e., monadic) types. We give
PolyComp an operational semantics, which we use to construct parametric
models for it. We show that equivalence in these models coincides with
corresponding notions of observational equivalence and that these, in
turn, depend on the types at which observations can be made. Finally,
we use our models to derive operational properties of PolyComp which
are independent of the choice of monad, and also discuss how monads
which model specific computational effects can be incorporated into our
framework. Successfully incorporating new language features into
parametric models of observational equivalence is nontrivial because
operational techniques are often not modular. In particular, term-level
recursion typically does not interact well with other features. To our
knowledge, ours is the first parametric model of observational
equivalence for a calculus supporting all the features of PolyComp.
This
is joint work with Neil Ghani.
Principles
of Programming Seminars