reynolds-abstraction.tex

\documentclass{article}
\usepackage[margin=1in]{geometry}
\usepackage{mathpartir}
\usepackage{stmaryrd}

\newtheorem{theorem}{Theorem}

\title{Types, Abstraction, and Parametric Polymorphism}
\author{Typeset by: Colin Gordon and James Wilcox}

\begin{document}
\maketitle
This document re-presents much of Reynolds' classic \emph{Types, Abstraction, and Parametric
Polymorphism} paper in modern notation.  This is the paper that defined parametricity.

\section*{An Extended Lambda Calculus}
This section defines syntax, typing, and denotational semantics for a language that is subjectively either
slightly more general than STLC (James' opinion) or slightly more restricted than System F (Colin's
opinion).  The language is approximately STLC plus some unspecified types, or System F minus
explicit type quantification.

Syntax:
\newcommand{\cond}[3]{\ensuremath{\mathsf{if}(#1)\mathsf{then}\{#2\}\mathsf{else}\{#3\}}}
\[
    \begin{array}{lrcl}
        \textrm{Type Constants} & \kappa & \in & C \;\textrm{(includes booleans)}\\
        \textrm{Type Variables} & \tau & \in & T\\
        \textrm{Types} & \omega\in\Omega & ::= & \kappa \mid \tau \mid \omega \rightarrow \omega'
        \mid \omega \times \omega'\\
        \textrm{Variables} & x,y,z & \in & V\\
        \textrm{Constants} & k & \in & \kappa\\
        \textrm{Expressions} & e & ::= & k \mid x \mid e_1(e_2) \mid (\lambda x:\omega\ldotp e) \mid
        \langle e_1 , e_2 \rangle \mid e.1 \mid e.2 \mid \cond{e}{e_1}{e_2}
    \end{array}
\]

Type rules:
\begin{mathpar}
    \inferrule{ k \in \kappa_\omega }{ \pi\vdash k : \omega }
    \and
    \inferrule{ }{\pi\vdash x : \pi(x) }
    \and
    \inferrule{
        \pi\vdash e_1 : \omega\rightarrow\omega'\\
        \pi\vdash e_2 : \omega
    }{
        \pi\vdash e_1(e_2) : \omega'
    }
    \and
    \inferrule{
        \pi,v:\omega\vdash e : \omega'
    }{
        \pi\vdash \lambda v:\omega\ldotp e : \omega'
    }
    \and
    \inferrule{
        \pi\vdash e : \omega\\
        \pi\vdash e' : \omega'\\
    }{
        \pi\vdash\langle e,e'\rangle : \omega\times\omega'
    }
    \and
    \inferrule{
        \pi\vdash\langle e\rangle : \omega\times\omega'
    }{
        \pi\vdash\langle e.1\rangle : \omega
    }
    \and
    \inferrule{
        \pi\vdash\langle e\rangle : \omega\times\omega'
    }{
        \pi\vdash\langle e.2\rangle : \omega'
    }
    \and
    \inferrule{
        \pi\vdash b : \mathsf{bool}\\
        \pi\vdash e : \omega\\
        \pi\vdash e' : \omega
    }{
        \pi\vdash\cond{b}{e}{e'} : \omega
    }
\end{mathpar}

Next Reynolds defines denotational semantics --- an interpretation of the above language into set
theory in terms of a mapping $S$ assigning sets to type variables and a mapping $CS$ assigning sets
to the base types such that $CS(\mathsf{bool})=\{\mathsf{true},\mathsf{false}\}$.  Specifically, this is a pair of
interpretations: interpreting types as the set of elements they contain, and terms as functions from
the set of contexts to the set representing the appropriate type.

Reynolds calls the first function, denoting types as the set of their elements, $S^\#$.

\newcommand{\denote}[2]{\ensuremath{\llbracket #1 \rrbracket_{#2}}}
\[
    \begin{array}{rcl}
        \denote{\kappa}{S} & = & CS(\kappa)\\
        \denote{\tau}{S} & = & S(\tau)\\
        \denote{\omega\rightarrow\omega'}{S} & = & \denote{\omega}{S}\rightarrow\denote{\omega'}{S}\\
        \denote{\omega\times\omega'}{S} & = & \denote{\omega}{S}\times\denote{\omega'}{S}\\
    \end{array}
\]
Where $\rightarrow$ and $\times$ can be used in the meta language to note a set of functions, or the
cartesian product, respectively.

Reynolds lifts this first function again to type environments as $S^{\#\star}$:
\[
    \denote{\pi}{S} = \lambda {v\in\mathsf{dom}(\pi)}\ldotp\denote{\pi(v)}{S}
\]

Expression semantics: Reynolds defines $\mu_{\pi\omega}$ as a mapping from well-typed terms and
semantic mappings to functions from environments to set elements.  He assumes for each constant type
$\omega$ a mapping $\alpha_\omega : \kappa_\omega \rightarrow \denote{\omega}{S}$.
\newcommand{\edenote}[5]{\ensuremath{{}^{#1}_{#2}\llbracket #3\rrbracket_{#4}(#5)}}
\[
    \begin{array}{rcl}
        \edenote{\pi}{\omega}{-}{-}{-} & : & \{ e \mid \pi\vdash e : \omega \} \rightarrow
        \Pi_{S:\mathcal{S}} (\denote{\pi}{S}\rightarrow\denote{\omega}{S})\\
        \edenote{\pi}{\omega}{k}{S}{\eta} & = & \alpha_\omega\;k\\
        \edenote{\pi}{\omega}{v}{S}{\eta} & = & \eta\;v\\
        \edenote{\pi}{\omega'}{e_1(e_2)}{S}{\eta} & = &
            \edenote{\pi}{\omega\rightarrow\omega'}{e_1}{S}{\eta}(\edenote{\pi}{\omega}{e_2}{S}{\eta})\\
        \edenote{\pi}{\omega\rightarrow\omega'}{\lambda x:\omega\ldotp e}{S}{\eta} & = & f \;\textrm{such that}\;
            f\;x=\edenote{\pi,v:\omega}{\omega'}{e}{S}{\eta,v:x}
        \\
        \edenote{\pi}{\omega\times\omega'}{\langle e,e' \rangle}{S}{\eta} & = & 
            \langle
            \edenote{\pi}{\omega}{e}{S}{\eta}
            ,
            \edenote{\pi}{\omega'}{e'}{S}{\eta}
            \rangle
        \\
        \edenote{\pi}{\omega}{e.1}{S}{\eta} & = & \edenote{\pi}{\omega\times\omega'}{e}{S}{\eta}_1\\
        \edenote{\pi}{\omega'}{e.2}{S}{\eta} & = & \edenote{\pi}{\omega\times\omega'}{e}{S}{\eta}_2\\
    \end{array}
\]
This is a standard set-theoretic denotational semantics.

\section*{The Abstraction Theorem}
This section is the heart of the paper, establishing the main result.  The rest of the paper is a
mixture of connections to related work and (important!) generalizations (modulo the assumption in
Section 8 of a set-theoretic semantics for System F which Reynolds later proved could not exist).

\newcommand{\rel}[2]{\ensuremath{\mathsf{Rel}(#1, #2)}}

For two set assignments $S_1$ and $S_2$, a \emph{relation assignment} is a function of type:
\[
    \Pi_{\tau\in T}\rel{S_1\tau}{S_2\tau}
\]
We can lift a relation assignment $R$ from type variables to types:
\[
    R^{\#} : 
    \Pi_{\omega\in\Omega}\rel{S_1^{\#}(\omega)}{S_2^{\#}(\omega)}
\]

as follows
\[
    \begin{array}{rcl}
    R^{\#}(\kappa) & = & I(CS(\kappa))\\
    R^{\#}(\tau) & = & R\;\tau\\
    R^{\#}(\omega\rightarrow\omega') & = & R^{\#}(\omega)\rightarrow R^{\#}(\omega')\\
    R^{\#}(\omega\times\omega') & = & R^{\#}(\omega)\times R^{\#}(\omega')\\
    \end{array}
\]

And $R^{\#}$ can be lifted further to operating on type environments ($R^{\#\star}$) in the obvious
way.

This is enough for us to (re)state the major theorems of the paper.

The first is a statement that the identity relation carries through the liftings to types and type
environments just described.
\begin{theorem}[Identity Extension]
Suppose $IA$ is a relation assignment such that $IA\;\tau=I(S\;\tau)$ for some subset of type
variables $T_0$ ($\tau\in
T_0\subseteq T$).  Then
\begin{itemize}
\item $\forall \omega\ldotp FV(\omega)\subseteq T_0 \Rightarrow IA^{\#}(\omega) = I(\denote{\omega}{S})$, and
\item $\forall \pi\ldotp (\forall v\in\mathsf{dom}(\pi)\ldotp FV(\pi(v))\subseteq T_0) \Rightarrow
        IA^{\#\star}(\pi) = I(S^{\#\star}(\pi))$
\end{itemize}
\end{theorem}

\begin{theorem}[Abstraction Theorem (Parametricity)]
For relation assignment $R$ between set assignments $S_1$ and $S_2$, 
for all $\pi$, $\omega$, $e$ such that $\pi\vdash e : \omega$, and 
$\langle \eta_1, \eta_2\rangle\in R^{\#\star}\pi$,
\[
    \langle
    \edenote{\pi}{\omega}{e}{S_1}{\eta_1}
    ,
    \edenote{\pi}{\omega}{e}{S_2}{\eta_2}
    \rangle
    \in R^{\#}\omega
\]
\end{theorem}

Another way to state this second theorem in English is that for any well-typed expression $e$ assuming
some number of abstract types, given 2 instantiations of that type related by a relation $R$, if
two dynamic environment bindings are related by $R$ (suitably lifted), then the results of evaluting
$e$ in those two environments (corresponding to two instantiations of the abstract types) will also
be related by $R$.

To connect back to the introduction, given two dynamic environments for the two representations of
complex numbers, because the representations are in bijective correspondence, any expression
evaluated with input environments in bijective correspondence will produce outputs in bijective
correspondence.

The term ``parametricity'' was actually coined later by Phil Wadler in his ``Theorems for Free''
paper.

The rest of the paper expands these two theorems for various forms of type quantification/binding,
and relates to some other work on denotational models of typed lambda calculi.

\end{document}