main.tex

% vim: ts=2: sw=2: expandtab: autoindent: spell:
%%%%%%%%%%%%%%%%%%%%%%% file typeinst.tex %%%%%%%%%%%%%%%%%%%%%%%%%
%
% This is the LaTeX source for the instructions to authors using
% the LaTeX document class 'llncs.cls' for contributions to
% the Lecture Notes in Computer Sciences series.
% http://www.springer.com/lncs       Springer Heidelberg 2006/05/04
%
% It may be used as a template for your own input - copy it
% to a new file with a new name and use it as the basis
% for your article.
%
% NB: the document class 'llncs' has its own and detailed documentation, see
% ftp://ftp.springer.de/data/pubftp/pub/tex/latex/llncs/latex2e/llncsdoc.pdf
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\documentclass[runningheads,a4paper]{llncs}
\usepackage[T1]{fontenc}
\usepackage{CJKutf8}
\usepackage{amssymb}
\usepackage{amsmath}
\setcounter{tocdepth}{3}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage[hang,labelfont=bf]{caption}
\usepackage[normalem]{ulem}
%% \usepackage{xcolor}
%% \makeatletter
%% \def\squiggly{\bgroup \markoverwith{\textcolor{red}{\lower3.5\p@\hbox{\sixly \char58}}}\ULon}
%% \makeatother
\usepackage[square,numbers]{natbib}


\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\newcommand{\Fw}{\ensuremath{\mathrm{F}_\omega}}
\newcommand{\Fi}{\ensuremath{\mathrm{F}_i}}
\newcommand{\HMX}{\ensuremath{\mathrm{HM}(\mathcal{X})}}
\newcommand{\lProlog}{\ensuremath{\lambda}Prolog}
\newcommand{\aProlog}{\ensuremath{\alpha}Prolog}
\newcommand{\muKanren}{\ensuremath{\mu\text{Kanren}}}

\newcommand{\todo}[1]{{\marginpar{\scriptsize\textcolor{magenta}{#1}}}}
\newcommand{\TODO}[1]{\textcolor{magenta}{TODO: #1}}


\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{Executable Relational Specifications of Polymorphic Type Systems
  using Prolog% \\ {\small(to appear in FLOPS 2016)}
  }

% a short form should be given in case it is too long for the running head
\titlerunning{Executable Relational Specifications of Polymorphic Type Systems}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{Ki Yung Ahn\and Andrea Vezzosi
%% \thanks{Please note that the LNCS Editorial assumes that all authors have used
%% the western naming convention, with given names preceding surnames. This determines
%% the structure of the names in the running heads and the author index.}%
%% \and Ursula Barth\and Ingrid Haas\and Frank Holzwarth\and\\
%% Anna Kramer\and Leonie Kunz\and Christine Rei\ss\and\\
%% Nicole Sator\and Erika Siebert-Cole\and Peter Stra\ss er
}
%
\authorrunning{Executable Relational Specifications of Polymorphic Type Systems using Prolog}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{Portland State University, Portland, OR, USA\\
     \path|kya@pdx.edu| \\~\\
     Chalmers University of Technology, Gothenburg, Sweden\\
     \path|vezzosi@chalmers.se|
   }

%
% NB: a more complex sample for affiliations and the mapping to the
% corresponding authors can be found in the file "llncs.dem"
% (search for the string "\mainmatter" where a contribution starts).
% "llncs.dem" accompanies the document class "llncs.cls".
%

\toctitle{Executable Relational Specifications of Polymorphic Type Systems using Prolog}
\tocauthor{Executable Relational Specifications of Polymorphic Type Systems using Prolog}
\maketitle


\begin{abstract}
A concise, declarative, and machine executable specification of
the Hindley--Milner type system (HM) can be formulated using
logic programming languages such as Prolog. Modern functional
language implementations such as the Glasgow Haskell Compiler
support more extensive flavors of polymorphism beyond Milner's
theory of type polymorphism in the late '70s. We progressively extend
the HM specification to include more advanced type system features.
An interesting development is that extending dimensions of polymorphism
beyond HM resulted in a multi-staged solution: resolve the typing relations
first, while delaying to resolve kinding relations, and then resolve
the delayed kinding relations. Our work demonstrates that logic programing
is effective for prototyping polymorphic type systems with rich features of
polymorphism, and that logic programming could have been even more effective
for specifying type inference if it were equipped with better theories and
tools for staged resolution of different relations at different levels.
\keywords{Hindley--Milner, functional language, type system,
  type inference, unification, parametric polymorphism,
  higher-kinded polymorphism, type constructor polymorphism,
  kind polymorphism, algebraic datatype, nested datatype,
  logic programming, Prolog, delayed goals
%%         GADT,
%%         generalized algebraic datatype
        }
\end{abstract}


%%%%%% \section{Introduction}\label{sec:intro} %%%%%%%%%%%%%%%
\input{intro} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Polymorphic Type Inference Specifications in Prolog}
\label{sec:poly}
We start from a Prolog specification for the Hindley--Milner type system
(HM) in \S\ref{ssec:HM} and then extend the specification to support
type constructor polymorphism and kind polymorphism in \S\ref{ssec:HMtck}.

The following two lines should be loaded into the Prolog system
before loading the specifications in this paper. {\small\vspace*{-1ex}
\begin{verbatim}
  :- set_prolog_flag(occurs_check,true).
  :- op(500,yfx,$).
\end{verbatim} \vspace*{-.7ex} }\noindent
The first line sets Prolog's unification operator \verb|=| to perform an
occurs check, which is needed for the correct behavior of type inference.
The second line declares \verb|$| as a left-associative infix operator,
which is used to represent the application operator in the object language
syntax. For instance, {\small\verb|E1$E2|} is an application of
{\small\verb|E1|} to {\small\verb|E2|}. Note that \verb|$| is left associative
because we want \verb|E1$E2$E3| to mean \verb|((E1$E2)$E3)|.\footnote{
	We intentionallay adopted the same symbol as the application operator
	\texttt{\$} in the Haskell standard library. In contrast to the
	right-associative operator in Haskell, our operator represents
	the default function application most often denoted by empty spaces
	and left-associative by convention.}

\begin{figure}[b]
\begin{verbatim}
  type(C,var(X),       T1) :- first(X:T,C), instantiate(T,T1).
  type(C,lam(X,E), A -> B) :- type([X:mono(A)|C],E,B).
  type(C,X $ Y,        B ) :- type(C,X,A -> B), type(C,Y,A).
  type(C,let(X=E0,E1), T ) :- type(C,E0,A), type([X:poly(C,A)|C],E1,T).

  first(K:V,[K1:V1|Xs]) :- K = K1, V=V1.
  first(K:V,[K1:V1|Xs]) :- K\==K1, first(K:V, Xs).
  
  instantiate(poly(C,T),T1) :- copy_term(t(C,T),t(C,T1)).
  instantiate(mono(T),T).
\end{verbatim}
\vspace*{-3ex}
\caption{Executable Relational Specification of HM in Prolog}
\label{fig:HM}
\vspace*{-2ex}
\end{figure}
\subsection{HM}\label{ssec:HM}
The four rules defining the {\small\verb|type|} predicate in the specification
of HM (Fig.~\ref{fig:HM}) are almost literal transcriptions of the typing rules
of HM. The query {\small\verb|type(C,E,T)|} represents a typing judgment usually
denoted by $\texttt{C}\vdash\texttt{E}:\texttt{T}$ on paper, meaning that
the expression {\small\verb|E|} can be assigned a type {\verb|T|} under the
typing context {\small\verb|C|}. A typing
context is a list of bindings. There are two kinds of bindings in HM: 
monomorphic bindings ({\small\verb|X:mono(A)|}) and
polymorphic bindings ({\small\verb|X:poly(C,A)|}).
Expressions in HM are either variables ({\small\verb|X|}), lambda expressions
({\small\verb|lam(X,E)|}), applications ({\small\verb|E1$E2|}), or
\texttt{let}-expressions ({\small\verb|let(X=E0,E1)|}).

The first rule for finding a type ({\small\verb|T1|}) of a variable
({\small\verb|var(X)|}) amounts to instantiating
({\small\verb|instantiate(T,T1)|}) the type ({\small\verb|T|}) from
the first binding ({\small\verb|X:T|}) that matches the variable
({\small\verb|X|}) bound in the typing context ({\small\verb|C|}).
The two rules for lambda expressions and applications are self-explanatory.
The last rule for \texttt{let}-expressions introduces polymorphic bindings.
HM supports rank-1 polymorphic types (a.k.a. type schemes), which are
introduced by this polymorphic \texttt{let}-bindings.\footnote{ Here,
	in this subsection, we consider non-recursive bindings only 
	but the specification of HM can be easily modified to support
	recursive bindings (see \S\ref{ssec:letrec}).}
The typing context {\small\texttt{C}} inside the polymorphic binding
{\small\verb|poly(C,A)|} is the typing context of the \texttt{let}-expression
where \texttt{A} is being generalized.
%% The Prolog specification of HM is only 8 lines (excluding empty lines).



% Note that a polymorphic biding \verb|poly(C,A)| refers to
% the typing context \verb|C| of the \texttt{let}-expression.

The {\small\verb|instantiate|} predicate
cleverly implements the idea of the polymorphic instantiation in HM.
The built-in predicate {\small\verb|copy_term|} makes a copy of
the first argument and unifies it with the second argument. The copied version
is identical to the original term except that all the Prolog variables have been
substituted with freshly generated variables. The instantiation of a polymorphic
type {\small\verb|poly(C,T)|} is implemented as
{\small\verb|copy_term(t(C,T),t(C,T1))|}.
Firstly, a copied version of {\small\verb|t(C,T)|} is made.
Say {\small\verb|t(C2,T2)|} is the copied version with all variables
in both {\small\verb|C|} and {\small\verb|T|}
are freshly renamed in {\small\verb|C2|} and {\small\verb|T2|}.
Secondly, {\small\verb|t(C2,T2)|}
is unified with {\small\verb|t(C,T1)|}, which amounts to {\small\verb|C2=C|}
and {\small\verb|T2=T1|}. Because {\small\verb|C2|} is being unified with
the original context {\small\verb|C|}, all freshly generated variables in
{\small\verb|C2|} are unified with the original variables in \verb|C|.
Therefore, only the variables in {\small\verb|T|} that do not occur in its
binding context {\small\verb|C|} will effectively be freshly instantiated in 
{\small\verb|T1|}. For example, the result of 
{\small\verb|copy_term(t([X:T],Y->X),t([X:T],T1))|} is
{\small\verb|T1 = Y1->X|}, where only {\small\verb|Y|} is instantiated to
a fresh variable {\small\verb|Y1|} but {\small\verb|X|} stays the same
because it appears in the typing context {\small\verb|[X:T]|}. This exactly
captures generalization and instantiation of polymorphic types in HM.

One great merit of this relational specification is that it also serves as
a machine executable reference implementation. We can run it
for type checking: {\small \vspace*{-1ex}
\begin{verbatim}
  ?- type([], lam(x,var(x)), A -> A).         
  true .
\end{verbatim} \vspace*{-.7ex} }\noindent
as well as for type inference: {\small \vspace*{-1ex}
\begin{verbatim}
  ?- type([], lam(f,lam(x,var(f)$var(x))), T).
  T = ((_G1571->_G1572)->_G1571->_G1572) .
\end{verbatim} \vspace*{-.7ex} }\noindent
and, although it is not the focus of this work,
also for type inhabitation: {\small \vspace*{-1ex}
\begin{verbatim}
  ?- type([], E, A -> A).
  E = lam(_G1555, var(_G1555)) .
\end{verbatim} \vspace*{-.7ex} }

In the following sections, we discuss how to add polymorphic features
to the specification. The specifications with the extended features
also serve as machine executable reference implementations, which
are able to perform both type checking and type inference.





\subsection{HM + Type Constructor Polymorphism + Kind Polymorphism}
\label{ssec:HMtck}
Modern functional languages such as Haskell support rich flavors of
polymorphism beyond type polymorphism. For example, consider
a generic tree datatype
\[ \textbf{data}~\textit{Tree}~c~a
  ~=~ \textit{Leaf}\,~a ~\mid~ \textit{Node}~(c~(\textit{Tree}~c~a)) \]
where $c$ determines the branching structure at the \textit{Node}s and $a$
determines the type of the value hanging on the \textit{Leaf}s. For instance,
it instantiates to a binary tree when $c$ instantiates to a pair constructor
and a rose tree when $c$ instantiates to a list constructor.
The type system of Haskell infers that $c$ has kind $*\to*$ and
$a$ has kind $*$. That is, this generic tree datatype is polymorphic on
the unary type constructor variable $c$ as well as on the type variable $a$.
Haskell's type system is also able to infer types for polymorphic functions
defined over \textit{Tree}s, which may involve polymorphism over
type constructors as well as over types. Furthermore, recent versions of the
Glasgow Haskell Compiler support kind polymorphism \cite{GPH2012}.

The Prolog specification in Fig.~\ref{fig:HMtck} describes
type constructor polymorphism and kind polymorphism, in only 32 lines
(excluding empty lines). We get kind polymorphism for free because
we can reuse the same \verb|instantiate| predicate for kinds, which was
used for types in the HM specification. However, the instantiation for
types needs to be modified, as in \verb|inst_type|, to ensure that
the kinds of freshly generated type constructor variables match with
the corresponding variables in the polymorphic type. For example, each use of
$\textit{Node}\,::\,
 \forall\,c\;a\,.\;c\;(\textit{Tree}\;c\;a)\to\textit{Tree}\;c\;a\,$
generates two variables, say $c'$ and $a'$, and the type system
should make sure that $c'$ has the same kind ($*\to*$) as $c$
and $a'$ the same kind ($*$) as $a$.
The \verb|samekinds| predicate used in \verb|inst_type| generates such
kinding relations exactly for this reason. Other than ensuring same kinds for
freshly generated variables, \verb|inst_type| instantiates polymorphic types
just as \verb|instantiate| does. In the remainder of this section, we focus
our discussion on the modifications to support type constructor variables.

Supporting type constructor variables of
arbitrary kinds introduces the possibility of ill-kinded type (constructor)
formation (e.g., $F\,G$ when $F:*\!\to\!*$ but $G:*\!\to\!*$ \;or\; 
$A\!\to\!B$ when $A:*\!\to\!*$). In our Prolog specification, we use
the atomic symbol \verb|o| to represent the kind usually denoted by $*$
(e.g., in Haskell) because \verb|*| is predefined as a built-in infix
operator in Prolog. The \verb|kind| predicate transcribes the kinding rules
for well-formed kinds, which is self-explanatory (HM without
\texttt{let}-binding duplicated on the type level instead of term level).
% a type constructor variable must be bounded in
% the kinding context (\verb|KC|), a function type \verb|A->B| is
% a well-formed type (of kind \verb|o|) when both \verb|A| and \verb|B|
% are well-formed types (of kind \verb|o|), and a type constructor application
% \verb|F$G| is well-formed when \verb|F| is an arrow kind (\verb|K1->K2|)
% whose codomain matches with the kind (\verb|K1|) of its argument \verb|G|.
% A type that satisfies these three kinding rules are well-formed kinds, 
% or well-kinded.

The typing rules (\verb|type|) need some modifications from the rules of HM,
in order to invoke checks for well-kindedness using the kinding rules
(\verb|kind|). We discuss the modification in three steps.

The first step is to have the typing rules take an additional argument for
the kinding context (\verb|KC|) along with the typing context (\verb|C|).
%% Because the kinding rules require a kinding context.
The typing rules
should keep track of the kinding context in order to invoke \verb|kind|
from \verb|type|.  That is, we change the definition of the \verb|type|
predicate from \verb|type(C,...)| to \verb|type(KC,C,...)|.
%% Thus, we add another argument to \verb|type| for
%% the kinding context

\begin{figure} % 32 lines
\begin{verbatim}
kind(KC,var(Z),K1) :- first(Z:K,KC), instantiate(K,K1).
kind(KC,F $ G, K2) :- kind(KC,F,K1 -> K2), kind(KC,G,K1).
kind(KC,A -> B,o)  :- kind(KC,A,o), kind(KC,B,o).

type(KC,C,var(X),     T1) --> { first(X:T,C) }, inst_type(KC,T,T1).
type(KC,C,lam(X,E), A->B) --> type(KC,[X:mono(A)|C],E,B), [kind(KC,A->B,o)].
type(KC,C,X $ Y,       B) --> type(KC,C,X,A->B), type(KC,C,Y,A).
type(KC,C,let(X=E0,E1),T) --> type(KC,C,E0,A), type(KC,[X:poly(C,A)|C],E1,T).

first(X:T,[X1:T1|Zs]) :- X = X1, T = T1.
first(X:T,[X1:T1|Zs]) :- X\==X1, first(X:T, Zs).

instantiate(poly(C,T),T1) :- copy_term(t(C,T),t(C,T1)).
instantiate(mono(T),T).

inst_type(KC,poly(C,T),T2) --> { copy_term(t(C,T),t(C,T1)) }, 
  { free_variables(T,Xs), free_variables(T1,Xs1) }, % Xs, Xs1 same length
  samekinds(KC,Xs,Xs1), { T1=T2 }. % unify T1 T2 later (T2 may not be var)
inst_type(KC,mono(T),T) --> [].

samekinds(KC,[X|Xs],[Y|Ys]) --> { X\==Y }, [kind(KC,X,K),kind(KC,Y,K)],
                                samekinds(KC,Xs,Ys).
samekinds(KC,[X|Xs],[X|Ys]) --> [], samekinds(KC,Xs,Ys).
samekinds(KC,[],    []    ) --> [].

variablize(var(X)) :- gensym(t,X).

infer_type(KC,C,E,T) :-
  phrase( type(KC,C,E,T), Gs0 ), % 1st stage of typing in this line
  copy_term(Gs0,Gs),             % 2nd stage of kinding from here
  bagof(Ty, member(kind(_,Ty,_),Gs), Tys),
  free_variables(Tys,Xs), % collect all free tyvars in Xs
  maplist(variablize,Xs), % concretize tyvar with var(t) where t fresh
  bagof(A:K, member(var(A),Xs), KC1), % kind bindngs for var(t)
  appendKC(Gs,KC1,Gs1), % extend each KC with KC1 for new vars
  maplist(call,Gs1).    % run all goals in Gs1

appendKC([],_,[]).
appendKC([kind(KC,X,K)|Gs],KC1,[kind(KC2,X,K)|Gs1]) :-
  append(KC1,KC,KC2), appendKC(Gs,KC1,Gs1).
\end{verbatim}
\caption{HM + type constructor polymorphism + kind polymorphism in Prolog
        $\qquad$
        (without pattern matching).}
\label{fig:HMtck}
\end{figure}

The second step is to invoke well-kindedness checks from the necessary
places among the typing rules. We follow the formulation of Pure Type
Systems \cite{Barendregt91}, a generic theory of typed lambda calculi,
which indicates that well-kindedness checks are required at the
formation of function types, that is, in the typing rule for lambda
expressions. One would naturally attempt the following modification:%
{\small\vspace*{-1ex}
\begin{verbatim}
  type(KC,C,lam(X,E),A->B) :- type(KC,C,[X:mono(A)|C],E,B),
                              kind(KC,A->B,o).
\end{verbatim} \vspace*{-.7ex} }\noindent
This second step modification is intuitive as a specification, but
rather fragile as a reference implementation. For instance,
a simple type inference query for the identity function fails
(where the HM specification successfully infers \verb|T = A -> A|):{\small \vspace*{-1ex}
\begin{verbatim}
  ?- type([],[],lam(x,var(x)),T).
  ERROR: Out of local stack
\end{verbatim} \vspace*{-.7ex} }

There are mainly two reasons for the erratic behavior.
Firstly, there is not enough information at the moment of
well-kindedness checking. At the invocation of \verb|kind|,
the only available information is that it is a function type \verb|A -> B|.
Whether \verb|A| and \verb|B| are variables, type constructor applications,
or function types may be determined later on, when there are other parts
of the expression to be type checked (or inferred). Secondly, we have
a conflicting view on type variables at the typing level and
at the kinding level. At the typing level, we think of type variables as
unification variables, implemented by Prolog variables in order to exploit
the unification natively supported in Prolog. At the kinding level,
on the contrary, we think of type variables as concrete names that
can be looked up in the kinding context (just like term variables
in the typing context).

The last step of the modification addresses the erratic behavior of
the second step. A solution for these two problems mentioned above is
to stage the control flow: first, get as much information as possible
at the typing level, and then, concretize Prolog variables with atomic names
for the rest of the work at the kinding level. Instead of directly invoking
\verb|kind| within \verb|type|, we collect the list of all the necessary
well-kindedness assertions into a list to be handled later.
This programming technique is known as \emph{delayed goals}
in logic programming, which is like building up a to-do list or continuation.
We use the Definite Clause Grammar (DCG) rules \cite{PerWar80,SWIPrologManual}
to collect delayed goals using a neat syntax. The DCG rules were originally
designed for describing production rules of formal grammar, where nonterminals
are specified within the brackets and context-sensitive conditions are
specified within curly braces using ordinary Prolog predicates. Here,
we exploit DCG rules (as many others do) as a neat syntax for
a \emph{writer monad} that collects \texttt{kind} assertions
as a side-output within the brackets (e.g., \verb|[kind(KC,A->B,o)]|) and pure
computations appear in curly braces (e.g., \verb|{ first(X:T,C) }|).
%% \footnote{
%%   For those not familiar with DCG rules and writer monads,
%%   specifications without using DCG are also available on the online repository
%%   (see \S\ref{sec:intro}, p.~\pageref{githubURL}). }
The \verb|infer_type| predicate implements the two-staged solution
as follows:\vspace{-.5ex}
\begin{itemize}
\item[1.]
The 1st line is the first stage at the typing level.
For example, {\small \vspace*{-1.1ex}
\begin{verbatim}
  ?- phrase( type([],[],lam(x,var(x)),T), Gs0 ).
  T = (_G1643->_G1643),
  Gs0 = [kind([], (_G1643->_G1643), o)] .
\end{verbatim} \vspace*{-1.1ex} }
it infers the most generic type ({\small\verb|_G1643->_G1643|})
of the identity function and generates one delayed goal, namely
{\;\small\verb|kind([], (_G1643->_G1643), o)|}.
\item[2.]
%% From the 2nd line,
%% we invoke this delayed goal after preprocessing of concretizing
%% the type variables.
In the 2nd line, we make a copied version of
the delayed goals using {\small\verb|copy_term|} in order to decouple
the variables of the first stage from the variables of the second stage.
After the 2nd line, {\small\verb|Gs|} contains a copied version of
{\small\verb|Gs0|} with freshly renamed variables, say
{\small\verb|Gs = [kind([], (_G2211->_G2211), o)]|}.
\item[3,4.]
The 3rd and 4th lines collects all the type variables
in {\small\verb|Gs|} into {\small\verb|Xs|}, that is,
{\small\verb|Xs=[_G2211]|}, continuing with the identity function example.
\item[5.]
The 5th line {\small\verb|maplist(variablize,Xs)|} instantiates
the Prolog variables collected in {\small\verb|Xs|} into concrete
type variables with fresh names. In {\small\verb|variablize|},
{\small\verb|gensym(t,X)|} generates atoms with fresh names that start with
{\small\verb|t|}. For instance, {\small\verb|X=t1|}, {\small\verb|X=t2|},
$\cdots$. After the 5th line, where it is concretized as
{\small\verb|_G2211=var(t1)|}, we have {\small\verb|Xs = [var(t1)]|} and
{\small\verb|Gs = [kind([], (var(t1)->var(t1)), o)]|}.
\item[6,7.] Freshly generated type variables need to be
registered to the kinding context in order to be well-kinded.
The 6th line monomorphically binds 
all the variable names in {\small\verb|Xs|} and collects them
into {\small\verb|KC1|}. Continuing with the identity function example,
{\small\verb|KC1=[t1:mono(K1)]|} after the 6th line. The 7th line
extends each kinding context in {\small\verb|Gs|} with {\small\verb|KC1|}
for the freshly generated variables. The goals with extended contexts are
collected in {\small\verb|Gs1|}. After 7th line, we have 
{\small\verb|Gs1 = [kind([t1:mono(K1)], (var(t1)->var(t1)), o)]|}.
\item[8.] Finally, the delayed well-kindedness assertions in {\small\verb|Gs1|}
  are called on as goals, which amounts to the following query
  for our identity function example:{\small \vspace*{-1ex}
\begin{verbatim}
  ?- kind([t1:mono(K1)], (var(t1)->var(t1)), o).
  K1 = o
\end{verbatim} \vspace*{-.7ex} }%
% It succeeds by inferring that the fresh variable 
% \verb|var(t1)| must have kind \verb|o|.
\vspace*{-1.5ex}
\end{itemize}

\section{Supporting Other Language Features}\label{sec:other}
The purpose of this section is to demonstrate that our Prolog specification
for polymorphic features is extensible for supporting other orthogonal
features in functional languages including general recursion
(\S\ref{ssec:letrec}), pattern matching over algebraic datatypes
(\S\ref{ssec:patlam}), and recursion schemes over non-regular
algebraic datatypes with user provided annotations (\S\ref{ssec:mit}).
The specification for the pattern-matching and the recursion schemes
in this section are extensions that build upon the specification
in \S\ref{ssec:HMtck}.

Discussions on the details of the Prolog code is kept relatively brief,
compared to the previous section, because our main purpose here is to
demonstrate that supporting these features does not significantly increase
the size and the complexity of our specification. Readers with further
interest are encouraged to experiment with our specifications available
online (see \S\ref{sec:intro}, p.~\pageref{githubURL}).

\subsection{Recursive Let-Bindings}\label{ssec:letrec}
Adding recursive \texttt{let}-bindings is obvious. We simply add
a monomorphic binding for the \texttt{let}-bound variable (\verb|X|)
when inferring the type of the expression (\verb|E0|) defining
the \texttt{let}-bound value as follows:
{\small \vspace*{-1ex}
\begin{verbatim}
  type(KC,C,letrec(X=E0,E1),T) --> type(KC,[X:mono(A)  |C],E0,A),
                                   type(KC,[X:poly(C,A)|C],E1,T).
\end{verbatim} \vspace*{-.7ex} }

We could also allow polymorphic recursion by type annotations
on the \texttt{let}-bound variable, like we will do for Mendler-style iteration
over non-regular datatypes in \S\ref{ssec:mit}.

\begin{figure} %%%% 14 lines
\begin{verbatim}
type(KC,C,Alts,A->T) --> type_alts(KC,C,Alts,A->T), [kind(KC,A->T,o)].

type_alts(KC,C,[Alt],          A->T) --> type_alt(KC,C,Alt,A->T).
type_alts(KC,C,[Alt,Alt2|Alts],A->T) --> type_alt(KC,C,Alt,A->T),
                                         type_alts(KC,C,[Alt2|Alts],A->T).

type_alt(KC,C,P->E,A->T) --> % assume single depth pattern (C x0 .. xn)
  { P =.. [Ctor|Xs], upper_atom(Ctor), % when P='Cons'(x,xs) then Xs=[x,xs]
    findall(var(X),member(X,Xs),Vs),   %    Vs = [var(x),var(xs)]  
    foldl_ap(var(Ctor),Vs,PE),         %    PE=var('Cons')$var(x)$var(xs)
    findall(X:mono(Tx),member(X,Xs),C1,C) }, % extend C with bindings for Xs
  type(KC,C1,PE,A), type(KC,C1,E,T).

upper_atom(A) :- atom(A), atom_chars(A,[C|_]), char_type(C,upper).

% foldl_ap(E, [E1,...,En], E$E1$...$En).
foldl_ap(E, []     , E).
foldl_ap(E0,[E1|Es], E) :- foldl_ap(E0$E1, Es, E).
\end{verbatim}
\vspace*{-2ex}
\caption{A Prolog specification of non-nested pattern-matching lambdas
$\qquad$ (coverage checking not included).}
\label{fig:patlam}
\end{figure}
\begin{figure} % 17 lines
\begin{verbatim}
kind(KC,mu(F), K)  :- kind(KC,F, K -> K).

type(KC,C,in(N,E), T) --> type(KC,C,E,T0),
                          { unfold_N_ap(1+N,T0,F,[mu(F)|Is]),
                            foldl_ap(mu(F),Is,T) }.

type(KC,C,mit(X,Alts),mu(F)->T) -->
  { is_list(Alts), gensym(r,R),
    KC1 = [R:mono(o)|KC], C1 = [X:poly(C,var(R)->T)|C] },
  type_alts(KC1,C1,Alts,F$var(R)->T).

type(KC,C,mit(X,Is-->T0,Alts),A->T) -->
  { is_list(Alts), gensym(r,R),
    foldl_ap(mu(F),Is,A), foldl_ap(var(R),Is,RIs),
    KC1 = [R:mono(K)|KC], C1 = [X:poly(C,RIs->T0)|C] },
  [kind(KC,F,K->K), kind(KC,A->T,o)], % delayed goals
  { foldl_ap(F,[var(R)|Is],FRIs) },
  type_alts(KC1,C1,Alts,FRIs->T).

% unfold_N_ap(N, E$E_1$...$E_N, E, [E_1,...,E_N]).
unfold_N_ap(0,E,    E,[]).
unfold_N_ap(N,E0$E1,E,Es) :- N>0, M is N-1,
                             unfold_N_ap(M,E0,E,Es0), append(Es0,[E1],Es).
\end{verbatim}
\vspace*{-1ex}
\caption{A Prolog specification for Mendler-style iteration
  on algebraic datatypes (including non-regular nested datatypes).}
\label{fig:mit}
\end{figure}



\subsection{Pattern Matching for Algebraic Datatypes}\label{ssec:patlam}
In Fig.~\ref{fig:patlam} (on p.~\pageref{fig:patlam}), we specify
pattern matching expressions without the scrutinee, which is
also known as pattern-matching lambdas. A pattern lambda is
a function that awaits an expression to be passed in
as an argument to pattern match its value. For example,
let $\{p_1\to e_1;\cdots; p_n\to e_n\}$ be a pattern-matching lambda.
Then, the application $\,\{p_1\to e_1;\cdots; p_n\to e_n\}\,e\,$
corresponds to a pattern matching expressions in Haskell of the form
${\bf\;case}\;e\;{\bf of}\;\{p_1\to e_1;\cdots; p_n\to e_n\}$.

We represent pattern-matching lambdas in Prolog as a list of clauses
that match each pattern to a body, for instance,
\verb|['Nil'-->E1, 'Cons'(x,xs)-->E2]|
where \verb|E1| and \verb|E2| are expressions of the bodies. For simplicity,
we implement the most simple design of non-nested patterns. That is,
a pattern is either an atom that represents a nullary data constructor,
such as \verb|'Nil'|, or a complex term with an $n$-ary function symbol
that represents an $n$-ary data constructor and $n$ variables as its arguments,
such as \verb|'Cons'(x,xs)|.
%% Atoms and function symbols normally start with lowercase letters in Prolog.
%% However, Prolog allows other names to become atoms and function symbols
%% when those names are single-quoted.
Here, we are using the convention that names of type constructors and
data constructors start with uppercase letters while names of term variables
(including pattern variables) start with lowercase letters. We also add
a delayed well-kindedness goal because pattern lambdas introduce function types
(\verb|A -> T|), just like ordinary lambda expressions.

%% kThe specification above for non-nested pattern-matching lambdas
%% kis only 14 lines. To sum up, the specification for HM extended
%% kwith type constructor polymorphism, kind polymorphism, and
%% knon-nested pattern matching for algebraic datatypes is in $32+14=46$
%% klines of Prolog, which is also an executable reference implementation
%% kof the type system.


\subsection{Recursion Schemes for Non-Regular Algebraic Datatypes}
\label{ssec:mit}
Consider the following two recursive datatype declarations in Haskell:
\begin{align*}
& \textbf{data}~\textit{List}~\,a~
      \,=\, N_{\!L}
       ~|~  C_{\!L}~a~(\textit{List}~a)\\
& \textbf{data}~\textit{Bush}~a
      \,=\, N_{\!B}
       ~|~  C_{\!B}~a~(\textit{Bush}\;(\textit{Bush}~a))
\end{align*}
\textit{List} is a homogeneous list, which is either empty
or an element tailed by a \textit{List} that contains (zero or more)
elements of \emph{the same type as the prior element}.
\textit{Bush} is a list-like structure that is either empty
or has an element tailed by a \textit{Bush} that contains (zero or more) 
elements \emph{but their type $(\textit{Bush}~a)$ is different from 
the type of the prior element $(a)$}.
%% The recursive component (\textit{List a} in $C_{\!L}~a~(\textit{List}~a)$),
%% which is the tail of a list, has exactly the same type argument ($a$) as
%% the datatype being defined
%% (\textit{List a} in $\textbf{data}~\textit{List}~a = \ldots$).

Every recursive component of \textit{List}, which is the tail of a list,
has exactly the same type argument ($a$) as the \textit{List} containing
the tail. Because the types of recursive occurrences in \textit{List} are
always the same, or \emph{regular}, and \textit{List} is therefore categorized
as a \emph{regular datatype}. The recursive component of \textit{Bush},
on the contrary, has a type argument (\textit{Bush a}) different from
the type argument ($a$) of its containing \textit{Bush}. Due to this
non-regularity of the types in its recursive occurrences, \emph{Bush} is
categorized as a \emph{non-regular datatype}, which is also known as
a \emph{nested datatype}\;\cite{BirMee98} because the types of recursive
components typically become nested as the recursion goes deeper.
% (e.g., $\textit{Bush}(\textit{Bush}(\cdots(Bush(\textit{Bush}~a))\cdots))$).

In order to define interesting and useful recursive functions over
non-regular datatypes, one needs polymorphic recursion, whose 
type inference is known to be undecidable without the aid of
user supplied type annotations. In Fig.~\ref{fig:mit} (on p\pageref{fig:mit}),
we specify a subset of a functional language that supports a recursion scheme,
which naturally generalizes from regular datatypes to non-regular datatypes.
In particular, we specify
the Mendler-style iteration \cite{matthes98phd,AbeMatUus03}
supported in the Nax language \cite{Ahn14thesis}. In Nax,
all recursive constructs, both at the type level and at the term level,
are defined using the primitives provided by the language, avoiding
uncontrolled general recursion.

%% \begin{figure}
%% \[ (\mu)\frac{\Delta \vdash F : \kappa \to \kappa}{
%%               \Delta : \mu_\kappa F : \kappa} \]
%% 
%% \[ (\textbf{in})
%%     \frac{ \Delta;\Gamma \vdash e :  F(\mu_\kappa F)\,\overline{A}
%%            \qquad \Delta \vdash F : \kappa \to \kappa
%%            \qquad \Delta \vdash \mu_\kappa F\, \overline{A} : *}{
%%            \Delta;\Gamma \vdash
%%            \textbf{in}_\kappa\,e  : \mu_\kappa F \, \overline{A} }
%% \]
%% \[ (\textbf{mit})
%%    \frac{\Delta;\Gamma \vdash }{
%%      \Delta;\Gamma \vdash \textbf{mit}_\kappa : \}
%% \]
%% \caption{A kinding rule ($\mu$) and typing rules of Mendler-style iteration}
%% \label{fig:mitrule}
%% \end{figure}


\begin{figure}\small
\begin{verbatim}
getKC0([ 'N':mono(o->o)            % Nat    = mu(var('N'))
       , 'L':mono(o->o->o)         % List A = mu(var('L')$A)
       , 'B':mono((o->o)->(o->o))  % Bush A = mu(var('B'))$A
       ]).

getC0(% Ctors of N
      [ 'Z':poly([] , N$R1)
      , 'S':poly([] , R1 -> N$R1)
      % Ctors of L
      , 'N':poly([] , L$A2$R2)
      , 'C':poly([] , A2-> R2-> L$A2$R2)
      % Ctors of B
      , 'BN':poly([] , B$R3$A3)
      , 'BC':poly([] , A3 -> R3$(R3$A3) -> B$R3$A3)
      % used in bsum example
      , 'plus':poly([], mu(N) -> mu(N) -> mu(N))
      ])
  :- N = var('N'), L = var('L'), B = var('B').

infer_len :- % length of List
  TM_len = mit(len,['N'      ->Zero,
                    'C'(x,xs)->Succ$(var(len)$var(xs))]),
  Zero = in(0,var('Z')),
  Succ = lam(x,in(0,var('S')$var(x))),
  getKC0(KCtx), getC0(Ctx),
  infer_type(KCtx,Ctx,TM_len,T), writeln(T).

%%%% ?- infer_len. % corresponds to "List a -> Nat"
%%%% mu(var(L)$_G1854)->mu(var(N))
%%%% true .

infer_bsum :- % sum of all elements in Bush of natural numbers
  TM_bsum = mit(bsum, [I]-->((I->mu(var('N')))->mu(var('N'))),
            [ 'BN'       -> lam(f,Zero)
            , 'BC'(x,xs) -> lam(f, % f : I -> Nat
                  var(plus) % f x + bsum xs (\ys -> bsum ys f)
                     $ (var(f)$var(x)) % calculate Nat value from x
                     $ (var(bsum) $ var(xs)  % recursive call on xs
                                  $ lam(ys,var(bsum)$var(ys)$var(f))))
            ]),
  Zero = in(0,var('Z')),
  getKC0(KCtx), getC0(Ctx),
  infer_type(KCtx,Ctx,TM_bsum,T), writeln(T).

%%%% ?- infer_bsum. % corresponds to "Bush i -> (i -> Nat) -> Nat"
%%%% mu(var(B))$_G1452-> (_G1452->mu(var(N)))->mu(var(N))
%%%% true .
\end{verbatim}
\caption{Example queries of type inference: List length and Bush sum.}
\label{fig:TIexample}
\end{figure}
%% \TODO{Add explanation using Bush example, how the variables including
%%   \texttt{Is} and \texttt{T0} in \texttt{Is-->T0} as discussed in conversation
%%   with Patricia.}

The {\small\verb|mu(F)|} appearing in the Prolog specification corresponds to
a recursive type $\mu F$ constructed by the fixpoint type operator $\mu$
applied to a base structure $F$, which is not recursive by itself. Here,
we require that $F$ is either a type constructor introduced by a (non-recursive)
datatype declaration or a partial application of such a type constructor.
We add a kinding rule for the fixpoint type operator by adding another rule of
the {\small\verb|kind|} predicate for {\small\verb|mu(F)|}. We also add two
accompanying rules for recursive values. The expression {\small\verb|in(N,E)|}
constructs a recursive value of type {\small\verb|mu(F)$I_0$...$I_N|}.
In case of regular datatypes, where \verb|mu(F)| does not require additional
type arguments (i.e., {\small\verb|mu(F):o|}), {\small\verb|N|} is \verb|0|.
The Mendler-style iteration expressions define (terminating) recursive
computation over recursive values. There are two rules for Mendler-style
iteration -- one for regular datatypes and the other for non-regular datatypes.

The Mendler-style iteration over regular datatypes (\verb|mit(X,Alts)|)
does not need any type annotation. The Mendler-style iteration over
non-regular datatypes (\verb|mit(X,Is-->T0,Alts)|) needs an annotation
(\verb|Is-->T0|) to guide the type inference because it is likely to rely on
polymorphic recursion. We require that \texttt{Is} must be list of variables.
For instance, \verb|mit(X,[I1,I2,I3]-->T0,Alts)| has type
\verb|(mu(F)$I1$I2$I3)->T0| for some \verb|F|. The specification for
Mendler-style iteration relies on pattern-matching lambdas discussed in
the previous subsection. Once we have properly set up the kinding context
and typing context for the name of the recursive call (\verb|X|), the rest
amounts to inferring types for pattern-matching lambdas. Pointers to further
details on Mendler-style recursion \cite{vene00phd,AbeMatUus03,AhnShe11} and
Nax \cite{Ahn14thesis} are available in the references section at the end of
this article. Here, in Fig.~\ref{fig:TIexample}, we provide type inference
queries on some example programs using Mendler-style iteration.



%% The specification for Mendler-style iteration in Fig.~\ref{fig:mit}
%% is only 18 lines, including pattern-matching lambdas $14+18=32$ lines,
%% including HM with type constructor polymorphism and kind polymorphism
%% the total is $32+14+18=64$ lines of Prolog (excluding empty lines).
% The complete specification, and also a reference implementation, of
% all the features discussed so far fits in only 64 lines of Prolog.

A missing part from a typical functional language's type system, which
we have not discussed in this paper, is the initial phase of populating
the kinding context and typing context from the list of algebraic datatype
declarations prior to type checking the expressions using them.
With fully functioning basic building blocks for kind inference
(\verb|kind|) and type inference (\verb|type|), inferring kinds of
type constructor names and inferring types for their associated
data constructors should be straightforward.


\section{Future Work}\label{sec:futwork}
We plan to continue our work on several additional features, including
generalized algebraic datatypes (GADTs) and real term-indices
in GADTs (as in Nax).

GADTs add the complexity of introducing local constraints
within a pattern-matching clause, which should not escape
the scope of the clause, unlike global unification constraints in HM.
It would be interesting to see whether Prolog's built-in support for
handling unification variables and symbols could help us express
the concept of local constraints as elegantly as we expressed
polymorphic instantiation in \S\ref{sec:poly}.
%% In addition, more user supplied annotations will be needed,
%% even when recursion is not involved, because GADT type inference is
%% undecidable \cite{DegtyarevV95} regardless of recursion.
%% In Nax, pattern-matching lambdas can have annotations,
%% just like the annotations on the Mender-style iteration in \S\ref{ssec:mit}.
%% to aid type inference.

The kind structure needed for type constructor polymorphism is exactly
the kinds supported in the higher-order polymorphic lambda calculus,
known as System \Fw\ \cite{girard72thesis}.
Type constructors in \Fw\ can have types as arguments.
For example, the type constructor \textit{List}
for lists has kind $* \to *$, which means that it needs one type argument
to be fully applied as a type (e.g. $\textit{List}\,~\texttt{Nat} : *$).
\begin{align*}
  &\text{kind in System \Fw}  &&\kappa ::= * \mid \kappa \to \kappa \\
  &\text{kind in System \Fi}  &&\kappa ::= * \mid \kappa \to \kappa
                                             \mid \{A\,\}\to \kappa
\end{align*}
To support terms, as well as types, to be supplied to type constructors
as arguments, the kind structure needs to be extended.
System~\Fi\ \cite{AhnSheFioPit13}, which Nax is based on, extends
the kind structure with $\{A\,\}\to \kappa$ to support term indices in types.
This extension allows type constructors 
such as $\textit{Vec} : * \to \{\textit{Nat}\,\} \to *$ for vectors
(a.k.a. length indexed lists). For instance,
$\textit{Vec}~\textit{Bool}~\{8\}$ is a type of boolean vectors of length 8.
There are two ramifications regarding type inference:
% being involved in type inference:
\begin{itemize}\vspace*{-.75ex}
\item the unification is modulo equivalence of terms: For instance,
  the type system should consider $\textit{Vec}~\textit{Bool}~\{n\}$ and
  $\textit{Vec}~\textit{Bool}~\{(\lambda x.x)\;n\}$ as equivalent types.
  \vspace*{.5ex}
\item Type inference/checking and kind inference/checking invoke each other:
  A typing rule has to invoke a kinding rule to support
  type constructor polymorphism  (\S\ref{ssec:HMtck}).
  In the extended kind structure, types can appear in kinds
  ($A$ in $\{\!A\}\to\kappa$) and therefore kinding rules
  need to invoke typing rules.
\end{itemize}
Extending our specification with term indices would be
an interesting future work that might involve resolving possible challenges
from these two ramifications.

In addition, we are planning to develop specifications for more practical
language constructs such as records with named fields and modules for
organizing definitions in different namespaces. To support high degree of
polymorphism with records and modules, we will also need to support
\emph{row polymorphism} \cite{Gaster96apolymorphic} and
\emph{first-class polymorphism} (e.g., \cite{QML09}).

%%%%%% \section{Related Work}\label{sec:relwork} %%%%%%%%%%%%%%%%%%%%%%%%%%
\input{relwork}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{Conclusions}\label{sec:concl}\vspace*{-.5ex}
During this work, we searched for relational specifications of type systems
that are executable in logic programming systems, only to find out that there
are surprisingly few (\S\ref{ssec:otherLP}); we found a few for HM but were not
able to find specifications for more sophisticated polymorphisms.
Our work is a pioneering case study on this subject matter,
demonstrating the possibility of relational specification for advanced
polymorphic features, highlighting the benefits of relational specifications,
and identifying limitations of the LP systems presently available.

There are novel features and designs scattered around in different
theories/systems that could be useful for relational specifications of
type systems, as discussed in \S\ref{sec:relwork} (e.g.,
nominal logic in LP, embedded DSLs for LP, abstractions
for control flow in LP, alternative resolution semantics). We believe
that there should be a tool that makes it easy to develop relational
specifications of type systems. Such a tool can open a new era
in language construction, analogous to the impact when parser generators
such as Yacc were first introduced. But to realize such a tool for applications
pedagogical examples, we need a combined effort of
both functional and logic programing communities to seamlessly put together
such novel ideas accomplished individually in different settings into
the context of ``\emph{relational specifications of polymorphic type systems}''.

% We defined in Prolog a type inference implementation for a non-trivial
% type system by making extensive use of Prolog's native support for
% unification, allowing us to obtain a concise and runnable specification.
% In particular we use logical variables to represent type (or kind) variables
% in type (or kind) schemas.
% 
% We overcame the conflicting view of type variables between type- and
% kind-checking by delaying kind-checking constraints until after
% type checking is completed and type variables can be made ground and so
% can be used as indexes into the kinding context. We believe this could
% have been simplified if there was either a language level support or
% well tailored framework for establishing a dual-view on the variables
% in logic programming.
% 
% We also showed the flexibility of this technique by successively
% extending the language with more advanced language features like
% recursive let, pattern matching and Mendler-style iteration.
% 
% The use of extra-logical built-ins like \verb|copy_term/2| makes so we
% can exploit Prolog's logical variables not only for unification but
% also to represent binding of quantified type (or kind) variables,
% greatly simplifying the handling of implicit polymorphism.
% 
% Logical variables can however also limit the predictability of how the
% program is going to behave, since a predicate running on inputs that
% are not grounded enough can get stuck.

% TODO
% TODO We have deomstrated our approach is useful as a pedagogical tool for
% TODO specifying the essense of advanced polymorphic features of found in
% TODO modern functional languages. TODO We hope to push forward to develop
% TODO our approach into a practical tool. TODO many languages didn't have
% TODO static
% TODO types now wants to support static types (at least optionally)
% TODO Typed Lua, Typed Clojure, Mypy, Flow, TypeScript
% TODO Mention typer project
% TODO 
%

\subsubsection*{Acknowledgements.}
Thanks to Patricia Johann for helping us clarify the specification
for Mendler-style iteration, Ekaterina Komendantskaya and
Frantisek Farka for the discussions on S-Resolution,
Peng Fu for pointers to Kanren, Chris Warburton for careful proofreading,
and FLOPS'16 reviewers for their feedback.
\makeatletter
\renewcommand\bibsection{\section*\bibname}
\makeatother
\bibliographystyle{abbrvnat}
\bibliography{main}

%% \newpage
%% \section*{Appendix: TODO}
\end{document}