-

paper.tex

@@ -9,7 +9,7 @@
 
 \DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}}
 \DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}}
-\DeclareUnicodeCharacter{2980}{\ensuremath{|||}}
+\DeclareUnicodeCharacter{2980}{\ensuremath{\Vvert}}
 \DeclareUnicodeCharacter{2081}{\ensuremath{_1}}
 \DeclareUnicodeCharacter{2082}{\ensuremath{_2}}
 \DeclareUnicodeCharacter{3A9}{\ensuremath{\Omega}}
@@ -174,13 +174,13 @@ where \id{hd} and \id{tl} are field names.  We could have written just
 Functions and data constructors are curried.  You can define the
 traditional \id{map} function as follows:
 \begin{verbatim}
-  map : (a : Type) ≡> (b : Type) ≡>
+  map : (a : Type) ⇛ (b : Type) ⇛
         (a -> b) -> List a -> List b;
   map f xs = case xs
     | nil => nil
     | cons x xs => cons (f x) (map f xs);
 \end{verbatim}
-The type declaration is optional.  The triple arrow $\equiv>$ is used
+The type declaration is optional.  The triple arrow $⇛$ is used
 for functions whose argument is \emph{implicit}, which is actually called
 \emph{erasable} in Typer.
 %% It is the dependent function type, used to give a name to the function
@@ -228,6 +228,8 @@ They're defined simply as values with a dedicated type \id{Macro}:
 where \id{macro} is the constructor of the \id{Macro} type and \id{ifthen}
 is the function which performs the expansion.  Ignoring the types, this is
 very similar to how it is done in Emacs Lisp.
+%% FIXME: Maybe discuss the fact that we receive a *List* of Sexp rather
+%% than a single Sexp as argument?
 The \id{ifthen} function
 could be defined as follows:
 \begin{verbatim}
@@ -282,6 +284,7 @@ analysis in one step, Typer further subdivides the syntactic analysis phase
 into two steps.  The first step does a rudimentary analysis that only
 extracts a generic tree structure, called S-expression.  The shape of
 S-expressions could be described with the datatype shown in
+%% FIXME: Discuss the absence of a "nil" element.
 Figure~\ref{fig:Typer-Sexp}.
 
 Note how, at this stage, the representation of the code has no notion of
@@ -655,6 +658,10 @@ anything left to generalize); if the free meta-variable is used in
 a non-erasable way, we signal an error since generalizing it with an
 erasable abstraction would lead to invalid code.
 
+%% FIXME: Discuss decidability/termination
+%% FIXME: Is it an actual strict superset of HM (I think so, except for
+%% the case of recursion where we currently require a type annotation).
+
 There are two further places where generalization happens: when a $\lambda$
 abstraction is elaborated in a context that expects an erasable function, we
 wrap it into an additional erasable $\lambda$; and when elaborating a \emph{type
@@ -721,6 +728,7 @@ calculus are the following:
         }
   \end{array}
 \end{displaymath}
+%% FIXME: Explain what these S/A/R mean!
 But the typing rule we use is slightly different for erasable functions:
 \begin{displaymath}
   \Infer{\Jtyper {\tau_1} s \\
@@ -1228,14 +1236,16 @@ making it more flexible at the same time.
 While it has not been officially released yet, its code can be found at
 \url{https://gitlab.com/monnier/typer}.
 
+\newenvironment{acks}{\subsection*{Acknowledgments}}{}
 \newcommand \grantsponsor[3] {#2 (#1)}
 \newcommand \grantnum[2] {#2}
-\subsection*{Acknowledgments}
+\begin{acks}
   This work was supported by the \grantsponsor{NSERC}{Natural Sciences and
     Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/} grant
   N$^o$~\grantnum{NSERC}{298311/2012}.  Any opinions, findings, and
   conclusions or recommendations expressed in this material are those of the
   author and do not necessarily reflect the views of the NSERC.
+\end{acks}
 
 \bibliographystyle{alpha}
 %% \bibliography{typer_theory}