part1-zilch.tex

.\begingroup
\usingnamespace{zilch:grammar}
\usingnamespace{zilch:rules}


\part{The language}\label{part:zilch}

\chapter{Introduction}\label{chap:zilch-introduction}

Low-level programming is programming with a few abstractions over the hardware.
For example, assembly languages mostly provide no or very little abstractions over CPU instructions (having one instruction set per target).
Functional programming is a kind of programming focused around functions and their composition.
However, because of this, many functional programming languages have a tendancy to be quite slow, at least compared to ``ordinary'' imperative programming languages.

\href{http://www.ats-lang.org/}{ATS} is one of those programming languages claiming to be both functional and quite low-level.
It compiles to C (therefore has a free FFI), has a complex dependent type system and many other things making it kind of great.
But ATS is hard to learn, because it has so much stuff\ldots

Yet Zilch is also a low-level functional programming language.
But the goal is to design a not-so-hard to learn programming language, while still having strong guarantees about the code written\footnote{When this was written, Zilch was far from production-ready, so most
	of the guarantees have not yet been described here.}.
Prior knowledge about ML-style programming is still recommended before trying to tackle Zilch, but anybody without this kind of knowledge should also be able to learn Zilch fairly easily.

This part will try to describe and formalize (at least a bit, but some parts may be left informal) the Zilch programming language, going from the usual syntax onto the operational semantics.
Implementation details (such as error messages, program optimisations, \ldots) will not be covered by this document.

\section*{Some notes on the notation used}\label{sec:zilch-introduction-notation}

Zilch is really not a small programming language.
Because of that, sometimes we need some specific notation to described things like inference rules.

The mainly used notation is described here, but not necessarily everything will be described (sometimes, a little bit of common sense helps to understand).

\begin{itemize}
	\item Grammar
	      \begin{figure}[H]
		      \centering
		      \scalebox{.5}{
			      \includegraphics{grammar-template-2}
		      }
	      \end{figure}
	      \begin{itemize}
		      \item Sharp rectangles describe that another rule is to be used there (the name of the rule is given in the rectangle);
		      \item Rounded rectangles describe terminal tokens, i.e.\ pieces of string that must be litterally matched;
		      \item The name of the grammar rule defined is given in the top-left corner of the diagram.
		            A rule matches if and only if it is possible to go from the left to the right, only following the rails;
	      \end{itemize}
	\item Type inference rules
	      \begin{itemize}
		      \item $\Gamma$ is the context containing all type-level information such as types of expressions;
		      \item The typing judgment $\TypeSequent{\Gamma}{e}{\rho}{\tau}{\epsilon}$ means that $e$ has type $\tau$ with multiplicity $\rho$ in the context $\Gamma$ and that evaluating it may yield effects in $\epsilon$;
		      \item $\scale{\pi}{\Gamma}$ denotes the scaling (multiplication) of all the multiplicities within $\Gamma$ by $\pi$;
		      \item $\add{\Gamma_1}{\Gamma_2}$ is pointwise addition between the two contexts $\Gamma_1$ and $\Gamma_2$.
	      \end{itemize}
\end{itemize}

\chapter{Grammar of Zilch programs}\label{chap:zilch-grammar}

A Zilch program is comprised of three different levels, each included in the next one:
\begin{itemize}
	\item The expression level, where an expression denotes a value which has a statically determined type;
	\item The declaration level, containing all function definitions, type definitions, etc;
	\item The module level, where imports and module declarations live in;
\end{itemize}

\noindent Because it is not easy to materialize indentation properties in the grammar, it will instead be marked using the non-terminals\footnote{Those symbols are reserved and actually used as terminals, so we put them as non-terminals to remove any ambiguity opportunities.} \texttt{\{}, \texttt{\}} and \texttt{;}.
Note that these are not actually present in the source code, and are only a mean of hinting an indentation change.
\texttt{x \{ y; z \}} really means \texttt{x} followed by \texttt{y} which may be more indented or on the same line, and \texttt{z} which must be aligned with the beginning of \texttt{y}.
It therefore describes both layouts:

\noindent\begin{minted}{\zilchlexer}
  -- `y` on the same line as `x`:
  x y
    z
  -- or `y` on a new line:
  x
    y
    z
\end{minted}
\vspace*{\baselineskip}

\begin{warningbox}
	If you are willing to make your own Zilch compiler, please note that you may also (or only) support the alternative layout as described in grammar rules, by making use of \verb|{|, \verb|;| and \verb|}| as terminals.
	It is not recommended, as \verb|;| is \textit{not} a reserved word, but may be considered for simplicity's sake.
	It is also not recommended as using \verb|{| and \verb|}| may clash with inline records and implicit parameters.
\end{warningbox}

\section{Lexicon}\label{sec:zilch-grammar-lexical}

This section describes the lexical structure of any Zilch program.
Note that the Unicode alternative syntax does not need to be supported, but makes the code look nicer.

\subsection{Identifiers, operators and reserved words}\label{subsec:zilch-grammar-lexical-identifiers}

Identifiers and operators are composed of only printable characters which are not considered special, and must not form keywords.
Lexically distinguishing between both types of symbols is done by only allowing alphanumeraical characters in identifiers, and symbolic characters in operators.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.75}{
				\includegraphics[width=\linewidth]{zilch/lexicon/keywords}
			}
			\\
			\scalebox{.8}{
				\includegraphics[width=\linewidth]{zilch/lexicon/special}
			}
			\\
			\scalebox{.4}{
				\includegraphics[width=\linewidth]{zilch/lexicon/identifier}
			}
		}
	}

	\caption{Lexical units for identifiers and operators.}
	\label{fig:zilch-grammar-lexical-identifiers-grammar}
\end{figure}

\subsection{Whitespaces}\label{subsec:zilch-grammar-lexical-whitespaces}

Whitespace tokens are basically word separators.
Because of that, comments are also counted as whitespaces, despite not really being an invisible sequence.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.5}{
			\includegraphics{zilch/lexicon/whitespaces}
		}
	}

	\caption{Whitespace lexical units.}
	\label{fig:zilch-grammar-lexical-whitespaces-grammar}
\end{figure}

\subsection{Numerical tokens}\label{subsec:zilch-grammar-lexical-numbers}

There are two kinds of numerical tokens: integers and floating points.
While floating points are always written using decimal digits, integers may be written using decimal digits, octal digits (if prefixed by \verb|0o| or \verb|0O|), hexadecimal digits (if prefixed by \verb|0x| or \verb|0X|) or binary digits (if prefixed by \verb|0b| or \verb|0B|).
A floating point number must always have digits on both sides of the dot (i.e.\ it is impossible to write \verb|0.| as in other programming languages) because it could else be mistaken with the dot syntax.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.5}{
			\includegraphics{zilch/lexicon/number}
		}
	}

	\caption{Numeric lexical units.}
	\label{fig:zilch-grammar-lexical-numbers-grammar}
\end{figure}

\subsection{String and character literals}\label{subsec:zilch-grammar-lexical-strings}

Strings are arrays of characters.
However, because it is tedious to write such arrays, we provide syntactic sugar to make it easier.

String literals are enclosed in double quotes \verb|"|, and character literal are enclosed in single quotes \verb|'|.
They can contain any character (both graphical and whitespaces), but some characters may be easier to type.
These basically have ``shorthands'' defined as escape sequences, each defined in Table~\ref{table:zilch-grammar-lexical-strings-escapesequences}.
Note that, while double and single quotes may be escaped, these may not necessarily be in respectively character and string literals.

Multiple string literals directly next to each other (as in \mintinline{\zilchlexer}{"abc" "def"}) are concatenated into one (so \mintinline{\zilchlexer}{"abcdef"}).

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.5}{
				\includegraphics{zilch/lexicon/string}
			}
			\\
			\scalebox{.5}{
				\includegraphics{zilch/lexicon/character}
			}
		}
	}

	\caption{String and character lexical units.}
	\label{fig:zilch-grammar-lexical-strings-grammar}
\end{figure}

\begin{table}[H]
	\begin{tabularx}{\textwidth}{*{5}{Y}}
		\toprule
		\verb|\a| & \verb|\b| & \verb|\f| & \verb|\n| & \verb|\r| \\
		\verb|\t| & \verb|\v| & \verb|\\| & \verb|\"| & \verb|\'| \\
		\bottomrule
	\end{tabularx}

	\caption{All available escape sequences.}
	\label{table:zilch-grammar-lexical-strings-escapesequences}
\end{table}

\section{Expressions}\label{sec:zilch-grammar-expressions}

Expressions are the basic building block of Zilch.
\textit{Everything} is an expression, from simple arithmetic like \texttt{3 + 6} to complex \texttt{let-in} expressions.

\subsection{Lambda abstraction}\label{subsec:zilch-grammar-expressions-lambda}

Lambda abstractions allow creating ``in-place'' anonymous functions.
For example, both following alternatives are equivalent (because the lambda abstraction does not capture anything there):
\begin{listing}[H]
	\inputminted{\zilchlexer}{examples/captureless-lambda-equivalence.zc}

	\captionsetup{style=invisible}
	\caption{Equivalence of non-capturing lambda with top-level function.}
\end{listing}
\vspace*{-\baselineskip}

\noindent However, these two are not quite equivalent:
\begin{listing}[H]
	\inputminted{\zilchlexer}{examples/closure-non-equivalence.zc}

	\captionsetup{style=invisible}
	\caption{Non-equivalence of capturing lambda with top-level function.}
\end{listing}
\vspace*{-\baselineskip}

\begin{infobox}
	Recursive lambda abstractions are unsupported.
	If you are feeling the need to have those, simply bind them to \texttt{rec} declaration, such as:
	\vspace*{\baselineskip}

	\begin{minted}{\zilchlexer}
		rec mylam := lam(x, y) => mylam(x, y)
  \end{minted}
\end{infobox}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.85}{
			\includegraphics[width=\linewidth]{zilch/expression/lambda}
		}
	}

	\caption{Grammar for lambda abstractions.}
	\label{fig:zilch-gramma-expressions-lambda-grammar}
\end{figure}

\subsection{Conditional}\label{subsec:zilch-grammar-expressions-conditional}

Conditional expressions allow selecting an expression based off the value of a condition.
However, it only works as a binary selector.
If n-ary selectors are needed, chaining \texttt{if}s is the only solution.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.5}{
			\includegraphics{zilch/expression/conditional}
		}
	}

	\caption{Grammar for conditional expressions.}
	\label{fig:zilch-gramma-expressions-conditional-grammar}
\end{figure}

\subsection{Let-in}\label{subsec:zilch-grammar-expressions-letin}

Let-in expressions allow binding local variables in the context of another expression.
However, it does not act the same as simply replacing the variable just like a macro because of evaluation order and potential side-effects.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.5}{
			\includegraphics{zilch/expression/let-in}
		}
	}

	\caption{Grammar for let-in blocks.}
	\label{fig:zilch-grammar-expressions-letin-grammar}
\end{figure}

\subsection{Local imports}\label{subsec:zilch-grammar-expressions-import}

One may want to import specific functions from given modules only in the scope of a function as these functions will only be used there.
This construct allows to scope imports closer to where they actually are used, by allowing the import to be local to an expression which may use it.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.5}{
			\includegraphics[width=\linewidth]{zilch/expression/import}
		}
	}

	\caption{Grammar for local import blocks.}
	\label{fig:zilch-grammar-expressions-import-grammar}
\end{figure}

\subsection{Pattern matching}\label{subsec:zilch-grammar-expressions-match}

Pattern matching is achieved through the use of a \texttt{match} expression.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.5}{
				\includegraphics{zilch/expression/pattern}
			}\\
			\scalebox{.9}{
				\includegraphics[width=\linewidth]{zilch/expression/match}
			}
		}
	}

	\caption{Grammar for match expressions.}
	\label{fig:zilch-grammar-expressions-match-grammar}
\end{figure}

\subsection{Record literals}\label{subsec:zilch-grammar-expressions-record}

Record literals allow constructing records in the same fashion as in e.g.\ C.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.5}{
			\includegraphics[width=\linewidth]{zilch/expression/record}
		}
	}

	\caption{Grammar for record literals.}
	\label{fig:zilch-gramma-expressions-record-grammar}
\end{figure}

\subsection{Variables, typed holes and literals}\label{subsec:zilch-grammar-expressions-basicexpr}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.7}{
			\includegraphics[width=\linewidth]{zilch/expression/atom}
		}
	}

	\caption{Grammar for expression atoms.}
	\label{fig:zilch-grammar-expressions-atom-grammar}
\end{figure}

% NOTE: &x now denotes making a reference
%
% The by-ref operator \texttt{\&id} is only allowed if it appears within the top-most application in a \texttt{let} local binding.
% For example, these uses of the by-ref operator are valid:
% \begin{listing}[H]
% 	\inputminted{\zilchlexer}{examples/correct-byref.zc}

% 	\captionsetup{style=invisible}
% 	\caption{Correct usage of by-ref operator.}
% \end{listing}
% \vspace*{-\baselineskip}

% Hoewver, these uses are invalid:
% \begin{listing}[H]
% 	\inputminted{\zilchlexer}{examples/incorrect-byref.zc}

% 	\captionsetup{style=invisible}
% 	\caption{Incorrect usage of by-ref operator.}
% \end{listing}
% \vspace*{-\baselineskip}
% In \texttt{test2}, the by-ref operator is in fact used in the application of \texttt{+} (recall that \texttt{a + b} is \texttt{\_+\_(a, b)}), which is not the top-most application in this local binding.

\subsection{Additive and multiplicative pairs}\label{subsec:zilch-grammar-expressions-pairs}

Pairs are separated into two distinct types, following LTT\footnote{Linear Type Theory}, to encode whether the two elements must be used or if only one is expected to be consumed.
It is possible to consume a single element from an additive pair, while all the elements must be consumed in a multiplicative pair.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.5}{
				\includegraphics[width=\linewidth]{zilch/expression/pair-mult-intro}
			}\\
			\scalebox{.8}{
				\includegraphics[width=\linewidth]{zilch/expression/pair-mult-elim}
			}
		}
	}

	\caption{Grammar for multiplicative pairs and eliminator.}
	\label{fig:zilch-grammar-expressions-pairs-mult-grammar}
\end{figure}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.5}{
				\includegraphics[width=\linewidth]{zilch/expression/pair-add-intro}
			}\\
			\scalebox{.6}{
				\includegraphics[width=\linewidth]{zilch/expression/pair-add-elim}
			}
		}
	}

	\caption{Grammar for additive pairs and eliminator.}
	\label{fig:zilch-grammar-expressions-pairs-add-grammar}
\end{figure}

\section{Types}\label{sec:zilch-grammar-types}

Types lie at the same level as expressions, but are put in a separate section for comprehensiveness sake.
An expression \verb|e| is said to be of type \verb|t| if evaluating it yields (or at least is supposed to) any value in the set \verb|t|.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.5}{
			\includegraphics{zilch/types/builtin}
		}
	}

	\caption{Grammar for builtin types.}
	\label{fig:zilch-grammar-types-builtin-grammar}
\end{figure}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.8}{
			\includegraphics[width=\linewidth]{zilch/types/effect-row}
		}
	}

	\caption{Grammar for effects rows.}
	\label{fig:zilch-grammar-types-effectrow-grammar}
\end{figure}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.8}{
				\includegraphics[width=\linewidth]{zilch/types/implicit-parameter}
			}\\
			\scalebox{.8}{
				\includegraphics[width=\linewidth]{zilch/types/explicit-parameter}
			}\\
			\scalebox{.8}{
				\includegraphics[width=\linewidth]{zilch/types/instance-parameter}
			}\\
			\scalebox{.85}{
				\includegraphics[width=\linewidth]{zilch/types/dependent}
			}
		}
	}

	\caption{Grammar for dependent types.}
	\label{fig:zilch-grammar-types-dependent-grammar}
\end{figure}

\begin{warningbox}
	The grammar for dependent types presented in figure~\ref{fig:zilch-grammar-types-dependent-grammar} allows more programs to be parsed than what is actually valid.
	Here is a list of erroneous syntactic objects:
	\begin{itemize}
		\item \texttt{$\otimes$}, \texttt{×} and \texttt{\&} types with implicit or instance parameters;
		\item \texttt{$\otimes$}, \texttt{×} and \texttt{\&} types with an effect row (unless it is the empty row \texttt{$\langle\rangle$});
		\item \texttt{\&} types with a multiplicity on any parameter (unless it is the unrestricted multiplicity \texttt{@$\omega$}).
	\end{itemize}
\end{warningbox}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.4}{
			\includegraphics[width=\linewidth]{zilch/types/universe-level}
		}
	}

	\caption{Grammar for universe levels.}
	\label{fig:zilch-grammar-types-level-grammar}
\end{figure}

\section{Declarations}\label{sec:zilch-grammar-declarations}

A Zilch module is composed of zero or more declarations.
There are 4 possible declarations:
\begin{itemize}
	\item New type definition;
	\item Effect definition;
	\item Value definition;
	\item Definition opening.
\end{itemize}

\noindent Each of them will be syntactically described in this section.

\subsection{Value definition}\label{subsec:zilch-grammar-declarations-value}

A function binding binds a variable to a value.
Both when the value is of a function type or of a simple value type, the binding is called a \textit{function binding}.
\vspace*{\baselineskip}

Because functions are first-class in Zilch, both function bindings defined below are completely equivalent (the lambda abstraction does not capture anything here):

\begin{listing}[H]
	\inputminted{\zilchlexer}{examples/function-value-equivalence.zc}

	\captionsetup{style=invisible}
	\caption{\texttt{let} with parameters and lambda equivalence.}
\end{listing}
\vspace*{-\baselineskip}

Function bindings may additionally be accompanied by \verb|where| blocks, which allow binding local variables in the scope of the expression.
This is mostly equivalent to putting those bindings at the beginning of a \verb|let-in| block:

\begin{listing}[H]
	\inputminted{\zilchlexer}{examples/function-where-let-equivalence.zc}

	\captionsetup{style=invisible}
	\caption{\texttt{where} equivalence with local \texttt{let} bindings.}
\end{listing}
\vspace*{-\baselineskip}

Note that recursive function bindings (bindings calling themselves in their definitions) are only allowed for \textit{functions}, and must be prefixed by \verb|rec| instead of \verb|let|.

Mutable function bindings are only allowed for non-recursive value bindings (i.e. \mintinline{\zilchlexer}{mut x : t := e} is allowed (if \verb|t| is a value type) but neither \mintinline{\zilchlexer}{mut x : t := x} nor \mintinline{\zilchlexer}{mut f(x) := e} are actually valid).

Top-level function bindings can additionnally be prefixed with special meta-attributes (described later in Section~\ref{subsec:zilch-grammar-declarations-meta}~``\nameref{subsec:zilch-grammar-declarations-meta}'').

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.9}{
				\includegraphics[width=\linewidth]{zilch/toplevel/function-definition}
			}\\
			\scalebox{.85}{
				\includegraphics[width=\linewidth]{zilch/toplevel/implicit-parameter}
			}\\
			\scalebox{.85}{
				\includegraphics[width=\linewidth]{zilch/toplevel/explicit-parameter}
			}\\
			\scalebox{.85}{
				\includegraphics[width=\linewidth]{zilch/toplevel/instance-parameter}
			}
		}
	}

	\caption{Grammar for value declarations.}
	\label{fig:zilch-grammar-declarations-value-grammar}
\end{figure}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.9}{
			\includegraphics[width=\linewidth]{zilch/toplevel/toplevel-function-definition}
		}
	}

	\caption{Grammar for top-level value definitions.}
	\label{fig:zilch-grammar-declarations-value-toplevel-grammar}
\end{figure}

\subsection{Effect definition}\label{subsec:zilch-grammar-declaration-effect}

Side effects lie everywhere in programming: from basic console I/O, networking, etc to mutating global variables.
Some programming languages (e.g. C, Java, etc) do not restrict those side effects to occur, leading to uncontrolled/undefined/undesirable behaviors.
Some other take a stricter route (e.g. Haskell, Koka, etc) and do not allow side effects occurring anywhere (Haskell uses monads, Koka uses algebraic effects).

In Zilch, the algebraic effects route has been taken as it seems to lead to more readable code, and can be compiled more efficiently, and mostly without surprises.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.9}{
			\includegraphics[width=\linewidth]{zilch/toplevel/effect-definition}
		}
	}

	\caption{Grammar for effect definitions.}
	\label{fig:zilch-grammar-declarations-effects-grammar}
\end{figure}

\subsection{New type definition}\label{subsec:zilch-grammar-declarations-type}

Sometimes, only working with primitive types is limiting.
For example, a function returning an unsigned integer may need to indicate some sort of error.

\noindent C-style programming languages use special values which are considered invalid as return values (e.g.\ $-1$).
This doesn't quite work when no return value from the return set is actually invalid, but the function is still expected to be able to indicate failure.

\noindent This is where custom types come in: it is possible to define a new ``or''-type (called ``enum'' in Zilch) to represent either a return value or no return value (in the case of a failure), usually called ``\texttt{Option}'' or ``\texttt{Maybe}''.

A function may also be expected to return multiple values.
In C-style programming languages, making use of references/pointers is one way, but using structures (called ``record''s) is the way to go in Zilch.

And some other times, using a specific type is not semantically clear enough.
For example, what does a \texttt{u64} mean as input to a function?
Zilch allows defining type aliases to address this issue, leading to code more clear.

When using the Foreign Function Interface (FFI), we may also want to interface with types.
However, types do not necessarily exist in the FFI, so they cannot be dynamically checked.
Moreover, some types usually defined in C (such as \texttt{FILE}) are very much implementation dependent, and it is not a good idea to rewrite them in Zilch.
In such cases, we can define \texttt{opaque} erased types (and only erased types, functions cannot be \texttt{opaque}) which can only be passed around behind pointers\footnote{Because the size of the type is unknown at compile-time, it is not possible to statically allocate enough memory on the stack to pass opaque data for function calls. However, if they are necessarily found behind pointers, we can just allocate the size of the pointer onto the stack.}.
An opaque type is of an unknown size which is guaranteed to be greater than 0.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.85}{
				\includegraphics[width=\linewidth]{zilch/toplevel/enum-definition}
			}\\
			\scalebox{.95}{
				\includegraphics[width=\linewidth]{zilch/toplevel/record-definition}
			}
		}
	}

	\caption{Grammar for new type definitions.}
	\label{fig:zilch-grammar-declarations-type-grammar}
\end{figure}

\begin{warningbox}
	The expression on the right hand side of the \texttt{:} in the declaration of a \texttt{record} is required to be of the form \texttt{type l} (where \texttt{l} can be anything).
	Any other expression must be considered invalid.
\end{warningbox}

\subsection{Mutually recursive definitions}\label{subsec:zilch-grammar-declarations-mutual}

Top-level bindings can refer to other top-level bindings as long as these are declared beforehand.
However, sometimes it is useful to define a few functions or data types which are mutually recursive.
For example, consider the following definitions for the two functions \texttt{even} and \texttt{odd} which return \texttt{true} if the number is even (resp. odd):
\begin{align*}
	\operatorname{even}(n) & = \begin{cases*}
		                           \mathrm{true}             & iff $n = 0$ \\
		                           \operatorname{odd}(n - 1) & otherwise
	                           \end{cases*}  \\
	\operatorname{odd}(n)  & = \begin{cases*}
		                           \mathrm{false}             & iff $n = 0$ \\
		                           \operatorname{even}(n - 1) & otherwise
	                           \end{cases*}
\end{align*}

This can be modeled in Zilch as:
\begin{listing}[H]
	\inputminted{\zilchlexer}{examples/mutual-even-odd.zc}

	\captionsetup{style=invisible}
	\caption{Mutual definitions of \texttt{even} and \texttt{odd}.}
\end{listing}\vspace*{-\baselineskip}
Note that without the \texttt{mutual} block, the definition of \texttt{even} would be considered ill, as \texttt{odd} does not exist in the scope yet.

An alternative modeling of this problem is by using \textit{forward declarations} (as in C) to declare the function \texttt{odd} before the function \texttt{even} so that \texttt{even} is allowed to make references to it.
This would be done as follows:
\begin{listing}[H]
	\inputminted{\zilchlexer}{examples/forwarddecls-even-odd.zc}

	\captionsetup{style=invisible}
	\caption{\texttt{even}/\texttt{odd} with forward declarations.}
\end{listing}
\vspace*{-\baselineskip}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.8}{
			\includegraphics[width=\linewidth]{zilch/toplevel/function-declaration}
		}
	}

	\caption{Grammar for value forward declarations.}
	\label{fig:zilch-grammar-declarations-mutual-forwarddecls-grammar}
\end{figure}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\scalebox{.6}{
			\includegraphics[width=\linewidth]{zilch/toplevel/mutual-definition}
		}
	}

	\caption{Grammar for mutual block definition.}
	\label{fig:zilch-grammar-declarations-mutual-block-grammar}
\end{figure}

\subsection{Meta-information}\label{subsec:zilch-grammar-declarations-meta}

Meta-information can be added to any top-level declaration.
They can be used for example to declare operator fixities, or add deriving clauses to auto-generate type class instances.
Any declaration accepts zero or more meta-specifiers, but each specifier is restricted as per these rules:
\begin{itemize}
	\item Fixity specifiers can only be applied to mixfix operators.
	      These are used to disambiguate expressions, and come in 5 flavors:
	      \begin{itemize}
		      \item \verb|infix <prec>|, \verb|infixr <prec>| and \verb|infixl <prec>| allow specifying the associativity (left, right or none) and precedence of infix operators (operators of the form \verb|_..._|);
	      \end{itemize}
	\item Deriving clauses can only be added to \verb|enum| and \verb|record| types;
	\item Inlining hints tell the compiler that a function may not have a huge cost, therefore can be inlined more easily;
	\item FFI imports/exports, to either retrieve or give a function defined in another compilation unit (most probably coming from another programming language like C);
	\item Default effect handlers can be added to any function binding of type \texttt{\{e\} -> \{a\} -> (() -> < eff | e > a) -> e a} (meaning it consumes the effect \verb|eff| given) (implicits may be given in any order).
	      These are used to remove any additional effects on the \verb|main| function without having to specify each of them.
	      Note that those handlers are implicitly internally exported (even when not \verb|public|), but still need to be \verb|public| to be used by hand.
\end{itemize}

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.7}{
				\includegraphics[width=\linewidth]{zilch/toplevel/meta-information}
			}\\
			\scalebox{.75}{
				\includegraphics[width=\linewidth]{zilch/toplevel/meta-specifier}
			}
		}
	}

	\caption{Grammar for meta-specifiers.}
	\label{fig:zilch-grammar-declarations-meta-grammar}
\end{figure}

\section{Modules}\label{sec:zilch-grammar-modules}

Modules allow grouping functions and types that are related to each other under a common namespace.
In Zilch, modules provide grouping, importing and visibility restrictions.

A Zilch module is declared according to the name and position of the file in the include path.
For example, if a file is named \verb|Internal.zc| in the directory \verb|Data/Something/A|, then it exports a module \verb|Data::Something::A::Internal|.

It can contain, in any order, many (possibly none) \texttt{import} statements (see Figure~\ref{fig:zilch-grammar-modules-importgrammar}) and any number of declarations as described in Section~\ref{sec:zilch-grammar-declarations}~``\nameref{sec:zilch-grammar-declarations}''.

A module $A$ may export another module $B$, meaning that anything imported from $B$ into $A$'s scope is exported by $A$.
If a plain function is aliased\footnote{Infix operators cannot be aliased because it would lead to many syntactical problems.} from the import of $B$ in $A$, the new name is exported by $A$ instead of the old one.
Operator fixities are exported only if their corresponding operators are also exported.
All imports are qualified, unless when \verb|open|ed.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\scalebox{.5}{
				\includegraphics[width=\linewidth]{zilch/modules/import}
			}\\
			\scalebox{.95}{
				\includegraphics[width=\linewidth]{zilch/modules/import-path}
			}
		}
	}

	\caption{Grammar for import statements.}
	\label{fig:zilch-grammar-modules-importgrammar}
\end{figure}

\chapter{Static semantics}\label{chap:zilch-staticsem}

Zilch is statically and strongly typed, meaning that types of expressions are checked at compile-time, and no implicit conversion are performed.
It also is type-infered, so there is no need to write the exact type of a function (unless in specific ambiguous states, e.g. with constraints).

The type system of Zilch is based off a quantitative dependent type system with non-cumulative universe polymorphism and algebraic effects.
In short, this means that types are allowed to be dependent on runtime values (which are not \texttt{@0}), and that the type \texttt{type l} has a single type which is \texttt{type (lsuc l)}.

This chapter will contain type inference rules accompanied by informal descriptions.
Some of the inference rules may be elided for simplicity, as writing them out would be either too cumbersome or difficult to understand.
In such case, the informal description will be more furnished to compensate.

\section{Multiplicities}\label{sec:zilch-staticsem-multiplicities}

The Quantitative Type Theory (QTT for short) relies on usage annotations called ``multiplicities'' to determine the status of a given computation.
The fragment $0,1,\omega$ is used to model these in Zilch, where:
\begin{itemize}
	\item $0$ is the multiplicity of erased expressions, that is expressions which are guaranteed to be fully evaluated at compile time and be completely stripped off the executable code;
	\item $1$ is the multiplicity of linear expressions, meaning that they can be referenced only once (as in Linear Logic);
	\item and $\omega$ which is the multiplicity for unrestricted values (which can be used either at compile time or at runtime).
\end{itemize}

There is a very important typing rule for multiplicities, as presented in figure~\ref{fig:zilch-staticsem-multiplicities-conv-typerules}, which relies on the relation $\leqslant$ defined in figure~\ref{fig:zilch-staticsem-multiplicities-partialorder}, allowing to specialise a multiplicity.
The $\cong$ relation embodies that two types are equivalent.

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\begin{prooftree}
			\hypo{\rho\in\{0, 1, \omega\}}
			\infer1{\rho\leqslant\omega}
		\end{prooftree}
		\hspace{1.5em}
		\begin{prooftree}
			\infer0{0\leqslant 0}
		\end{prooftree}
		\hspace{1.5em}
		\begin{prooftree}
			\infer0{1\leqslant 1}
		\end{prooftree}
	}

	\caption{Definition of the $\leqslant$ relation on multiplicities.}
	\label{fig:zilch-staticsem-multiplicities-partialorder}
\end{figure}

In the general sense, if $\pi \leqslant \rho$ then it means that $\pi$ is more specialised than $\rho$, or that the multiplicity $\pi$ can be used in place of $\rho$ at the specific point where this relation holds.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\begin{prooftree}
			\hypo{\TypeSequent{\Gamma}{e}{\rho}{\tau_1}{\epsilon}}
			\hypo{\tau_1\cong\tau_2}
			\hypo{\pi \leqslant \rho}
			\infer3[\textsc{[Type-Conv]}]{\TypeSequent{\Gamma}{e}{\pi}{\tau_2}{\epsilon}}
		\end{prooftree}
	}

	\caption{Type inference rules for multiplicity specialisation.}
	\label{fig:zilch-staticsem-multiplicities-conv-typerules}
\end{figure}

\section{Types, universes and effects}\label{sec:zilch-staticsem-types}

In Zilch, not only expressions have types, but types also do.
While this may sound a little bit complex, it in fact allows easily solving a few problems happening in some of other programming languages allowing generic programming:
\begin{itemize}
	\item A type may be passed partially applied to a function or a type;
	\item Type constraints live as inhabitants of other sets of types;
	      As such, constraints cannot be passed in place of other types, which would imply weird type system behaviours.
	\item A partially applied type (in opposition to a fully applied type, called a ``concrete kind'') cannot be given to a function requiring a concrete type.
\end{itemize}

Types of types are mainly organized in 4 categories:
\begin{itemize}
	\item Concrete types, which are denoted as \verb|type l| in Zilch, are types which are fully applied to arguments;
	\item Partially applied types (also called ``type constructors'') can only be applied to more arguments, but may yield any kind of type.
	      Just like functions at the expression level, type constructors are written using the arrow syntax \verb|_->_|;
	\item Effect types are special kinds of types which are only allowed to specify possible effects when computing a function.
	      Such types are grouped under the \verb|effect| kind.
\end{itemize}

Type inference rules are proposed in figure~\ref{fig:zilch-staticsem-types-universes-typerules} for type universes, and in figure~\ref{fig:zilch-staticsem-types-effects-typerules} for algebraic effects.

\begin{figure}[H]
	\centering

	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\tau}{0}{\Etype{\ell}}{\Etotal}}
				\infer2[\textsc{[Universe-Lift]}]{\TypeSequent{\scale{0}{\Gamma}}{\Ellift{\tau}}{0}{\Etype({\Elsuc{\ell}})}{\Etotal}}
			\end{prooftree}
			\\\vspace{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\infer1[\textsc{[Universe-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Etype{\ell}}{0}{\Etype({\Elsuc{\ell}})}{\Etotal}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\infer0[\textsc{[Universe-Var]}]{\TypeSequent{\scale{0}{\Gamma}, \ell :^0 \Elevel}{\ell}{0}{\Elevel}{\Etotal}}
			\end{prooftree}
			\\\vspace{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell_1}{0}{\Elevel}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell_2}{0}{\Elevel}{\Etotal}}
				\infer2[\textsc{[Universe-$\sqcup$]}]{\TypeSequent{\scale{0}{\Gamma}}{\Elmax{\ell_1}{\ell_2}}{0}{\Elevel}{\Etotal}}
			\end{prooftree}
			\\\vspace{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\infer1[\textsc{[Universe-Suc]}]{\TypeSequent{\scale{0}{\Gamma}}{\Elsuc{\ell}}{0}{\Elevel}{\Etotal}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\hypo{n$ is a natural$}
				\infer1[\textsc{[Universe-I]}]{\TypeSequent{\scale{0}{\Gamma}}{n}{0}{\Elevel}{\Etotal}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for type universes.}
	\label{fig:zilch-staticsem-types-universes-typerules}
\end{figure}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\tau_i}{0}{\Eeffect}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{e_j}{0}{\Eeffect}{\Etotal}}
				\infer2[\textsc{[Effect-Row]}]{\TypeSequent{\scale{0}{\Gamma}}{\Eeffectrow{\tau_i}{e_j}}{0}{\Eeffect}{\Etotal}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\infer0[\textsc{[Effect-Var]}]{\TypeSequent{\scale{0}{\Gamma}, e :^0 \Eeffect}{e}{0}{\Eeffect}{\Etotal}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for algebraic effects.}
	\label{fig:zilch-staticsem-types-effects-typerules}
\end{figure}

\section{Types of expressions}\label{sec:zilch-staticsem-exprs}

\subsection{Function types and lambda expressions}\label{subsec:zilch-staticsem-exprs-pi}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{A}{0}{\Etype \ell_1}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}, x :^0 \tau_A}{B}{0}{\Etype \ell_2}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\epsilon}{0}{\Eeffect}{\Etotal}}
				\infer3[\textsc{[$\rightarrow$-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Epi{x}{\rho}{A}{\epsilon}{B}}{0}{\Etype(\Elmax{\ell_1}{\ell_2})}{\Etotal}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{A}{0}{\Etype \ell_1}{\Etotal}}
				\hypo{\TypeSequent{\Gamma, x :^{\scale{\rho}{\pi}} A}{e}{\pi}{B}{\epsilon}}
				\hypo{\pi = 0 \Rightarrow \epsilon,\epsilon^\prime \equiv \Etotal}
				\infer3[\textsc{[$\rightarrow$-I$_1$]}]{\TypeSequent{\Gamma}{\Elam{x}{\rho}{A}{e}}{\pi}{\Epi{x}{\rho}{A}{\epsilon}{B}}{\epsilon^\prime}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma}{e}{\pi}{A}{\epsilon}}
				\hypo{\pi=0 \Rightarrow \epsilon^\prime \equiv \Etotal}
				\infer2[\textsc{[$\rightarrow$-I$_2$]}]{\TypeSequent{\Gamma}{\Edo{e}}{\pi}{\Efun{\omega\ \Eone}{\epsilon}{A}}{\epsilon^\prime}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma}{f}{\rho}{\Epi{y}{\pi}{A}{\epsilon}{B}}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{x}{0}{A}{\Etotal}}
				\hypo{\scale{\rho}{\pi} = 0}
				\hypo{\pi=0 \Rightarrow \epsilon \equiv \Etotal}
				\infer4[\textsc{[$\rightarrow$-E$_0$]}]{\TypeSequent{\Gamma}{\Eapp{f}{x}}{\pi}{\subst{B}{y}{x}}{\epsilon}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma_1}{f}{\rho}{\Epi{y}{\pi}{A}{\epsilon}{B}}{\epsilon^\prime}}
				\hypo{\TypeSequent{\Gamma_2}{x}{1}{A}{\epsilon^\second}}
				\infer2[\textsc{[$\rightarrow$-E$_1$]}]{\TypeSequent{\add{\Gamma_1}{\scale{\scale{\rho}{\pi}}{\Gamma_2}}}{\Eapp{f}{x}}{\rho}{\subst{B}{y}{x}}{\epsilon,\epsilon^\prime,\epsilon^\second}}
			\end{prooftree}
		}
	}

	\caption{Type inference rule for function types.}
	\label{fig:zilch-staticsem-exprs-pi-typerules}
\end{figure}

The rule \textsc{[$\rightarrow$-I]} may seem quite weird, as creating a lambda does not perform any effect (or it performs the effect $\Etotal$).
However, we require an effect $\epsilon^\prime$ to be performed by creating a lambda.
That way, we can also create lambdas in effectful contexts.
This could also be materialised by defining a subtyping relation $\subtype$ on effects where $\Etotal \subtype \epsilon$ and we can generalise the effect $\epsilon$ in the rule \textsc{[Type-Conv]} (in figure~\ref{fig:zilch-staticsem-multiplicities-conv-typerules}).
Also, any effect performed by \texttt{e} is lifted to the type of the lambda.

\subsection{Local bindings and effect handling}\label{subsec:zilch-staticsem-exprs-local}

The rules \textsc{[RecIn$_0$]} and \textsc{[RecIn$_1$]} rely on a predicate $\Eterminates{x}$ which returns whether the function $x$ is expected to always terminate or not.
It is important because we disallow erasing function calls which cannot be guaranteed to always terminate (to prevent from making the type-checker loop indefinitely).
In the case of non-erased terms, we use termination checking to put the builtin $\Ediv$\ effect on functions which may not terminate (which are not \textit{total}).

The predicate $\Eterminates{x}$ is left undefined as it is an implementation detail\footnote{There are many ways to detect termination, either through termination metrics as in ATS, or structural recursion as in Coq or Agda, or just never allow recursion, etc. There are many ways to handle this and none is objectively better than all others.}.
However it must be present to ensure consistency and non-looping static behaviors.

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{A}{0}{\Etype{\ell}}{\Etotal}}
				\hypo{\TypeSequent{\Gamma, x :^{\scale{\pi}{\rho}} A}{b}{\pi}{B}{\epsilon}}
				\infer[no rule, rule margin=1ex]2{\TypeSequent{\scale{0}{\Gamma}}{a}{0}{A}{\Etotal}\hspace{1.5em}%
				\scale{\pi}{\rho}=0\hspace{1.5em}%
				\pi = 0 \Rightarrow \epsilon \equiv \Etotal}
				\infer1[\textsc{[LetIn$_0$]}]{\TypeSequent{\Gamma}{\Eletin{x}{\rho}{A}{a}{b}}{\pi}{\subst{B}{x}{a}}{\epsilon}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma_1}}{A}{0}{\Etype{\ell}}{\Etotal}}
				\hypo{\TypeSequent{\Gamma_1, x :^{\scale{\pi}{\rho}} A}{b}{\pi}{B}{\epsilon}}
				\hypo{\TypeSequent{\Gamma_2}{a}{1}{A}{\epsilon^\prime}}
				\infer3[\textsc{[LetIn$_1$]}]{\TypeSequent{\add{\Gamma_1}{\scale{\scale{\pi}{\rho}}{\Gamma_2}}}{\Eletin{x}{\rho}{A}{a}{b}}{\pi}{\subst{B}{x}{a}}{\epsilon,\epsilon^\prime}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{A}{0}{\Etype{\ell}}{\Etotal}}
				\hypo{\TypeSequent{\Gamma, x :^{\scale{\pi}{\rho}} A}{b}{\pi}{B}{\epsilon}}
				\infer[no rule, rule margin=1ex]2{\TypeSequent{\scale{0}{\Gamma}, x :^0 A}{a}{0}{A}{\Etotal}\hspace{1.5em}%
				\scale{\pi}{\rho}=0\hspace{1.5em}%
				\pi = 0 \Rightarrow \epsilon \equiv \Etotal\hspace{1.5em}
				\Eterminates{x}}
				\infer1[\textsc{[RecIn$_0$]}]{\TypeSequent{\Gamma}{\Erecin{x}{\rho}{A}{a}{b}}{\pi}{\subst{B}{x}{a}}{\epsilon}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma_1}}{A}{0}{\Etype{\ell}}{\Etotal}}
				\hypo{\TypeSequent{\Gamma_1, x :^{\scale{\pi}{\rho}} A}{b}{\pi}{B}{\epsilon}}
				\infer[no rule, rule margin=1ex]2{\TypeSequent{\Gamma_2, x :^\omega A}{a}{1}{A}{\epsilon^\prime}\hspace{1.5em}%
				\neg \Eterminates{x} \Rightarrow \Ediv \in \epsilon^\prime}
				\infer1[\textsc{[RecIn$_1$]}]{\TypeSequent{\add{\Gamma_1}{\scale{\scale{\pi}{\rho}}{\Gamma_2}}}{\Erecin{x}{\rho}{A}{a}{b}}{\pi}{\subst{B}{x}{\Efix{x}{a}}}{\epsilon,\epsilon^\prime}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for \texttt{let} and \texttt{rec} local bindings.}
	\label{fig:zilch-staticsem-exprs-local-letin-typerules}
\end{figure}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{E(\mathsf{eff}) = \{\varsigma_1\ op_1, \varsigma_2\ op_2, \ldots, \varsigma_n\ op_n\}}
				\hypo{\TypeSequent{\scale{0}{\Gamma_0}}{\mathsf{eff}}{0}{\Eeffect}{\Etotal}}
				\infer[no rule, rule margin=1ex]2{\TypeSequent{\Gamma_0}{e}{1}{A}{\mathsf{eff}, \epsilon}\hspace{1.5em}%
				\TypeSequent{\scale{0}{\Gamma_i}}{op_i}{0}{\Efun{\overrightarrow{\rho_i\ A_i}}{\Eeffectrow{\mathsf{eff}}{}}{B_i}}{\Etotal}}
				\infer[no rule, rule margin=1ex]1{\TypeSequent{\Gamma_i, \Eresume :^{\varsigma_i} \Efun{B_i}{\epsilon_j}{A}, {x_i}_k :^{{\rho_i}_k} {A_i}_k }{e_i}{\pi}{A}{\epsilon_j}\hspace{1.5em}%
				\pi \neq 0}
				\infer1[\textsc{[Effect-E$_1$]}]{\TypeSequent{\add{\scale{\pi}{\Gamma_0}}{ \sum_i{\Gamma_i}}}{\Ewithhnd{\mathsf{eff}}{\varsigma_i}{op_i}{(\overrightarrow{x_i})}{e_i}{e}}{\pi}{A}{\epsilon,\epsilon_j}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma_1}{f}{1}{\Efun{(\Efun{\omega\ \Eone}{\Eeffectrow{\mathsf{eff}}{\epsilon}}{A})}{\epsilon}{A}}{\epsilon^\prime}}
				\hypo{\TypeSequent{\Gamma_2}{e}{1}{A}{\mathsf{eff}, \epsilon^\second}}
				\hypo{\pi \neq 0}
				\infer3[\textsc{[Effect-E$_2$]}]{\TypeSequent{\add{\Gamma_1}{\scale{\pi}{\Gamma_2}}}{\Ewith{f}{e}}{\pi}{A}{\epsilon,\epsilon^\prime,\epsilon^\second}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for local effect handlers.}
	\label{fig:zilch-staticsem-exprs-local-with-typerules}
\end{figure}

\subsection{Multiplicative and additive units}\label{subsec:zilch-staticsem-exprs-units}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\infer1[\textsc{$\mathbf{1}$-F}]{\TypeSequent{\scale{0}{\Gamma}}{\Eone}{0}{\Etype \ell}{\Etotal}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\infer1[\textsc{$\top$-F}]{\TypeSequent{\scale{0}{\Gamma}}{\Etop}{0}{\Etype \ell}{\Etotal}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\pi=0 \Rightarrow \epsilon \equiv \Etotal}
				\infer1[\textsc{[$\mathbf{1}$-I]}]{\TypeSequent{\Gamma}{\Emultunit}{\pi}{\Eone}{\epsilon}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\hypo{\pi=0 \Rightarrow \epsilon \equiv \Etotal}
				\infer1[\textsc{[$\top$-I]}]{\TypeSequent{\Gamma}{\Eaddunit}{\pi}{\Etop}{\epsilon}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma_1}{a}{\pi}{\Eone}{\epsilon}}
				\hypo{\TypeSequent{\Gamma_1, z :^0 \Eone}{B}{0}{\Etype \ell}{\Etotal}}
				\hypo{\TypeSequent{\Gamma_2}{b}{\pi}{B}{\epsilon^\prime}}
				\hypo{\pi=0 \Rightarrow \epsilon,\epsilon^\prime \equiv \Etotal}
				\infer4[\textsc{[$\mathbf{1}$-E]}]{\TypeSequent{\add{\Gamma_1}{\Gamma_2}}{\Emultunitelim{z}{\rho}{a}{b}}{\pi}{\subst{B}{z}{\Emultunit}}{\epsilon,\epsilon^\prime}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for multiplicative and additive units.}
	\label{fig:zilch-staticsem-exprs-units-typerules}
\end{figure}

\subsection{Multiplicative and additive pairs}\label{subsec:zilch-staticsem-exprs-pairs}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{A}{0}{\Etype \ell_1}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}, x :^0 \tau_A}{B}{0}{\Etype \ell_2}{\Etotal}}
				\infer2[\textsc{[$\otimes$-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Etensor{x}{\rho}{A}{B}}{0}{\Etype(\Elmax{\ell_1}{\ell_2})}{\Etotal}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{A}{0}{\Etype \ell_1}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}, x :^0 \tau_A}{B}{0}{\Etype \ell_2}{\Etotal}}
				\infer2[\textsc{[$\&$-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Eand{x}{A}{B}}{0}{\Etype(\Elmax{\ell_1}{\ell_2})}{\Etotal}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{a}{0}{A}{\Etotal}}
				\hypo{\TypeSequent{\Gamma}{b}{\pi}{\subst{B}{x}{a}}{\epsilon}}
				\hypo{\scale{\rho}{\pi}=0}
				\hypo{\pi=0 \Rightarrow \epsilon\equiv\Etotal}
				\infer4[\textsc{[$\otimes$-I$_0$]}]{\TypeSequent{\scale{0}{\Gamma}}{\Emultpair{a}{b}}{\pi}{\Etensor{x}{\rho}{A}{B}}{\epsilon}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma_1}{a}{1}{A}{\epsilon}}
				\hypo{\TypeSequent{\Gamma_2}{b}{\pi}{\subst{B}{x}{a}}{\epsilon^\prime}}
				\infer2[\textsc{[$\otimes$-I$_1$]}]{\TypeSequent{\add{\scale{\scale{\rho}{\pi}}{\Gamma_1}}{\Gamma_2}}{\Emultpair{a}{b}}{\pi}{\Etensor{x}{\rho}{A}{B}}{\epsilon,\epsilon^\prime}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma}{a}{\pi}{A}{\epsilon}}
				\hypo{\TypeSequent{\Gamma}{b}{\pi}{\subst{B}{x}{a}}{\epsilon^\prime}}
				\hypo{\pi=0 \Rightarrow \epsilon,\epsilon^\prime \equiv \Etotal}
				\infer3[\textsc{[$\&$-I]}]{\TypeSequent{\Gamma}{\Eaddpair{a}{b}}{\pi}{\Eand{x}{A}{B}}{\epsilon,\epsilon^\prime}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma_1}, z :^0 \Etensor{x}{\rho}{A}{B}}{C}{0}{\Etype \ell}{\Etotal}}
				\hypo{\TypeSequent{\Gamma_1}{m}{\pi}{\Etensor{x}{\rho}{A}{B}}{\epsilon}}
				\infer[no rule, rule margin=1ex]2{\TypeSequent{\Gamma_2, a :^{\scale{\scale{\varsigma}{\rho}}{\pi}} A, b :^{\scale{\varsigma}{\pi}} \subst{B}{x}{a}}{n}{\pi}{C}{\epsilon^\prime}\hspace{1.5em}%
				(\pi=0 \Rightarrow \epsilon,\epsilon^\prime \equiv \Etotal) \vee (\varsigma=0 \Rightarrow \epsilon \equiv \Etotal)}
				\infer1[\textsc{[$\otimes$-E]}]{\TypeSequent{\add{\scale{\varsigma}{\Gamma_1}}{\Gamma_2}}{\Emultpairelim{a}{b}{z}{\varsigma}{m}{n}}{\pi}{\subst{C}{z}{\Emultpair{a}{b}}}{\epsilon,\epsilon^\prime}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma}{e}{\pi}{\Eand{x}{A}{B}}{\epsilon}}
				\hypo{\pi=0 \Rightarrow \epsilon \equiv \Etotal}
				\infer2[\textsc{[$\&$-E$_1$]}]{\TypeSequent{\Gamma}{\Eaccess{e}{1}}{\pi}{A}{\epsilon}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma}{e}{\pi}{\Eand{x}{A}{B}}{\epsilon}}
				\hypo{\pi=0 \Rightarrow \epsilon \equiv \Etotal}
				\infer2[\textsc{[$\&$-E$_2$]}]{\TypeSequent{\Gamma}{\Eaccess{e}{2}}{\pi}{\subst{B}{x}{\Eaccess{e}{1}}}{\epsilon}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for multiplicative and additive pairs.}
	\label{fig:zilch-staticsem-exprs-pairs-typerules}
\end{figure}

\subsection{Booleans}\label{subsec:zilch-staticsem-exprs-booleans}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\infer1[\textsc{[bool-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Ebool}{0}{\Etype \ell}{\Etotal}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\infer0[\textsc{[bool-I$_1$]}]{\TypeSequent{\Gamma}{\Etrue}{\pi}{\Ebool}{\epsilon}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\infer0[\textsc{[bool-I$_2$]}]{\TypeSequent{\Gamma}{\Efalse}{\pi}{\Ebool}{\epsilon}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{c}{0}{\Ebool}{\Etotal}}
				\hypo{\TypeSequent{\Gamma}{t}{\pi}{A}{\epsilon}}
				\hypo{\TypeSequent{\Gamma}{e}{\pi}{B}{\epsilon^\prime}}
				\hypo{\pi=0 \Rightarrow \epsilon,\epsilon^\prime \equiv \Etotal}
				\infer4[\textsc{[bool-E$_0$]}]{\TypeSequent{\Gamma}{\Eifthenelse{c}{t}{e}}{\pi}{\Eifthenelse{c}{A}{B}}{\epsilon,\epsilon^\prime}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma_1}{c}{\rho}{\Ebool}{\epsilon}}
				\hypo{\TypeSequent{\Gamma_2}{t}{1}{A}{\epsilon^\prime}}
				\hypo{\TypeSequent{\Gamma_2}{e}{1}{A}{\epsilon^\second}}
				\hypo{\pi=0 \Rightarrow \epsilon,\epsilon^\prime,\epsilon^\second \equiv \Etotal}
				\infer4[\textsc{[bool-E$_1$]}]{\TypeSequent{\add{\Gamma_1}{\scale{\pi}{\Gamma_2}}}{\Eifthenelse{c}{t}{e}}{\pi}{A}{\epsilon,\epsilon^\prime,\epsilon^\second}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for booleans.}
	\label{fig:zilch-staticsem-exprs-booleans-typerules}
\end{figure}

\subsection{Atomic expressions}\label{subsec:zilch-staticsem-exprs-atoms}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\infer0[\textsc{[Var]}]{\TypeSequent{\Gamma, x :^\pi A}{x}{\pi}{A}{\epsilon}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for variables.}
	\label{fig:zilch-staticsem-exprs-atoms-variables-typerules}
\end{figure}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\infer1[\textsc{[Natural-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Eunsigned{N}}{0}{\Etype{\ell}}{\Etotal}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\infer1[\textsc{[Integer-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Esigned{N}}{0}{\Etype{\ell}}{\Etotal}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{n$ is a natural number$}
				\infer1[\textsc{[Natural-I]}]{\TypeSequent{\Gamma}{n}{\pi}{\Eunsigned{M}}{\epsilon}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\hypo{n$ is a natural number$}
				\infer1[\textsc{[Integer-I]}]{\TypeSequent{\Gamma}{\pm n}{\pi}{\Esigned{M}}{\epsilon}}
			\end{prooftree}

		}
	}

	\caption{Type inference rules for integral atoms.}
	\label{fig:zilch-staticsem-exprs-atoms-integers-typerules}
\end{figure}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\ell}{0}{\Elevel}{\Etotal}}
				\infer1[\textsc{[Char-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Echar}{0}{\Etype{\ell}}{\Etotal}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\hypo{c$ is a character$}
				\infer1[\textsc{[Char-I]}]{\TypeSequent{\Gamma}{c}{\pi}{\Echar}{\epsilon}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for character atoms.}
	\label{fig:zilch-staticsem-exprs-atoms-characters-typerules}
\end{figure}

\begin{figure}[H]
	\framebox[\textwidth][c]{
		\parbox{\textwidth}{
			\centering

			\begin{prooftree}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{A}{0}{\Etype{\ell}}{\Etotal}}
				\hypo{\TypeSequent{\scale{0}{\Gamma}}{\rho}{0}{\Eregion}{\Etotal}}
				\infer2[\textsc{[Ref-F]}]{\TypeSequent{\scale{0}{\Gamma}}{\Eref{A}{\rho}}{0}{\Etype{\ell}}{\Etotal}}
			\end{prooftree}
			\hspace{1.5em}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma}{p}{\pi}{\Eref{A}{\rho}}{\epsilon}}
				\infer1[\textsc{[Ref-E]}]{\TypeSequent{\Gamma}{\Ederef{p}}{\pi}{A}{\epsilon}}
			\end{prooftree}
			\\\vspace*{\baselineskip}
			\begin{prooftree}
				\hypo{\TypeSequent{\Gamma}{e}{\pi}{A}{\epsilon}}
				\infer1[\textsc{[Ref-I]}]{\TypeSequent{\Gamma}{\Emkref{e}}{\pi}{\Eref{A}{\rho}}{\epsilon}}
			\end{prooftree}
		}
	}

	\caption{Type inference rules for references.}
	\label{fig:zilch-staticsem-exprs-atoms-ptr-typerules}
\end{figure}

\section{Module semantics}\label{sec:zilch-staticsem-modules}

Let $I$ be a set of paths denoted as $\{ p_1, p_2, \ldots, p_n \}$ called the ``include path''.
Paths are compared after being normalized, meaning that \verb|.| and \verb|dir/..| are equal (they are both normalized to the current directory).

A Zilch module is identified from one of the roots in the include path.
For example, a file \verb|src/Language/X/Parser.zc| with the include path $\{ \text{src} \}$ will have \verb|Language::X::Parser| as a module name.

When importing a module into the current scope, several cases may arise:
\begin{itemize}
	\item The module name does not correspond to a file accessible from the include path.
	      In such case, an error must be thrown and compilation must be stopped.
	\item The module name corresponds to multiple files in the include path.
	      Handling this is left unspecified as several options are available.\footnote{One may choose to select an arbitrary file, or error out.}
	\item The module name corresponds to only one file in the include path.
\end{itemize}

One must be careful about importing non-module elements.
Because everything in Zilch is scoped, imports can also reference elements which are deeply nested within other elements (e.g. an \verb|enum| constructor).
For example, given the file \verb|A/B/C.zc| containing an \verb|public enum A := ...|, it is allowed to \verb|import A::B::C::A|.
As a result, import resolution becomes a little more difficult: the above case must hold for any path denoted by the import (at least one of \verb|A.zc|, \verb|A/B.zc|, \verb|A/B/C.zc|, \verb|A/B/C/A.zc| must exist).
If the import path is partially matched, the remaining part is considered to reference an arbitrarily deeply nested element, which must therefore exist in scope.
Note that only \verb|public| elements can be imported.

Imports are qualified by default.
This means that all imports do not populate the current scope, unless explicitly \verb|open|ed.
Imports can also be aliased, where an aliased qualified import simply populates another name.
When unqualified, an alias provides a qualified way of accessing the module's identifiers in case of scope conflict (when two imported modules have a common identifier).

Imported identifiers can also be aliased locally, only if they do not refer to operators.

\section{A few notes}\label{sec:zilch-staticsem-notes}

Static semantics are described for a subset of the Zilch programming language known as the ``core''.
The ``core'' is a dependently- and quantitatively- typed lambda calculus with effects and universe polymorphism where all functions have a single argument.

Although typing rules are described only for the ``core'', it is very easy to translate the surface language (Zilch) to the ``core''.
Just for the sake of comprehensiveness, it is assumed that mixfix expressions are already reduced to simple function applications (i.e. that given the mixfix operator \texttt{\_+\_}, \texttt{1 + 2} is translated into \texttt{\_+\_(1, 2)}).

\def\D#1{{\color{black}\mathcal{D}(}{\surface{#1}}{\color{black})}}
The translation from a surface CST $\surface{A}$ into a core AST $\core{B}$ is defined by the relation $\D{A} \equiv \core{B}$ as below.
Imports and meta-attributes may be handled any way.

\begin{description}[itemindent=0pt,left=0pt]
	\item[For expressions]
		\begin{align*}
			\D{\lambda() \Rightarrow e}                                             & \equiv \core{\D{\lambda(\omega\ \_ : \mathbf{1}) \Rightarrow e}}                                                                                 \\
			\D{\lambda(\overline{\rho\ x : A}) \Rightarrow e}                       & \equiv \core{\lambda(\rho_0\ x_0 : \D{A_0}) \Rightarrow \ldots \Rightarrow \lambda(\rho_n\ x_n : \D{A_n}) \Rightarrow \D{e}}                     \\
			\D{f(\overline{x})}                                                     & \equiv \core{\D{f}(\D{x_0})(\ldots)(\D{x_n})}                                                                                                    \\
			\D{() \to e}                                                            & \equiv \core{\D{(\omega\ \_ : \mathbf{1}) \to e}}                                                                                                \\
			\D{(\overline{\rho\ x : A}) \to e}                                      & \equiv \core{(\rho_0\ x_0 : \D{A_0}) \to \ldots \to (\rho_n\ x_n : \D{A_n}) \to \D{e}}                                                           \\
			\D{if\ c\ then\ t\ else\ e}                                             & \equiv \core{if\ \D{c}\ then\ \D{t}\ else\ \D{e}}                                                                                                \\
			\D{(\overline{\rho\ x : A}) \otimes B}                                  & \equiv \core{(\rho_0\ x_0 : \D{A_0}) \otimes \ldots \otimes (\rho_n\ x_n : \D{A_n}) \otimes \D{B}}                                               \\
			\D{()}                                                                  & \equiv \core{()}                                                                                                                                 \\
			\D{(e)}                                                                 & \equiv \core{\D{e}}                                                                                                                              \\
			\D{(x_0, x_1, \ldots, x_n)}                                             & \equiv \core{(\D{x_0}, (\D{x_1}, (\ldots, (\D{x_{n-1}}, \D{x_n})\ldots))}                                                                        \\
			\D{let\ (\overline{x}) \coloneqq e; f}                                  & \equiv \core{let\ (x_0, \__0) \coloneqq \D{e};\ldots; let\ (x_{n-1},x_n) \coloneqq \__{n-1}; \D{f}}                                              \\
			\D{(\overline{x : A}) \mathbin{\&} B}                                   & \equiv \core{(x_0 : \D{A_0}) \mathbin{\&} \ldots \mathbin{\&} (x_n : \D{A_n}) \mathbin{\&} \D{B}}                                                \\
			\D{\langle\rangle}                                                      & \equiv \core{\langle\rangle}                                                                                                                     \\
			\D{\langle e\rangle}                                                    & \equiv \core{\D{e}}                                                                                                                              \\
			\D{\langle x_0, x_1, \ldots, x_n\rangle}                                & \equiv \core{\langle\D{x_0}, \langle\D{x_1}, \langle\ldots, \langle\D{x_{n-1}}, \D{x_n}\rangle\ldots\rangle\rangle}                              \\
			\D{let\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B \coloneqq e; g} & \equiv \core{let\ \rho\ f : \D{(\overline{\sigma\ x : A}) \to \epsilon\ B} \coloneqq \D{\lambda(\overline{\sigma\ x : A}) \Rightarrow e}; \D{g}} \\
			\D{rec\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B \coloneqq e; g} & \equiv \core{rec\ \rho\ f : \D{(\overline{\sigma\ x : A}) \to \epsilon\ B} \coloneqq \D{\lambda(\overline{\sigma\ x : A}) \Rightarrow e}; \D{g}} \\
			% \D{let\ \rho\ x \coloneqq f(\overline{x}, \&a, \overline{y}); e}        & \equiv \core{\D{let\ \rho\ (a, x) \coloneqq f(\overline{x}, a, \overline{y}); e}}                                                                \\
			% TODO: change \& to something else
			\D{e}                                                                   & \equiv \core{e}                                                                                                                                  \\
		\end{align*}

	\item[For the top-level]
		\begin{align*}
			\D{let\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B \coloneqq e} & \equiv \core{let\ \rho\ f : \D{\overline{(\sigma\ x : A)} \to \epsilon\ B} \coloneqq \D{\lambda(\overline{\sigma\ x : A}) \Rightarrow e}} \\
			\D{rec\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B \coloneqq e} & \equiv \core{rec\ \rho\ f : \D{\overline{(\sigma\ x : A)} \to \epsilon\ B} \coloneqq \D{\lambda(\overline{\sigma\ x : A}) \Rightarrow e}} \\
			\D{val\ \rho\ f(\overline{\sigma\ x : A}) : \epsilon\ B}             & \equiv \core{val\ \rho\ f : (\sigma_0\ x_0 : \D{A_0}) \to \ldots \to (\sigma_n\ x_n : \D{A_n}) \to \epsilon\ \D{B}}                       \\
		\end{align*}
\end{description}

\let\D\undefined



\endgroup