@@ -3,7 +3,7 @@
33In this section we discuss a variety of additional features:
44auto implicit and default
55arguments, literate programming, interfacing with external libraries through the
6−foreign function interface, type providers, and the universe hierarchy.
6+foreign function interface, type providers, code generation and the universe hierarchy.
77
88\subsection{Auto implicit arguments}
99
@@ -332,6 +332,139 @@ example in this section was purposefully simple. More complex type provider
332332implementations, including a statically-checked SQLite binding, are available
333333in an external collection.\footnote{\url{https://github.com/david-christiansen/idris-type-providers}}
334334
335+\subsection{JavaScript Target}
336+
337+\Idris{} is capable of producing \emph{JavaScript} code that can be run in a browser
338+as well as in the \emph{NodeJS} environment or alike. One can use the FFI to
339+communicate with the \emph{JavaScript} ecosystem.
340+
341+\subsubsection*{Code Generation}
342+
343+\noindent
344+Code generation is split into two separate targets. To generate code that is
345+tailored for running in the browser issue the following command:
346+
347+\begin{SaveVerbatim}{jscodegen}
348+
349+$ idris --codegen javascript hello.idr -o hello.js
350+
351+\end{SaveVerbatim}
352+\useverb{jscodegen}
353+
354+\noindent
355+The resulting file can be embedded into your HTML just like any other
356+\emph{JavaScript} code.
357+
358+\noindent
359+Generating code for \emph{NodeJS} is slightly different. \Idris{} outputs
360+a \emph{JavaScript} file that can be directly executed via \texttt{node}.
361+
362+\begin{SaveVerbatim}{nodecodegen}
363+
364+$ idris --codegen node hello.idr -o hello
365+$ ./hello
366+Hello world
367+
368+\end{SaveVerbatim}
369+\useverb{nodecodegen}
370+
371+\noindent
372+Take into consideration that the \emph{JavaScript} code generator is using
373+\texttt{console.log} to write text to \texttt{stdout}, this means that it will
374+automatically add a newline to the end of each string. This behavior
375+does not show up in the \emph{NodeJS} code generator.
376+
377+\subsubsection*{Using the FFI}
378+
379+\noindent
380+To write a useful application we need to communicate with the outside
381+world. Maybe we want to manipulate the DOM or send an Ajax request. For this
382+task we can use the FFI. Since most \emph{JavaScript} APIs demand callbacks
383+we need to extend the FFI so we can pass functions as arguments.
384+
385+\noindent
386+The \emph{JavaScript} FFI works a little bit differently than the regular FFI.
387+It uses positional arguments to directly insert our arguments into a piece
388+of \emph{JavaScript} code.
389+
390+\noindent
391+One could use the primitive addition of \emph{JavaScript} like so:
392+
393+\begin{SaveVerbatim}{jsaddition}
394+
395+module Main
396+
397+primPlus : Int -> Int -> IO Int
398+primPlus a b = mkForeign (FFun "%0 + %1" [FInt, FInt] FInt) a b
399+
400+main : IO ()
401+main = do
402+ a <- primPlus 1 1
403+ b <- primPlus 1 2
404+ print (a, b)
405+
406+\end{SaveVerbatim}
407+\useverb{jsaddition}
408+
409+\noindent
410+Notice that the \texttt{\%n} notation qualifies the position of the
411+\texttt{n}-th argument given to our foreign function starting from 0. When
412+you need a percent sign rather than a position simply use \texttt{\%\%}
413+instead.
414+
415+\noindent
416+Passing functions to a foreign function is very similar. Let's assume that
417+we want to call the following function from the \emph{JavaScript} world:
418+
419+\begin{SaveVerbatim}{jstwice}
420+
421+function twice(f, x) {
422+ return f(f(x));
423+}
424+
425+\end{SaveVerbatim}
426+\useverb{jstwice}
427+
428+\noindent
429+We obviously need to pass a function \texttt{f} here (we can infer it from
430+the way we use \texttt{f} in \texttt{twice}, it would be more obvious if
431+\emph{JavaScript} had types).
432+
433+\noindent
434+The \emph{JavaScript} FFI is able to understand functions as arguments when
435+you give it something of type \texttt{FFunction}. The following example code
436+calls \texttt{twice} in \emph{JavaScript} and returns the result to our
437+\Idris{} program:
438+
439+\begin{SaveVerbatim}{jshof}
440+module Main
441+
442+twice : (Int -> Int) -> Int -> IO Int
443+twice f x = mkForeign (
444+ FFun "twice(%0,%1)" [FFunction FInt FInt, FInt] FInt
445+) f x
446+
447+main : IO ()
448+main = do
449+ a <- twice (+1) 1
450+ print a
451+
452+\end{SaveVerbatim}
453+\useverb{jshof}
454+
455+\noindent
456+The program outputs \texttt{3}, just like we expected.
457+
458+\subsubsection*{Shrinking down generated \emph{JavaScript}}
459+
460+\Idris{} can produce very big chunks of \emph{JavaScript} code. However, the
461+generated code can be minified using the \texttt{closure-compiler} from
462+Google. Any other minifier is also suitable but \texttt{closure-compiler}
463+offers advanced compilation that does some aggressive inlining and code
464+elimination. \Idris{} can take full advantage of this compilation mode and
465+it's highly recommended to use it when shipping a \emph{JavaScript}
466+application written in \Idris{}.
467+
335468\subsection{Cumulativity}
336469
337470Since values can appear in types and \emph{vice versa}, it is natural that types themselves