-
Notifications
You must be signed in to change notification settings - Fork 0
/
relwork.tex
126 lines (117 loc) · 7.6 KB
/
relwork.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
\section{Related Work}\label{sec:relwork}
\subsection{\HMX, CHR, and Typol}
The idea of using logic programming (LP) to specify type systems is not new,
for instance, Typol \cite{Despeyroux84} and \HMX\ \cite{HMX99}.
Typol is a specification language for both static semantics (i.e. type systems)
and dynamic semantics of programming languages, where type checkers and
interpreters could be generated directly from Typol specifications
by compiling the specification into Prolog code. Although \citet{Despeyroux84}
demonstrated that Typol can be used for type system based on HM (more
specifically, the core of ML), it was mainly used for language specifications
without parametric polymorphism --- in the 80's, there were not as much
practical programming languages supporting parametric polymorphism as
in the 21st century.
In the late 90's, \citet*{HMX99} defined a general framework called \HMX\ for
specifying extensions of HM (e.g., records, type classes, intersection types)
and \citet{tyinferCHR02} implemented \HMX\ using Constraint Handling Rules (CHR)
in Prolog. Testing a type system extension in the \HMX\ framework provides
a certain level of confidence that the extension would work well with
type polymorphism in HM. Testing an extension by extending our specification
provides additional confidence that the extension would work well with
type constructor polymorphism and kind polymorphism, as well as
with type polymorphism.
CHR have been used for type inference in many other occasions. For instance,
\citet{CsorbaCHRforTyInf12} discuss ``\emph{Pros and Cons of using CHR for
Type Inference}'' of the Q programming language, which is a functional
language well suited for complex calculations on large volume of data.
Although Q was designed to be strongly typed, prior implementations dynamically
checked those types during runtime execution. They implemented a static type
inference for Q using CHR in Prolog. Interestingly, our work using Prolog for
type inference shares a common \emph{Con} (difficulties they had to overcome
by workaround) in their work using CHR in Prolog for type inference.
One of their difficulties was to ``influence the firing order of rules
with different heads'', which corresponds to our need to process \texttt{kind}
predicates after processing \texttt{type} predicates. Such \emph{Cons} seem
to be common in LP regardless of the use of CHR.
\subsection{Delayed Goals and Control Flow in Logic Programming}
The concept of delayed goals has been used in many different contexts in LP.
An AILog
% \footnote{A logical inference system for designing intelligent agents.}
textbook \cite{AILogTextBook}
introduces delaying goals as one of the useful abilities of a meta-interpreter.
Several Prolog systems including SWI and SICStus provide built-in support for
delaying a goal until certain conditions are met using the predicates
such as {\small\verb|freeze|} or {\small\verb|when|}. In our specification,
%% supporting type constructor polymorphism and kind polymorphism,
we could not simply use {\small\verb|freeze|} or {\small\verb|when|}
because we pre-process the collected delayed goals (see \verb|variablize|
in \S\ref{ssec:HMtck}).
Recently, \citet{SchDemDesWei13} implemented delimited continuations for
Prolog, which might be a useful abstraction for the delayed goals
used in our work.
\subsection{Other Logic Programming Systems}\label{ssec:otherLP}
Some experimental Prolog implementations support interesting features such as
nominal abstraction in \aProlog\ \cite{cheney04iclp} and a (restricted version
of) higher-order unification in \lProlog\ \cite{nadathur99cade}. However, we
have not found a relational specification of a polymorphic type systems using
them. The \aProlog\ developer attempted to implement the HM type inference for
mini-ML in \aProlog, but failed to produce a working version.\footnote{
See \texttt{miniml.apl} in the examples directory of
the \aProlog\ version 0.4 or 0.3.}
The Teyjus \lProlog\ compiler version 2 includes a PCF \cite{Scott69} example,
which is similar to HM but without polymorphic \texttt{let}-bindings.
In both example implementations, they define the type inference predicate
tailored for type inference only (unlike our relational specification that
works for both type checking and inference) and the unification used in
their type inference are manually crafted rather than relying on
the native unification of the LP systems.
Kanren\footnote{ Kanren is a phonetic transcription of the Kanji word
\begin{CJK}{UTF8}{min}{関連}\end{CJK} meaning ``\emph{relation}''.
See \url{http://kanren.sourceforge.net/} } \cite{ReasonedSchemer}
is a declarative LP system embedded in a pure functional subset of Scheme.
A relational implementation of HM is provided in
the Kanren repository,% \footnote{See \url{http://kanren.sourceforge.net/\#Sample}}
which works for both type checking, type inference, and also for
type inhabitance searching, as in our HM specification in Prolog.
A simplified version called miniKanren \cite{minikanrenThesis} has been
implemented in several dialects of Scheme
\footnote{See \url{http://minikanren.org/} }
and an even further simplified kernel \muKanren\ \cite{microKanren}
is being implemented in growing number of host languages as
an embedded Domain Specific Language (eDSL) for LP. By design, Kanren
does not provide concrete syntax, therefore, it is not best suited for
a specification language. However, Kanren has its benefits of being
flexible, simple, and portable. If one is to build a tool based on LP concepts
and wishes to support interfaces to one or more programming languages,
\muKanren\ may be a good choice to target as the backend.
Executable type system specifications in Prolog have been studied for supporting
static types in Prolog itself (e.g., \cite{SchrijversCWD08}). Recently, there
has been research on type inference using LP with non-standard semantics (e.g.,
corecursive, coinductive) for object-oriented languages (e.g., featherweight
Java) but functional languages were left for future work \cite{AL-ECOOP09}.
\citet{SRLP15} have developed S-resolution, which is proven \cite{PCR15} to
produce the same results when the depth-first-search style SLD-resolution
used in Prolog is proven to be inductive. S-resolution can also answer
some queries for which SLD-resolution fails to terminate.
%% S-resolution encompasses both inductive
%% and coinductive reasonings by supporting sound productivity checking criteria
%% for recursively defined predicates.
S-resolution might be useful for us to eliminate the need for delayed goals
in our specification.
\subsection{Descriptions of Type Inference Algorithms in ITPs}
There are several formal descriptions of type inference algorithms using
Interactive Theorem Provers (ITPs) such as Coq \cite{Dubois00} and
Isabelle/HOL \cite{UrbanN2009}. The primary motivation %% NaraschewskiN-JAR,
in such work is to formally prove theoretical properties (e.g., soundness,
principal typing) of type inference algorithms, which is different from
our motivation of providing a human readable and machine executable
specification for the type system to reduce the gap between
theoretical specification and practical implementation. Some of those
descriptions are not even executable because the unification is merely
specified as a set of logical axioms.
Formally describing certifiable type inference in ITPs is challenging
(and therefore also challenging to extend or modify) for two reasons.
First, fresh names should be monitored more explicitly and rigorously for
the sake of formal proof. Second, algorithms may need to be massaged
differently from their usual representations, in order to convince
the termination checker of the ITP (e.g. \cite{JFP:185139}).