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

Commits: eac6b267 by Stefan Monnier at 2018-10-29T20:39:17Z Reorder related works; make it fit in 16 pages

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -121,7 +121,7 @@ The paper presents the following contributions of the design of Typer: \item An elaboration phase which combines HM-style type inference and macro-expansion, relying on the inferred type information to distinguish macro calls. -\item A core language that extends ICC*~\cite{Barras08} with inductive types +\item An extension of ICC*~\cite{Barras08} with inductive types and a new rule for impredicativity. \end{itemize}

@@ -168,11 +168,11 @@ To define a new datatype to represent singly linked lists you can write: | cons (hd : a) (tl : List a); \end{verbatim} %% -where \id{hd} and \id{tl} are field names. We could have written just -\verb+cons a (List a)+ instead to keep the fields anonymous. - +where \id{hd} and \id{tl} are optional field names: we could have written just +\verb+cons a (List a)+ instead. +%% Functions and data constructors are curried. You can define the -traditional \id{map} function as follows: +\id{map} function as follows: \begin{verbatim} map : (a : Type) ⇛ (b : Type) ⇛ (a -> b) -> List a -> List b; @@ -264,7 +264,7 @@ that monad. \label{sec:syntax}

\newcommand \FigTyperSexp { - \begin{figure}[b] + \begin{figure} \begin{displaymath} \MAlign{ \kw{type}~\id{Sexp} \ @@ -278,7 +278,6 @@ that monad. \label{fig:Typer-Sexp} \end{figure} } -\FigTyperSexp

Once lexical analysis is performed, rather than performing the syntactic analysis in one step, Typer further subdivides the syntactic analysis phase @@ -291,6 +290,8 @@ 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}).

+\FigTyperSexp + 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 that S-expressions are analyzed to distinguish the various constructs such @@ -298,7 +299,7 @@ as macro calls, function calls, \kw{let} bindings, variable references, etc.

Any S-expression written using an infix or mixfix operator can also be written some other way, following the underscore convention of Agda's -mixfix~\cite{Danielsson08}. In the case of Typer, instead of writing +mixfix~\cite{Danielsson08}. In the case of Typer, instead of: \begin{verbatim} let x = a * b + c in x \end{verbatim} @@ -340,7 +341,7 @@ Then it will consider ``\texttt{+ (f(5) * 6) -}'' and add an open paren: ... g + ((f(5) * 6) - x ... \end{verbatim} and so on and so forth. What sets OPG apart here is that it makes these -choices without considering $e$ nor the surrounding context: instead, it +choices without considering $e$ nor the surrounding context: it bases its decision only on the pair of keywords.

In Typer, the grammar is represented by simply associating to each keyword @@ -455,10 +456,9 @@ is that macro's definition. %% turns it into an expression in Typer's core $\lambda$-calculus.

Elaboration is the phase in Typer's compiler which turns an S-expression -into an expression in Typer's core $\lambda$-calculus. We want a large part of -this phase to be itself implemented in Typer so that we can prove some of -its properties, such as the correctness of the compilation of pattern -matching~\cite{Cockx18}. +into an expression in Typer's core $\lambda$-calculus. We want most of this phase +to be itself implemented in Typer so that we can prove properties such as +the correctness of the compilation of pattern matching~\cite{Cockx18}.

Figure~\ref{fig:Lexp} shows the (simplified) representation used internally for that calculus. Notice that \id{Lexp} represents both what is usually @@ -727,11 +727,11 @@ extended with annotations to indicate which arguments are |~ (x:\tau_1)\TEarw\tau_2 ~|~ \lambda x:\tau \TEarw e ~|~ \TEapp{e_1}{e_2}} \end{array} \end{displaymath} -Those annotations are similar to those of Bernardy \etal's colored pure type -systems~\cite{Bernardy12}, in that the annotation on a function or function -call has to match the annotation of the function's type. -The rules of the colored pure type system corresponding to Typer's core -calculus are the following: +Those annotations are similar to those of Bernardy \etal's colored PTS +(CPTS)~\cite{Bernardy12}, in that the annotation on a function or function +call has to match the annotation of the function's type. The rules of the +CPTS corresponding to Typer's core calculus are the +following: \begin{displaymath} \begin{array}{lcl} \mathcal{S} &=& {~ \kw{Type}~\ell ~|~ \ell\in\mathbb{N} ~} \ @@ -746,8 +746,14 @@ 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: +Where $\mathcal{S}$ is the set of possible sorts (i.e.~types of types), +$\mathcal{A}$ is the set of axioms, and $\mathcal{R}$ specifies the set of +allowed abstractions: $(k, s_1, s_2, s_3)$ means that an arrow of color +$k$ can go from an argument in sort $s_1$ to a result in sort +$s_2$, and that this arrow will live in sort $s_3$. + +Compared to a normal CPTS, we use a slightly different typing rule for +erasable functions: \begin{displaymath} \Infer{\Jtyper {\tau_1} s \ \Jtyper[\Gamma,x:\tau_1] e {\tau_2} \ @@ -953,14 +959,14 @@ redundant in ICC*. More specifically: \begin{proof} By induction on the derivation of $\Jtyper[\Gamma_e] e {\tau_e}$. Since $\tau_e : \kw{Prop}$, clearly $e$ can neither be a sort nor an arrow type and it - cannot be $x$ itself either, so it can only be either a $\lambda y:\tau_y \to e_y$ or + cannot be $x$ itself either, so it can only be either a $\lambda y:\tau_y \to e_y$ or an application $e_1~e_2$. We can apply the induction hypothesis to $e_y$ and to $e_1$. As for $e_2$, there are two cases: either $e_1$ takes an argument of type $\tau_1:\kw{Type}~\ell'$ in which case we're done, or it takes an argument of type $\tau_1:\kw{Prop}$ in which case we can again apply the induction hypothesis. \end{proof} -Corollary: the rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since +Corollary: ICC*'s rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since we could convert all the impredicative functions that use it to functions that use $(\kw{e}, s, \kw{Prop}, \kw{Prop})$ instead.

@@ -975,9 +981,9 @@ this respect weaker than CIC. But Typer is incomparable to CIC because in another respect it allows things that CIC does not.

As mentioned before, CIC has a special restriction that large inductive -types (i.e. inductive types that belong to a universe that is smaller than +types (i.e.~inductive types that belong to a universe that is smaller than some of the values it carries) cannot be used in a strong elimination -(i.e. a \kw{case} analysis that returns a type in a universe larger than +(i.e.~a \kw{case} analysis that returns a type in a universe larger than that of the object analyzed).

This restriction means for example that while we can define in Coq @@ -988,15 +994,17 @@ a large inductive type like: | arw : Ω -> Ω -> Ω | all : forall k:Set, (k -> Ω) -> Ω. \end{verbatim} -we cannot prove properties such as: +we cannot prove properties such as the following (which we needed +while working on~\cite{Monnier07}): \begin{verbatim} forall K₁ K₂ F₁ F₂ P, all K₁ F₁ = all K₂ F₂ -> P K₁ F₁ -> P K₂ F₂. \end{verbatim} This important restriction significantly reduces the applicability of large -inductive types, but is needed because it would be otherwise possible to -``smuggle'' a large element within an inductive object of a smaller universe -and take it back out later, resulting in unsoundness~\cite{Coquand86b}. +inductive types, but is needed because it would be otherwise possible +to ``smuggle'' a large element within an inductive object of a smaller +universe 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 @@ -1026,16 +1034,7 @@ discussed by Fruchart and Longo in~\cite{Fruchart96}. %% FIXME: re-order!

%% FIXME: Shorten, and then add things: -%% F-star? ATS? - - %% - impredicativity and ICC, -%% - the handling of refinement (Zombie) -%% - let-generalizaintion -%% - comparison to template haskell's elaboration -%% - comparison to Idris -%% - comparison to Lean and Idris's elaboration/tacitcs tools -

%% \nocite{Miquel01,Barras08} %ICC %% \nocite{Bernardo09} %ICIC @@ -1050,12 +1049,66 @@ predecessors to be able to list them all. We will try and limit ourselves to some recent systems which share enough of their design or their goals here.

-\paragraph{Scala} provides sophisticated meta programming~\cite{Burmako13} -and staged computation~\cite{Rompf13} facilities used in novel ways. - -\paragraph{The Star language}\hspace{-10pt}~\cite{McCabe13} is statically +\paragraph{Honu}\hspace{-10pt}~\cite{Rafkind12} is a programming language in +the Racket system which provides an extensible infix/mixfix syntax +integrated with Racket's metaprogramming facilities. +\textbf{Typed Racket}~\cite{Felleisen11} uses an extension +of Scheme's macro system to implement a statically typed variant of Racket +as a sort of embedded DSL, thus implementing the type checker as part of +a macro. It shares with Typer the characteristic of mixing Lisp-style +macros and static typing, and generally the Racket system shares with Typer +the goal of a being a ``language workbench'' on top of which other languages +can easily be defined, Typed Racket and Honu being just some examples. +%% At first look one might see Typer as a dependently typed Typed +%% Racket. Indeed both have a powerful macro system and a static type +%% system. But there are some important differences. The first difference +%% directly related to this article is that Typed Racket lacks built-in +%% support for mixfix. +%% +%% Another important difference is that Typed Racket macros ala Scheme are +%% hygienic while Typer's macros currently do not provide hygiene. +%% %% Typer is still in its infancy and hygienic macros is future work. +%% Also, Typer's macros are intended to work with dependently typed pieces of +%% code and mathematical proofs and thus require access to the type environment +%% at the expansion site. Typed Racket and more generally Scheme macros, on +%% the other hand, do not have access to the lexical environment at the +%% expansion site. +The \textbf{Star} language~\cite{McCabe13} is a statically typed programming language which also makes it easy to define embedded DSLs via syntactic and macro expansion facilities. +\textbf{Scala} also provides sophisticated meta programming~\cite{Burmako13} +and staged computation~\cite{Rompf13} facilities used in novel ways. +\textbf{OCaml} offers extensible syntax and metaprogramming +facilities in various forms, such as via its Camlp4 +system~\cite{de2003camlp4} and more recently with \emph{extension points}, +which work like macros, by mapping OCaml AST to OCaml AST. +%% where the ``P4'' stands for PreProcessor +%% and Pretty-Printer. Much like a macro system, it allows the programmer to +%% describe an extension to the OCaml parser. The job of CamlP4 is to convert +%% those extensions to standard OCaml's AST. The syntax extension is transparent +%% to the programmer. But CamlP4 is a separate tool from the compiler and the +%% drawback of this approach is that, unlike Nemerle or Typer, syntactic +%% extensions do not have access to typing information. +%% This is one of the +%% main reasons why Typer adopts a macro system which is build-in with +%% the compiler. +%% +%% ToDo : Find article/citation for Alain Frisch extension points (if any) +%% Recent versions of OCaml (after version 4.01.0) also come with +%% . The grammar now accepts annotations to the source file and +%% a special construct, extension nodes, for syntax extension. When the +%% compiler encounters an annotated branch in the AST or an extension node in +%% an expression it calls the macro associated with the annotation. Of course, +%% as in the case of Template Haskell, this means that uses of those extensions +%% have to use a special syntax and hence feel like second-class features. +%% +%% In a language like Typer, where the philosophy is to push most +%% constructs out of the compiler and into libraries such method would +%% result in the source file being fully annotated everywhere. For +%% example, \id{if_then_else} and many other constructs are part of the +%% OCaml syntax and would require annotation in Typer if we were to use +%% such strategy. We therefore think Typer has hit a sweet spot between +%% Lisp and OCaml.

\paragraph{Template Haskell}\hspace{-10pt}~\cite{Sheard02} is an extension of Haskell to allow @@ -1067,15 +1120,23 @@ purely functional language. %% For such purpose, our use of a Typer's interleaving of type inference and macro expansion is very similar to that of Template Haskell. But Typer and Template Haskell differ on how the macros are used by the programmer: in Template Haskell, macro calls are -made explicit in the source file by preceding them with a $ sign rather +made explicit in the source file by preceding them with a \Char{$} sign rather than being determined by their type. Also Template Haskell is not meant to add new binding forms to the language: arguments to the macro are type checked before being passed to the macro. +%%

-\paragraph{Zombie}\hspace{-10pt}~\cite{Casinghino14} is an experimental +\paragraph{Idris}\hspace{-10pt}~\cite{Brady13} and +\textbf{F-Star}~\cite{Swamy16} are programming languages with dependent +types. They shares many of Typer's goals and also offers metaprogramming +facilities, although these facilities are more aimed at writing proofs, +while Typer's metaprogramming facilities are more currently geared toward +syntactic extensions. +%% +\textbf{Zombie}~\cite{Casinghino14} is an experimental programming language with dependent types. One of its most novel features is to eschew automatic reductions at the type level and require manual cast -operation instead. This is a bit like of Typer's intentionally weak typing +operations instead. This is a bit like of Typer's intentionally weak typing rule for \kw{case}, relying on explicit cast operations using type equality witnesses for type refinement, but pushed yet further.

@@ -1086,37 +1147,22 @@ not just infix operators. Their use of mixfix operators like the idea of adding mixfix to S-expressions in Typer using operator precedence grammar. For a more detailed and formal discussion on mixfix operators and Agda, see~\cite{Danielsson08}. - -\paragraph{Idris}\hspace{-10pt}~\cite{Brady13} is a programming language -based on type theory. It shares many of Typer's goals and also offers -metaprogramming facilities. - -\paragraph{Honu}\hspace{-10pt}~\cite{Rafkind12} is a programming language in -the Racket system which provides an extensible infix/mixfix syntax -integrated with Racket's metaprogramming facilities. - -\paragraph{Typed Racket}\hspace{-10pt}~\cite{Felleisen11} uses an extension -of Scheme's macro system to implement a statically typed variant of Racket -as a sort of embedded DSL, thus implementing the type checker as part of -a macro. It shares with Typer the characteristic of mixing Lisp-style -macros and static typing, and generally the Racket system shares with Typer -the goal of a being a ``language workbench'' on top of which other languages -can easily be defined, Typed Racket and Honu being just some examples. - -%% At first look one might see Typer as a dependently typed Typed -%% Racket. Indeed both have a powerful macro system and a static type -%% system. But there are some important differences. The first difference -%% directly related to this article is that Typed Racket lacks built-in -%% support for mixfix. - -%% Another important difference is that Typed Racket macros ala Scheme are -%% hygienic while Typer's macros currently do not provide hygiene. -%% %% Typer is still in its infancy and hygienic macros is future work. -%% Also, Typer's macros are intended to work with dependently typed pieces of -%% code and mathematical proofs and thus require access to the type environment -%% at the expansion site. Typed Racket and more generally Scheme macros, on -%% the other hand, do not have access to the lexical environment at the -%% expansion site. +%% +\textbf{Coq}~\cite{Coq00} has syntactic extensions similar +to mixfix as well as a sophisticated metaprogramming language known as +Ltac~\cite{Delahaye00}. More recently other metaprogramming languages have +been designed for it such as Mtac~\cite{Ziliani13} and Rtac~\cite{Malecha16}. +%% Coq's syntactic +%% extensions, based on CamlP4, are fairly sophisticated. But Coq's +%% metaprogramming language is a separate language that is very different from +%% Coq core language Gallina and you can't directly invoke Ltac tactics from +%% Gallina code. This is a key difference between Coq and Typer. We wish for +%% Typer to have the same language for both purposes as Lisp and Scheme have +%% already demonstrated the benefits of having the same language for both. +%% +%% Nonetheless, it remains to be shown that macros are as user-friendly +%% to automate mathematical proofs as tactics written in Ltac which is a +%% domain specific language tailored for this task.

%% \subsection{Dylan} %% Dylan~\cite{Dylan,Backrach99} is a functional and object-oriented @@ -1194,56 +1240,6 @@ can easily be defined, Typed Racket and Honu being just some examples. %% %% to Typer's macros who also have access to the environment at the %% %% expansion site.

-\paragraph{OCaml}\hspace{-10pt} offers extensible syntax and metaprogramming -facilities in various forms, such as via its Camlp4 -system~\cite{de2003camlp4} and more recently with \emph{extension points}, -which work like macros, by mapping OCaml AST to OCaml AST. - -%% where the ``P4'' stands for PreProcessor -%% and Pretty-Printer. Much like a macro system, it allows the programmer to -%% describe an extension to the OCaml parser. The job of CamlP4 is to convert -%% those extensions to standard OCaml's AST. The syntax extension is transparent -%% to the programmer. But CamlP4 is a separate tool from the compiler and the -%% drawback of this approach is that, unlike Nemerle or Typer, syntactic -%% extensions do not have access to typing information. -%% This is one of the -%% main reasons why Typer adopts a macro system which is build-in with -%% the compiler. - -%ToDo : Find article/citation for Alain Frisch extension points (if any) -%% Recent versions of OCaml (after version 4.01.0) also come with -%% . The grammar now accepts annotations to the source file and -%% a special construct, extension nodes, for syntax extension. When the -%% compiler encounters an annotated branch in the AST or an extension node in -%% an expression it calls the macro associated with the annotation. Of course, -%% as in the case of Template Haskell, this means that uses of those extensions -%% have to use a special syntax and hence feel like second-class features. - -%% In a language like Typer, where the philosophy is to push most -%% constructs out of the compiler and into libraries such method would -%% result in the source file being fully annotated everywhere. For -%% example, \id{if_then_else} and many other constructs are part of the -%% OCaml syntax and would require annotation in Typer if we were to use -%% such strategy. We therefore think Typer has hit a sweet spot between -%% Lisp and OCaml. - -\paragraph{Coq}\hspace{-10pt}~\cite{Coq00} has syntactic extensions similar -to mixfix as well as a sophisticated metaprogramming language known as -Ltac~\cite{Delahaye00}. More recently other metaprogramming languages have -been designed for it such as Mtac~\cite{Ziliani13} and Rtac~\cite{Malecha16}. -%% Coq's syntactic -%% extensions, based on CamlP4, are fairly sophisticated. But Coq's -%% metaprogramming language is a separate language that is very different from -%% Coq core language Gallina and you can't directly invoke Ltac tactics from -%% Gallina code. This is a key difference between Coq and Typer. We wish for -%% Typer to have the same language for both purposes as Lisp and Scheme have -%% already demonstrated the benefits of having the same language for both. - -%% Nonetheless, it remains to be shown that macros are as user-friendly -%% to automate mathematical proofs as tactics written in Ltac which is a -%% domain specific language tailored for this task. - - \section{Conclusion}

Typer is a new experimental language in the family of dependently typed

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