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

Commits: 45685bab by Stefan Monnier at 2018-10-26T20:04:54Z -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -180,10 +180,10 @@ traditional \id{map} function as follows: | nil => nil | cons x xs => cons (f x) (map f xs); \end{verbatim} -%% FIXME: It's actually not optional for recursive functions (like map). -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. +The type declaration is generally optional, although we currently require it +for recursive definitions. 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 %% argument, so it can be used in the return type. In type theory this is %% often presented with the notation $\Pi,x!:!t_1 . t_2$, but in the above case it @@ -285,8 +285,11 @@ 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}. +Figure~\ref{fig:Typer-Sexp}. Note that contrary to the Lisp S-expression +syntax, parentheses are only used for grouping purposes, so \texttt{(x)} +will produce the same \id{Sexp} as just \texttt{x}. And we use +\texttt{()} as the printed representation of the zero-length \id{symbol} +(which we call \emph{espilon}).

Note how, at this stage, the representation of the code has no notion of bindings, functions, types, or function calls. It's only in a second step @@ -990,6 +993,8 @@ erasable $k$) and prove its property (again with erasable $K_1$ and $K_2$).

\subsection{Impredicativity rules of Typer}

+%% FIXME: Maybe remove this subsection. + Once we decided to try our luck with this conjecture, it was a small step to add yet more potentially risky features to our calculus. So we currently also allow impredicativity at all universe levels rather than only at the

View it on GitLab: https://gitlab.com/monnier/typer/commit/45685bab7429afa796c08a787af0709444d6...