[Prev][Next][Index][Thread]

types for Scott numerals (or re: Non Strictly Positive Datatypes)



While studying parametricity, Luca Cardelli, Gordon Plotkin, and 
I looked at typed versions of the Scott numerals.  A short discussion 
of Scott numerals appears in the note below, in LaTeX.   

In his recent message Martin Hofmann describes an example of useful, 
non-strictly-positive datatypes.  The Scott numerals provide another 
example.  This example is (I believe) quite simple and nice. 

Martin Abadi

-----------------------------------------------------------------

\documentstyle[11pt]{article}


\newcommand{\arrow}{\rightarrow}
\newcommand{\inn}{{\it in}}
\newcommand{\outt}{{\it out}}
\newcommand{\successor}{{\it succ}}
\newcommand{\ncase}{{\it case}}


\title{Types for the Scott numerals}
\author{Mart\'{\i}n Abadi
 \and 
Luca Cardelli
 \and
Gordon Plotkin} 

\date{February 18, 1993}

\begin{document}
\maketitle


In the untyped lambda calculus, the Scott numerals are defined by:
\begin{eqnarray*}
0 & = & \lambda x \lambda y.\: x\\
\successor & = & \lambda n \lambda x \lambda y.\: yn\\
\ncase & = & \lambda n\lambda a\lambda f.\: naf
\end{eqnarray*}
where $\ncase(n)(a)(f)$ returns $a$ if $n$ is 0 and $f(x)$ if $n$ 
is the successor of $x$ (see, e.g.,~\cite{W}).
The Scott numerals are distinguished
from the Church numerals by their ``linearity'': the bound variables of $0$, 
$\successor$, and $\ncase$ occur at most once in the bodies of these functions,
and the predecessor function $\lambda n.\: n(0)(\lambda x.\: x)$
can be computed trivially.

The Scott numerals can be typed in an extension of System F with
covariant recursive types.
We can take the type of the Scott numerals to be the solution to the equation
$S = \forall R.\: (R \arrow (S \arrow R) \arrow R)$:
\begin{eqnarray*}
0 & = & 
\Lambda R \lambda x:R \lambda y:(S \arrow R).\: x\\
& : & S\\
\successor & = & 
\lambda n:S \Lambda R \lambda x:R \lambda y:(S \arrow R).\: yn\\
& : & S \arrow S\\
\ncase & = & 
	\lambda n: S \Lambda R \lambda a: R \lambda f:(S \arrow R).\:
	nRaf\\
& : & S \arrow \forall R.\/(R \arrow (S \arrow R) \arrow R)\\
\end{eqnarray*}

Since $S$ is a covariant recursive type, it can be represented
by the System F type $M = \mu X .\: G[X]$ where 
$G[X] = \forall R.\: (R \arrow (X \arrow R) \arrow R)$
and $\mu X .\: G[X] = \forall X.\: ((G[X] \arrow X) \arrow X)$.
Let $N = G[M]$, and let $\inn: N \arrow M$ and $\outt: M \arrow N$
be the two halves of the isomorphism between $M$ and $N$.
Using $\inn$ and $\outt$, we can give new System F versions of 
0, $\successor$, and $\ncase$.  For this,
it turns out to be easiest to use $N$ rather than $M$ as the type of numbers.
We set:
\begin{eqnarray*}
0 & = & 
\lambda R\lambda x:R \lambda y:(M \arrow R).\: x\\
& : & N \\
\successor & = & 
\lambda n:N \Lambda R \lambda x:R \lambda y:(M \arrow R).\: y(\inn(n))\\
& : & N \arrow N\\
\ncase & = & 
	\lambda n: N \Lambda R \lambda a: R \lambda f:(N \arrow R).\:
	nRa(f \circ \outt)\\
& : & N \arrow \forall R.\/(R \arrow (N \arrow R) \arrow R)
\end{eqnarray*}

A numeral system based on $M$ 
can be obtained by working through the isomorphism,
or can be derived from scratch.
These two approaches yield somewhat different
results.  An abundance of superficially different numeral systems 
can be obtained, in part because neither $\inn \circ \outt$
nor $\outt \circ \inn$ is $\beta\eta$-equivalent to the identity.
Note that these numeral systems are not as efficient as the original one, 
or as the one based on the recursive type $S$: 
the two halves of the isomorphism $\inn$ and $\outt$ are not linear.


After considering these typed version of the Scott numerals,
we may wish to check that they are in fact isomorphic to the standard
natural numbers.
A direct argument uses many of the datatype constructions studied
in~\cite{PA}:
$$\begin{array}{llll}
M & \equiv & N 
	&\hbox{\rm by unfolding}\\
& \equiv & \mu X \forall R.\: ((1 \arrow R) \arrow (X \arrow R) \arrow R)
	&\hbox{\rm since $R \equiv (1 \arrow R)$}\\
& \equiv & \mu X \forall R.\: (((1 \arrow R) \times (X \arrow R)) \arrow R)
	&\hbox{by uncurrying}\\
& \equiv & \mu X \forall R.\: (((1 + X) \arrow R) \arrow R)
	&\hbox{turning a $\times$ into a $+$}\\
& \equiv & \mu X.\: (1 + X)
	&\hbox{\rm as                                                        
	$1 + X \equiv \mu R.\: (1 + X)$}
\end{array}$$


Similarly, we can give Scott versions for other familiar datatypes
using covariant recursive types. This works out particularly
well when recursive types can be defined up to
equality rather than just up to isomorphism.




\bibliographystyle{alpha}


\begin{thebibliography}{99}

\bibitem{PA} Gordon Plotkin and Mart\'{\i}n Abadi.
A logic for parametric polymorphism.
To appear in 
{\it Proceedings of the International Conference on Typed Lambda 
Calculi and Applications}, March 1993.

\bibitem{W} Christopher Wadsworth.
Some unusual $\lambda$-calculus numeral systems.
In {\it To H.~B.~Curry: Essays on Combinatory Logic, Lambda
Calculus and Formalism}, J.P.~Seldin and J.~R.~Hindley, eds., 
Academic Press, 1980.

\end{thebibliography}

\end{document}