Movatterモバイル変換


[0]ホーム

URL:


Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

Sign up
Appearance settings

Commitf4e4e0c

Browse files
committed
icwe14 wip
1 parentefa6b7b commitf4e4e0c

File tree

5 files changed

+1577
-1
lines changed

5 files changed

+1577
-1
lines changed

‎papers/icwe14/icwe14.pdf‎

296 KB
Binary file not shown.

‎papers/icwe14/icwe14.tex‎

Lines changed: 341 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,341 @@
1+
\documentclass{llncs}
2+
3+
\usepackage[utf8]{inputenc}
4+
\usepackage[unicode=true,hidelinks]{hyperref}
5+
\usepackage{listings}
6+
\usepackage{lmodern}
7+
8+
\lstdefinelanguage{Scala}%
9+
{morekeywords={abstract,%
10+
case,catch,char,class,%
11+
def,else,extends,final,for,%
12+
if,import,implicit,%
13+
match,module,%
14+
new,null,%
15+
object,override,%
16+
package,private,protected,public,%
17+
for,public,return,super,%
18+
this,throw,trait,try,type,%
19+
val,var,%
20+
with,%
21+
yield,%
22+
lazy%
23+
},%
24+
sensitive,%
25+
morecomment=[l]//,%
26+
morecomment=[s]{/*}{*/},%
27+
morestring=[b]",%
28+
morestring=[b]',%
29+
showstringspaces=false%
30+
}[keywords,comments,strings]%
31+
32+
\lstdefinelanguage{JavaScript}%
33+
{morekeywords={for, var, attributes, class, classend, do, else, empty, endif, endwhile, fail, function,
34+
functionend, if, implements, in, inherit, inout, not, of, operations, out, return,
35+
then, types, while, use},%
36+
sensitive,%
37+
morecomment=[l]//,%
38+
morecomment=[s]{/*}{*/},%
39+
morestring=[b]",%
40+
morestring=[b]',%
41+
showstringspaces=false%
42+
}[keywords,comments,strings]%
43+
44+
\lstset{language=Scala,%
45+
% mathescape=false,%
46+
% columns=[c]fixed,%
47+
% aboveskip=\smallskipamount,
48+
% belowskip=\smallskipamount,
49+
% basewidth={0.5em, 0.4em},%
50+
basicstyle=\small\ttfamily,
51+
captionpos=b,
52+
keywordstyle=\bfseries
53+
% xleftmargin=0.5cm
54+
}
55+
56+
\newcommand{\jscode}[1]{\lstinline[language=JavaScript]|#1|}
57+
\newcommand{\scalacode}[1]{\lstinline[language=Scala]|#1|}
58+
%\newcommand{\code}[1]{\texttt{#1}}
59+
60+
\begin{document}
61+
62+
\title{Using Path-Dependent Types to Build Type-Safe JavaScript Foreign Function Interfaces}
63+
64+
\author{Julien Richard-Foy\and Olivier Barais}
65+
66+
\institute{IRISA, Universite de Rennes, France}
67+
68+
%\email{\{first\}.\{last\}@irisa.fr}
69+
70+
\maketitle
71+
72+
\begin{abstract}
73+
74+
\end{abstract}
75+
76+
\section{Introduction}
77+
78+
We recently observed the emergence of several statically typed programming languages compiling to JavaScript (\emph{e.g.} Java/GWT~\cite{Kereki09_GWT}, Dart~\cite{Griffith11_Dart}, TypeScript~\cite{fenton2012typescript}, Kotlin\footnote{\href{http://kotlin.jetbrains.org}{http://kotlin.jetbrains.org}}, Opa\footnote{\href{http://opalang.org}{http://opalang.org}}, SharpKit\footnote{\href{http://sharpkit.net}{http://sharpkit.net}}, Haxe~\cite{Cannasse08_HaXe}, Idris~\cite{Brady13_Idris}, Elm~\cite{czaplicki2012elm}). Developers can use them to write the client-side part of their Web applications, relying on a\emph{foreign function interface} mechanism to call the Web browser native API.
79+
80+
However we observe that, despite these languages are statically typed, their integration of the browser API either is not type safe or gives less expression power to developers. Indeed, integrating an API designed for a dynamically typed language into a statically typed language can be challenging. For instance, the\jscode{createElement} function return type depends on the value of the\jscode{String} parameter it is passed.
81+
82+
This paper reviews some common functions of the browser API, identifies those which are not well encoded in statically typed programming languages and shows new ways to encode them with more type safety while keeping the native API expression power. We find that type parameters are sufficient to achieve this goal and that\emph{path-dependent types} provide an even more convenient encoding for the end developers.
83+
84+
The remainder of the paper is organized as follows. The next section reviews the most common functions of the browser API and how they are integrated in statically typed languages. Section\ref{sec-contribution} shows ways to improve their integration. Section\ref{sec-validation} validates our contribution. Section\ref{sec-related} discusses some related works and section\ref{sec-conclusion} concludes.
85+
86+
\section{Background}
87+
\label{sec-background}
88+
89+
This section reviews the most commonly used browser functions and presents the way they are integrated in GWT, Dart, TypeScript, Kotlin, Opa, SharpKit, Haxe, Idris and Elm.
90+
91+
\subsection{The browser API and its integration in statically typed languages}
92+
93+
The client-side part of the code of a Web application essentially reacts to user events (\emph{e.g.} mouse clicks), triggers actions and updates the document (DOM) according to their effect. Table~\ref{table-dom-api} lists the main functions supported by the Web browsers according to the Mozilla Developer Network\footnote{\href{https://developer.mozilla.org/en-US/docs/DOM/DOM\_Reference/Introduction}{https://developer.mozilla.org/en-US/docs/DOM/DOM\_Reference/Introduction}} (we removed the functions that can trivially be encoded in a static type system).
94+
95+
\begin{table}
96+
\centering
97+
\begin{tabular}{ll}
98+
\hline
99+
Name & Description \\
100+
\hline
101+
\jscode{getElementsByTagName(name)} & Find elements by their tag name \\
102+
\jscode{getElementById(id)} & Find an element by its\jscode{id} attribute \\
103+
\jscode{createElement(name)} & Create an element \\
104+
\jscode{target.addEventListener(name, listener)} & React to events \\
105+
\hline
106+
\end{tabular}
107+
108+
\label{table-dom-api}
109+
\caption{Web browsers main functions}
110+
\end{table}
111+
112+
The main challenge comes from the fact that these functions are polymorphic in their return type or in their parameters.
113+
114+
For instance, functions\jscode{getElementsByTagName(name)},\jscode{getElementById(id)} and\jscode{createElement(name)} can return values of type\jscode{DivElement} or\jscode{InputElement} or any other subtype of\jscode{Element} (their least upper bound). The interface of\jscode{Element} is more general and provides less features than its subtypes, so it is important for the encoding of these functions in a statically typed language to be as precise as possible.
115+
116+
In the case of\jscode{getElementById(id)}, the\jscode{id} parameter gives no clue on the possible type of the searched element so it is hard to infer more precisely the return type of this function. Hence, most implementations define a return type of\jscode{Element}. The drawback of this approach is that developers may get a value with a type weaker than they need and may require to explicitly downcast it, thus loosing type safety.
117+
118+
However, in the case of\jscode{getElementsByTagName(name)} and\jscode{createElement(name)}, there is exactly one possible return type for each value of the\jscode{name} parameter:\emph{e.g.}\jscode{getElementsByTagName('input')} always returns a list of\jscode{InputElement} and\jscode{createElement('div')} always returns a\jscode{DivElement}. This characteristic makes it possible to encode each of these functions by defining as many parameterless functions as there are possible tag names, where each function fixes the initial\jscode{name} parameter to be one of the possible values and exposes the corresponding specialized return type. Listing~\ref{lst-create-element-overload} illustrates such an encoding in the Java language.
119+
120+
\begin{figure}
121+
\begin{lstlisting}[label=lst-create-element-overload,language=Java,caption={Encoding of the \jscode{createElement(name)} function in Java using parameterless functions fixing the initial \jscode{name} parameter value}]
122+
DivElement createDivElement();
123+
InputElement createInputElement();
124+
FormElement createFormElement();
125+
...
126+
\end{lstlisting}
127+
\end{figure}
128+
129+
The case of \jscode{target.addEventListener(name, listener)} is a bit different. The \jscode{name} parameter defines the event to listen to and the \jscode{listener} parameter the function to call back each time such an event occurs. Instead of being polymorphic in its return type, it is polymorphic in its \jscode{listener} parameter. Nevertheless, a similar property as above holds: there is exactly one possible type for the \jscode{listener} parameter for each value of the \jscode{name} parameter. For instance, a listener of \jscode{'click'} events is a function taking a \jscode{MouseEvent} parameter, a listener of \jscode{'keydown'} events is a function taking a \jscode{KeyboardEvent} parameter, and so on. The same pattern as above (defining a set of functions fixing the \jscode{name} parameter value) can be used to encode this function in a statically typed language, but an alternative encoding could be to define one function taking one parameter carrying both the information of the event name and the event listener. Listing~\ref{lst-add-event-listener-one-param} shows such an encoding in Java.
130+
131+
\begin{figure}
132+
\begin{lstlisting}[label=lst-add-event-listener-one-param,language=Java,caption={Encoding of the \jscode{target.addEventListener(name, listener)} function in Java using one paremeter carrying both the information of the event name and the event listener}]
133+
// --- API Definition
134+
interface EventTarget {
135+
void addEventListener(EventListener listener);
136+
}
137+
138+
interface EventListener {}
139+
140+
interface ClickEventListener extends EventListener {
141+
void onClick(ClickEvent event);
142+
}
143+
144+
interface KeyDownEventListener extends EventListener {
145+
void onKeyDown(KeyboardEvent event);
146+
}
147+
148+
// --- Usage
149+
void logClicks(EventTarget target) {
150+
target.addEventListener(new ClickEventListener {
151+
public void onClick(ClickEvent event) {
152+
console.log(event.button);
153+
}
154+
});
155+
}
156+
\end{lstlisting}
157+
\end{figure}
158+
159+
Table~\ref{table-existing-encodings} summarizes, for each statically typed language, which approach is used to encode each function of the browser API.
160+
161+
\begin{table}
162+
\centering
163+
\begin{tabular}{|l|c|c|c|c|}
164+
\hline &\jscode{getElementById} &\jscode{getElementsByTagName} &\jscode{createElement} &\jscode{addEventListener} \\
165+
\hline Java & lub & lub & comb & plop \\
166+
\hline Dart & lub & lub \\
167+
\hline TypeScript \\
168+
\hline Haxe & lub & lub \\
169+
\hline Opa \\
170+
\hline Kotlin & lub & lub \\
171+
\hline SharpKit & lub & lub \\
172+
\hline Idris \\
173+
\hline Elm \\
174+
\hline
175+
\end{tabular}
176+
\label{table-existing-encodings}
177+
\caption{Summary of the encodings used by existing statically typed languages}
178+
\end{table}
179+
180+
\subsection{Limitations of existing encoding approaches}
181+
182+
We distinguished three approaches to integrate the challenging parts of the browser API into statically typed languages. This section compares these approaches in terms of type safety, expression power and convenience to use from the end developer point of view.
183+
184+
The first approach, consisting in using the least upper bound of all the possible types is not type safe because it sometimes requires developers to explicitly downcast values to their expected specialized type.
185+
186+
The second approach, consisting in defining as many functions as there are possible return types of a function, is completely type safe but can lead to combinatorial explosion in some situations. Consider for instance listing~\ref{lst-js-comb} defining a JavaScript function that both creates an element and registers an event listener when a given event occurs on it. Note that the event listener is passed both the event and the element. Encoding such a function in a statically typed language using this approach would require to create one function for each combination of tag name and event name.
187+
188+
\begin{figure}
189+
\begin{lstlisting}[label=lst-js-comb,language=JavaScript]
190+
var createAndListenTo = function (tagName, eventName, listener) {
191+
var element = document.createElement(tagName);
192+
element.addEventListener(eventName, function (event) {
193+
listener(event, element);
194+
});
195+
};
196+
\end{lstlisting}
197+
\end{figure}
198+
199+
The third approach, consisting in combining two parameters into one parameter carrying all the required information, is type safe too, but reduces the expression power because it forbids developers to partially apply the function by supplying only one parameter. Consider for instance listing~\ref{lst-js-react} that defines a function partially applying the\jscode{addEventListener} function\footnote{This pattern is often used by functional reactive programming libraries like Rx.js~\cite{liberty2011reactive}}. Such a function is impossible to encode using this approach, in a statically typed language.
200+
201+
\begin{figure}
202+
\begin{lstlisting}[label=lst-js-react,language=JavaScript]
203+
var observe = function (target, name) {
204+
return function (listener) {
205+
target.addEventListener(name, listener);
206+
}
207+
};
208+
\end{lstlisting}
209+
\end{figure}
210+
211+
In summary, browser API integration by existing statically typed languages compiling to JavaScript is either not type safe or not as modular or expressive as the underlying JavaScript API.
212+
213+
\section{Contribution}
214+
\label{sec-contribution}
215+
216+
In this section we show how we can encode the functions presented previously, in a type safe and convenient way for developers while keeping the same expression power.
217+
218+
We first propose a solution in the Java mainstream language, using\emph{generics}, and show how we can improve it using\emph{path-dependent types}, in Scala.
219+
220+
\subsection{Parametric Polymorphism}
221+
222+
In all the cases where a type\scalacode{T} involved in a function depends on the value of a parameter\scalacode{p} of this function (all the aforementionned functions are in this case, excepted\jscode{getElementById}), we can encode this relationship in the type system using type parameters as follows:
223+
224+
\begin{enumerate}
225+
\item Create a parametrized class\scalacode{P<U>}
226+
\item Set the type of\scalacode{p} to\scalacode{P<U>}
227+
\item Use type\scalacode{U} instead of type\scalacode{T}
228+
\end{enumerate}
229+
230+
Listing~\ref{lst-generics-dom} shows this approach applied to the\jscode{createElement} function: we created a type\scalacode{ElementName<E>}, the\scalacode{name} parameter is not a\scalacode{String} but a\scalacode{ElementName<E>}, and the function returns an\scalacode{E} instead of an\scalacode{Element}. The\scalacode{ElementName<E>} type encodes the relationship between the name of an element and the type of this element. For instance, we created a value\scalacode{Input} of type\scalacode{ElementName<InputElement>}. The last two lines shows how this API is used by end developers: by passing the\scalacode{Input} value as parameter to the function, it fixes the type parameter\scalacode{E} to\scalacode{InputElement} so the returned value has the most possible precise type.
231+
232+
\begin{figure}
233+
\begin{lstlisting}[label=lst-generics-dom,language=java]
234+
// --- API Definition
235+
class ElementName<E> {}
236+
237+
<E> E createElement(ElementName<E> name);
238+
239+
final ElementName<InputElement> Input = new ElementName<InputElement>();
240+
final ElementName<ImageElement> Img = new ElementName<ImageElement>();
241+
242+
// --- Usage
243+
InputElement input = createElement(Input);
244+
ImageElement img = createElement(Img);
245+
\end{lstlisting}
246+
\end{figure}
247+
248+
\scalacode{getElementsByTagName} can be encoded in very similar way, and listing~\ref{lst-generics-events} shows the encoding of the\jscode{addEventListener} function.
249+
250+
\begin{figure}
251+
\begin{lstlisting}[label=lst-generics-events,language=java]
252+
// --- API Definition
253+
class EventName<E> {}
254+
255+
interface EventTarget {
256+
<E> void addEventListener(EventName<E> name, Function<E, Void> callback);
257+
}
258+
259+
final EventName<MouseEvent> Click = new EventName<MouseEvent>();
260+
261+
// --- Usage
262+
ButtonElement btn = createElement(Button);
263+
btn.addEventListener(Click, e -> console.log(e.button))
264+
\end{lstlisting}
265+
\end{figure}
266+
267+
\subsection{Path-Dependent Types}
268+
269+
\begin{figure}
270+
\begin{lstlisting}[label=lst-dt-dom]
271+
trait ElementName {
272+
type Element
273+
}
274+
275+
def createElement(name: ElementName): name.Element = ...
276+
\end{lstlisting}
277+
\end{figure}
278+
279+
280+
\begin{figure}
281+
\begin{lstlisting}[label=lst-dt-events]
282+
trait EventName {
283+
type Data
284+
}
285+
object Click extends EventDef { type Data = MouseEvent }
286+
287+
def on(name: EventName)(handler: Rep[name.Data] => Rep[Unit]): Rep[Unit]
288+
289+
val clicks = on(Click)
290+
clicks(event => println(event.offsetX))
291+
\end{lstlisting}
292+
\end{figure}
293+
294+
\section{Validation}
295+
\label{sec-validation}
296+
297+
We show that our encodings support the challenging functions defined in listings\ref{lst-js-comb} and\ref{lst-js-react}.
298+
299+
Listing\ref{lst-generics-comb} and\ref{lst-generics-react} show how these functions can be implemented. They are basically a direct translation from JavaScript to Java.
300+
301+
\begin{figure}
302+
\begin{lstlisting}[label=lst-generics-comb,language=java]
303+
<A, B> void createAndListenTo(
304+
ElementName<A> tagName,
305+
EventName<B> eventName,
306+
Function2<A, B, Void> listener) {
307+
A element = document.createElement(tagName);
308+
element.addEventListener(eventName, event -> listener.apply(event, element));
309+
}
310+
\end{lstlisting}
311+
\end{figure}
312+
313+
\begin{figure}
314+
\begin{lstlisting}[label=lst-generics-react,language=java]
315+
<A> Function<Function<A, Void>, Void> observe(EventTarget target, EventName<A> name) {
316+
return listener -> {
317+
target.addEventListener(name, listener);
318+
}
319+
}
320+
\end{lstlisting}
321+
\end{figure}
322+
323+
\subsection{Limitations}
324+
325+
We do not help with\jscode{getElementById}.
326+
327+
The name of an element or the name of an event can not anymore be a value resulting of the concatenation of Strings.
328+
329+
\section{Related Works}
330+
\label{sec-related}
331+
332+
Ravi Chugh\emph{et. al.}~\cite{Chugh12_DJS} showed how to make a subset of JavaScript statically typed using a dependent type system. They require complex type annotations to be written by developers.
333+
334+
\section{Conclusion}
335+
\label{sec-conclusion}
336+
337+
\bibliographystyle{plain}
338+
\bibliography{references.bib}
339+
340+
341+
\end{document}

‎papers/icwe14/llncsdoc.sty‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
% This is LLNCSDOC.STY the modification of the
2+
% LLNCS class file for the documentation of
3+
% the class itself.
4+
%
5+
\def\AmS{{\protect\usefont{OMS}{cmsy}{m}{n}%
6+
A\kern-.1667em\lower.5ex\hbox{M}\kern-.125emS}}
7+
\def\AmSTeX{{\protect\AmS-\protect\TeX}}
8+
%
9+
\def\ps@myheadings{\let\@mkboth\@gobbletwo
10+
\def\@oddhead{\hbox{}\hfil\small\rm\rightmark
11+
\qquad\thepage}%
12+
\def\@oddfoot{}\def\@evenhead{\small\rm\thepage\qquad
13+
\leftmark\hfil}%
14+
\def\@evenfoot{}\def\sectionmark##1{}\def\subsectionmark##1{}}
15+
\ps@myheadings
16+
%
17+
\setcounter{tocdepth}{2}
18+
%
19+
\renewcommand{\labelitemi}{--}
20+
\newenvironment{alpherate}%
21+
{\renewcommand{\labelenumi}{\alph{enumi})}\begin{enumerate}}%
22+
{\end{enumerate}\renewcommand{\labelenumi}{enumi}}
23+
%
24+
\def\bibauthoryear{\begingroup
25+
\def\thebibliography##1{\section*{References}%
26+
\small\list{}{\settowidth\labelwidth{}\leftmargin\parindent
27+
\itemindent=-\parindent
28+
\labelsep=\z@
29+
\usecounter{enumi}}%
30+
\def\newblock{\hskip .11em plus .33em minus -.07em}%
31+
\sloppy
32+
\sfcode`\.=1000\relax}%
33+
\def\@cite##1{##1}%
34+
\def\@lbibitem[##1]##2{\item[]\if@filesw
35+
{\def\protect####1{\string ####1\space}\immediate
36+
\write\@auxout{\string\bibcite{##2}{##1}}}\fi\ignorespaces}%
37+
\begin{thebibliography}{}
38+
\bibitem[1982]{clar:eke3} Clarke, F., Ekeland, I.: Nonlinear
39+
oscillations and boundary-value problems for Hamiltonian systems.
40+
Arch. Rat. Mech. Anal. 78, 315--333 (1982)
41+
\end{thebibliography}
42+
\endgroup}

0 commit comments

Comments
 (0)

[8]ページ先頭

©2009-2025 Movatter.jp