intro.tex

\section{Introduction}\label{sec:intro}
When implementing the type system of a programming language, we often face
a gap between the design described on paper and the actual implementation.
Sometimes there is only an ambiguous description in English (or in other
natural languages). Even when there is a mathematical description of
the type system on paper, there can be a gap between the description and
the implementation. Language designers and implementers can suffer from
this gap because it is difficult to determine whether a problem originated
from a flaw in the design or a bug in the implementation.
Having a declarative (i.e., structurally similar to the design)
and flexible (i.e., easily extensible) machine executable specification
is extremely helpful, especially for prototyping or testing
experimental extensions to the language's type system.  
Jones' attempt of \emph{Typing Haskell in Haskell} \cite{JonesTHiH99} is
an exemplary work that demonstrates the value of such a concise, declarative,
and machine executable specification: the authors report that 90+ pages of
Hugs type checker implementation in C could be specified in only 400+ lines of
readable Haskell script.

% In our work, we use Prolog to specify advanced polymorphic features of
% modern functional languages.
Logic programming languages like Prolog are natural candidates for
the purpose of specifying type systems that support type inference:
the syntax and semantics are designed to represent logical inference rules
(which is how type systems are typically formalized) and they offer native
support for unification (which is the basic building block of type inference
algorithms). As a result, type system specifications become even more succinct
in Prolog than in functional languages. More importantly, the specifications
are \emph{relational}, capturing both type checking and type inference
without duplication.

Our contributions are demonstrating
\begin{itemize}\vspace*{-1ex}
\item A relational specification for a polymorphic type system that can be
	executed for both purposes of type checking and type inference
	(\S\ref{ssec:HM}).
\item A succinct and declarative specification for several dimensions of
	polymorphism (type, type constructor, kind) in less than 35 lines
	of Prolog (\S\ref{ssec:HMtck}).
\item A specification that is easily extend from the prior specifications
	with several pragmatic features such as pattern matching,
	recursion schemes, and polymorphic recursion (with the help of
	a few type annotation) (\S\ref{sec:other}).
% We believe our specification is usable without expert knowledge
% in logic programming because we only used built-ins and fairly basic
% library predicates, not relying on any specialized frameworks.
\item A two-staged inference scheme for types and kinds using delayed goals
	(\S\ref{ssec:HMtck}):
	We discovered that kind inference can be delayed after type inference
	(it is in some sense quite natural).
% and relied on native unification
% in Prolog as much as possible.
% (which helped our specification to be more succinct).
\item A motivating example for a dualized view on variables
	in logic programming:
	Type variables are viewed as unifiable logic variables
	in type inference but they are viewed as concrete/atomic
	variables (or identifiers) in kind inference in our specification.
	Better way of organizing this concept is desirable to produce
	better relational specifications for polymorphic type systems.
\end{itemize}

We give a step-by-step tutorial style explanation of our specification in
\S\ref{sec:poly}, gradually extending from the Prolog specification of
the simply-typed lambda calculus. In \S\ref{sec:other}, we demonstrate
that our method of specification is flexible for extensions with
other language features. All our Prolog specification in \S\ref{sec:poly}
and \S\ref{sec:other} are tested on SWI Prolog 7.2 and its source code are
available online.\footnote{
	\url{http://kyagrd.github.io/tiper/} }\label{githubURL}
We contemplate on more challenging language features such as GADTs and
term indices in \S\ref{sec:futwork}, discuss related work in
\S\ref{sec:relwork}, and summarize our discussion in \S\ref{sec:concl}.