Stefan pushed to branch report/jfla-2019 at Stefan / Typer

Commits: 1de1c2fd by Stefan Monnier at 2018-10-26T17:50:33Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== 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%7D.

+\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/%7D 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}

View it on GitLab: https://gitlab.com/monnier/typer/commit/1de1c2fd4861265a588d4413351ae1905fdd...