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

Commits: c66d283d by Christopher League at 2018-10-25T20:34:32Z Minor fixes, read through §5.1

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -5,6 +5,7 @@ \usepackage{mathpartir} \usepackage{mdframed,empheq} \usepackage{parskip} +\usepackage{fancyvrb} % prevent unfortunate line break in a short verbatim

\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} \DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}} @@ -101,8 +102,8 @@ support a fairly familiar infix syntax, yet simple enough that it maps straightforwardly to the equivalent of Lisp's S-expressions.

While the core language lets us manipulate proofs, Typer is mostly meant to -be used as a programming language. So we wanted that the power of fully -dependent types should not unduly get in the way of programs that do not +be used as a programming language. So we wanted the power of fully +dependent types to not unduly get in the way of programs that do not make use of them. Concretely, we tried to design Typer in such a way that programs can be written with just as few extra annotations as in any other ML-family language. @@ -155,8 +156,8 @@ two core elements: functions and datatypes. To define a function which adds \end{verbatim} %% Like in Agda~\cite{Bove09}, the type of dependently typed functions is -written ``\texttt{(x :~$\tau_1$) -> $\tau_2$}''. This could also have used a bit of -a syntactic sugar to become: +written ``\texttt{(x :~$\tau_1$) -> $\tau_2$}''. The definition above +could have used a bit of a syntactic sugar to become: \begin{verbatim} add1 x = x + 1; \end{verbatim} @@ -195,20 +196,20 @@ This allows you to introduce new locally scoped definitions. The shape of this construct is ``$\texttt{let}~\id{decls}~\texttt{in}~\id{exp}$'' where \id{decls} is a sequence of declarations such as the ones shown above, separated by -semi-colons. For example, we could have defined the above map function +semicolons. For example, we could have defined the above map function as follows: -\begin{verbatim} +\begin{Verbatim}[samepage=true] map f = let map' xs = case xs | nil => nil | cons x xs => cons (f x) (map' xs) in map' -\end{verbatim} -%As you can guess from this example, +\end{Verbatim} +%As you can guess from this example,

Typer has fundamentally two syntactic categories: expressions and declarations. A Typer file is defined as a sequence of declarations, -separated by semi-colons. +separated by semicolons. %% Most Lisps manage to conflate those two %% categories, but in our case, we were unable to unify them without %% introducing more problems. E.g. Common-Lisp solves the problem by treating @@ -253,7 +254,7 @@ Wherever the above macro is in scope, the programmer can write: Being purely functional, Typer resorts to the usual monadic technique to get access to a side effecting world, just as is done in Haskell. In the above code, \id{ME} is the macro-expansion monad, used for the same purpose as the -one used in Template Haskell~\cite{Sheard02}, and \id{return} is the unit of +one in Template Haskell~\cite{Sheard02}, and \id{return} is the unit of that monad.

\section{Syntactic structure}

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