chapter2.tex

\chapter{Model of Computation}

To preserve the transparency of interoperation, ML and Scheme must not force Haskell to evaluate reducible expressions in Haskell boundaries in the incompatible evaluation contexts, and must force their evaluation in all other evaluation contexts. Haskell boundaries must be a new kind of value that ML and Scheme can force to become a reducible expression in certain evaluation contexts, and thereby force the evaluation of the inner Haskell reducible expressions to Haskell values and the conversion of those values to ML or Scheme.

Since ML and Scheme do not force Haskell to evaluate in some evaluation contexts, we must factor Haskell boundaries out of ML and Scheme evaluation context nonterminals, $\symcont$, into new evaluation context nonterminals. We name these new nonterminals $\symconf$ because they allow ML and Scheme to force Haskell to evaluate, and we rename the primary evaluation context nonterminals from $\symcont$ to $\symconu$ (unforced) because they do not. Likewise, we factor Haskell boundaries out of ML and Scheme value nonterminals, $\symvalt$,  into new value nonterminals. We name these new nonterminals $\symvalf$ (forced) and rename the old value nonterminals from $\symvalt$ to $\symvalu$ (unforced). We rename Haskell evaluation contexts and values to $\symconf$ and $\symvalf$, respectively.

In ML and Scheme, we tie $\symconf$ and $\symconu$ together by replacing $\symconu$ with $\symconf$ in the syntax and operational semantics in all evaluation contexts except the incompatible ones. Likewise, we tie $\symvalf$ and $\symvalu$ together by replacing $\symvalu$ with $\symvalf$ in the syntax and operational semantics in those same evaluation contexts. $\symconf$ evaluation contexts produce $\symvalf$ values, and $\symconu$ evaluation contexts produce $\symvalu$ values. $\symconu$ only applies to incompatible evaluation contexts, and $\symconf$ applies to all others. ML and Scheme use $\symconf$ to evaluate expressions. We rename the meta evaluation context from $\varconmt$ to $\varconm$.

Transparency is restored for interoperation in all cases with our changes to the model of computation of Matthews and Findler.

\begin{theorem}{Interoperation is transparent:}
\label{thmtransparent}
\begin{enumerate}
\item
\varexph
$\simeq$
\exphm
{
	\vartyh
}
{
	\vartym
}
{
	(
	\expmh
	{
		\vartym
	}
	{
		\vartyh
	}
	{
		\varexph
	}
	)
}
$\simeq$
\exphs
{
	\varcsh
}
{
	(
	\expsh
	{
		\varcsh
	}
	{
		\varexph
	}
	)
}
\item
\varexpm
$\simeq$
\expmh
{
	\vartym
}
{
	\vartyh
}
{
	(
	\exphm
	{
		\vartyh
	}
	{
		\vartym
	}
	{
		\varexpm
	}
	)
}
$\simeq$
\expms
{
	\varcsm
}
{
	(
	\expsm
	{
		\varcsm
	}
	{
		\varexpm
	}
	)
}
\item
\varexps
$\simeq$
\expsh
{
	\varcsh
}
{
	(
	\exphs
	{
		\varcsh
	}
	{
		\first
		{
			\varexps
		}
	}
	)
}
$\simeq$
\expsm
{
	\varcsm
}
{
	(
	\expms
	{
		\varcsm
	}
	{
		\first
		{
			\varexps
		}
	}
	)
}
\end{enumerate}
where $\simeq$ denotes observational equivalence \cite{felleisen09}.
\begin{proof}
By structural induction.
\end{proof}
\end{theorem}

The conversion of type abstractions between Haskell and ML was not straightforward. The application of a converted type abstraction cannot substitute the type argument into the nested expression because the type argument is meaningless in the nested expression's language. Instead, the application substitutes the type argument and a lump into the boundary's outer and inner types, respectively. Since the natural embedding requires the boundary's outer and inner types to be equal \cite{matthews07}, we use a new notion of equality called lump equality that allows lumps within the boundary's inner type to match any corresponding type in the boundary's outer type.

Figures \ref{figsymbols}--\ref{figsyntax2} present legends of symbol and syntax names; figure \ref{figunbrand} presents the unbrand function; figure \ref{figequality} presents the lump equality relation; figures \ref{fighs}--\ref{fighsos} present Haskell; figures \ref{figms}--\ref{figmsos} present ML; and figures \ref{figss}--\ref{figsmos} present Scheme.

\clearpage

\input{model/symbols.tex}

\clearpage

\input{model/syntax.tex}

\clearpage

\input{model/unbrand.tex}

\clearpage

\input{model/equality.tex}

\clearpage

\input{model/haskell/syntax.tex}

\clearpage

\input{model/haskell/typing-rules.tex}

\clearpage

\input{model/haskell/operational-semantics/haskell.tex}

\clearpage

\input{model/haskell/operational-semantics/ml.tex}

\clearpage

\input{model/haskell/operational-semantics/scheme.tex}

\clearpage

\input{model/ml/syntax.tex}

\clearpage

\input{model/ml/typing-rules.tex}

\clearpage

\input{model/ml/operational-semantics/ml.tex}

\clearpage

\input{model/ml/operational-semantics/haskell.tex}

\clearpage

\input{model/ml/operational-semantics/scheme.tex}

\clearpage

\input{model/scheme/syntax.tex}

\clearpage

\input{model/scheme/typing-rules.tex}

\clearpage

\input{model/scheme/operational-semantics/scheme.tex}

\clearpage

\input{model/scheme/operational-semantics/haskell.tex}

\clearpage

\input{model/scheme/operational-semantics/ml.tex}

\clearpage