Stefan pushed to branch report/jfla-2019 at Stefan / Typer
Commits: 1347e7b4 by Stefan Monnier at 2018-10-28T22:53:12Z -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -348,7 +348,22 @@ two precedence levels: one for its left side and another for its right side. Then parsing uses the following rule: when we see ``$\id{kw}_1~e~\id{kw}_2$'', we lookup the right precedence of $\id{kw}_1$ and the left precedence of $\id{kw}_2$, and we then attach $e$ to -whichever is higher. +whichever is higher. If the precedences are equal, then we consider those +two keywords as part of a mixfix. + +For example, given the default grammar, we can define the new form +``$\kw{if}~e_1~\kw{then}~e_2~\kw{else}~e_3$'' by setting the precedences as +follows; +\begin{verbatim} + define-operator "if" () 2; + define-operator "then" 2 1; + define-operator "else" 1 66; +\end{verbatim} +After which such a form gets parsed identically to +``$\id{if_then_else_}~e_1~e_2~e_3$''. Note that the modification of the +grammar is independent from the definition of \id{if_then_else_} as +a macro: the grammar can be changed for infix functions and new macros +can be defined without changing the grammar.
While it enjoys a simple and efficient implementation\footnote{as well as some other interesting properties such as the ability to parse backward.} @@ -394,8 +409,6 @@ to an OPG grammar we disallow these context-dependent parsing rules, such that we do not need to know what is a macro call, let alone figure out what is that macro's definition.
-%% FIXME: Show how to change the precedence table for if/then/else - \section{Elaboration} \label{sec:elaboration}
@@ -655,43 +668,44 @@ specialized (i.e. Typer inserts a type application).
HM performs generalization (i.e.~introduction of implicit (type) abstractions) whenever a value is defined in a let-binding. Typer does the -same with the following differences: if the variable had a type annotation, -we don't perform generalization (instead, the bidirectional type checking -propagates the type information into the function so there shouldn't be -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 - annotation}, all remaining free meta variables are generalized into -erasable arrows. - -We use the ``\texttt{?}'' prefix for user-written meta-variables, so the +same when the variable had a type annotation, but with the following +difference: if a 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. + +For definitions that come with a type annotation, Typer also provides a form +of generalization: first, when elaborating a \emph{type annotation}, all +remaining free meta variables are generalized into erasable arrows, so the user can write: \begin{verbatim} map : (?a -> ?b) -> List ?a -> List ?b; \end{verbatim} +where we use the ``\texttt{?}'' prefix for user-written meta-variables, so +Typer will add \texttt{?a} and \texttt{?b} as two additional erasable +arguments. %% and this will be elaborated to a type equivalent to: %% \begin{verbatim} %% map : (a : Type) ≡> (b : Type) ≡> %% (a -> b) -> List a -> List b; %% \end{verbatim} -and Typer will add \texttt{?a} and \texttt{?b} as two additional erasable -arguments. This reproduces the same behavior as that used in systems such -as Twelf~\cite{Pfenning99}. After that, when we define +This reproduces the same behavior as that used in systems such as +Twelf~\cite{Pfenning99}. + +Second, when a $\lambda$ abstraction is elaborated in a context that expects an +erasable function, we wrap it into an additional erasable $\lambda$. So if the +previous type annotation is followed by: \begin{verbatim} map f x = ...; \end{verbatim} -it defines \texttt{map} as a normal $\lambda$ abstraction whereas the context -(from the previous type annotation) expects a function with two erasable -arguments, so the elaboration of the $\lambda$ will automatically add the two -additional (erasable) $\lambda$ corresponding to \texttt{?a} and \texttt{?b}. +the elaboration will automatically add the two additional (erasable) $\lambda$ +corresponding to \texttt{?a} and \texttt{?b}. + +We believe this behaves just like HM inference for the corresponding +sublanguage, but have not shown it yet. Also we do not know whether this +inference algorithm is guaranteed to terminate in theory, but it seems to +perform well in practice. Given that macro-expansion is allowed to perform +arbitrary side-effects, we have already given up the idea of guaranteeing +termination of elaboration anyway.
\section{Core language}
@@ -986,28 +1000,27 @@ and take it back out later, resulting in unsoundness~\cite{Coquand86b}.
Since Typer's impredicativity is limited to erasable elements, those large elements cannot really be taken back out later anyway, by virtue of their -erasability. For this reason, we conjecture that our form of +erasability. For this reason, we \emph{conjecture} that our form of impredicativity does not require this restriction on strong elimination. As a consequence, in Typer we can define the above inductive type (with an 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 -bottom. Clearly, this risks falling victim of paradoxes like -Hurken's~\cite{Hurkens95}, so buyer beware: we have no yet made any serious -attempt at proving or disproving the soundness of this extension. - The weak justification behind it, is a philosophical one: erasable arguments are not \emph{significant}, so a function that takes an erasable argument could be considered as a mere ``schema'' or ``prototype'' which stands for all the specialized versions of the function. A similar argument is discussed by Fruchart and Longo in~\cite{Fruchart96}.
+%% \subsection{Impredicativity rules of Typer} + +%% 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 +%% bottom. Clearly, this risks falling victim of paradoxes like +%% Hurken's~\cite{Hurkens95}, so buyer beware: we have no yet made any serious +%% attempt at proving or disproving the soundness of this extension. + + \section{Related work}
%% FIXME: re-order!
View it on GitLab: https://gitlab.com/monnier/typer/commit/1347e7b4fde3f332a915af40a98438bb6413...
Afficher les réponses par date