trilogy / spec / src / syntax-and-semantics / index.tex

\section{Syntax and Semantics}
\label{sec:syntax}

As previously mentioned, grammars in this document are
\href{https://en.wikipedia.org/wiki/Parsing_expression_grammar}{PEGs},
albeit lacking in all syntax sugar.

In this section, terminals each refer to token types, though for tokens
with a single source text representation, their textual representation
is preferred for readability. The productions refer to nodes in the
abstract syntax tree, and are named as they are in the implementation
source code.

Following relevant blocks describing the syntax of \Trilogy{} code is some
approximation of a formalization of the semantics of that code, using some
loose understanding of the notation and rules of what might be natural
deduction, which I may or may not have learned briefly some years ago.
I am no expert, and if some expert ever sees this I will gladly accept any
corrections to these notes, as I am sure they will be conflicting themselves
in more than a few places.

Seeing as I am not an expert, some symbols used in potentially non-
standard ways in the following documentation are summarized here.
Some are further formalized later.

\begin{itemize}
    \item $\Gamma :> \Phi$ --- Extends from, as a scope. Names looked up in the
    context $\Phi$ will search $\Phi$ first; if not found, the context $\Gamma$
    is searched. New names bound are bound in $\Phi$ without affecting $\Gamma$.
    Names which are rebound (e.g.\ in assignment) are rebound in the scope in
    which they are found.
    \item $P = E$ --- Unifies, via the pattern unification algorithm. Given the
    pattern $P$ and value $E$, find values for the free variables in $P$ such that
    that $P$ and $E$ represent the same value.
    \item $a := P$ --- Declares, as a name. $P$ is a pattern and $a$ is a name
    bound by that pattern. Patterns often declare more than one name.
    \item $\text{read}(\sigma)$ --- Read, as a file. $\sigma$ is a String which is interpreted
    as a URL, and $\text{read}(\sigma)$ is the contents of the file located by that URL.
    \item $e \in E$ --- Is an element of, via iteration. The value $E$ is a value
    which can be converted to an Iterator. Each $e$ is an element of that iterator.
    \item $X \Rightarrow \Phi$ --- Continues execution in context. After evaluation
    of the code $X$, the evaluation of the program continues at least once. Due to
    branching, there may be multiple executions remaining at this time. The
    continuing context of the program in each of these branches is denoted as
    $\Phi$.
    \item $X : \top$ --- Continues execution. $\Gamma\vdash X : \top$ could be
    seen as equivalent to $\Gamma \vdash X \Rightarrow \Gamma$, in that execution
    continues, possibly more than once, but without modifying the context.
    \item $X : \bot$ --- Ends execution. After evaluation of the code $X$,
    no further code is executed. This may be due to failed branching (fizzling),
    or as a result of certain control flow (e.g. \kw{return}).
    \item $X : \tau$ --- Is of type. More specifically than execution, a value may
    be of a particular type. This is treated similarly to $\top$ in terms of
    execution continuing, possibly more than once, but we have additional
    information about the type of the value that the expression $X$ evaluated to.
    \item $X \vartriangle \eta$ --- Yields, as an effect. The expression $X$ causes
    an effect $\eta$ to be yielded. That effect will be handled later.
    \item $P\ \triangleleft\ B$ --- Inverts with, as a handler. A construct that is
    held in scope, when an effect matching $P$ is yielded, $B$ is used as a handler.
    \item $X\ \triangledown\ \tau$ --- Resumes with. The expression $X$ causes
    the recently yielded effect to resume with a value of type $\tau$.
    \item $X\ \triangleright\ \tau$ --- Cancels to. The expression $X$ causes the
    continuation of the recently yielded effect to be cancelled, resuming execution
    from its limit, which evaluates to a value of type $\tau$.
    \item $\text{addr}(X)$ --- Address of, as an instance. The address of the value
    of the evaluated value of $X$ is used, rather than the actual value of $X$
    itself. Values of reference type have such addresses, values of structural type
    do not, but you could imagine that every distinct value of structural type has
    its own unique pseudo-address that is used equivalently.
\end{itemize}

\subsection{Trilogy}

While the specifics of most of the executable code in \Trilogy{} are separated into
the three sublanguages, the non-executable parts of the language are considered
to be part of \Trilogy{} as a whole.

\subsubsection{Whitespace}

Between any two tokens may be any number of comment nodes. Additionally,
any whitespace (including line breaks) may occur between any two tokens
without issue. In certain marked cases, however, line breaks are required
as a statement terminator; in such cases, the line break is always interpreted
as a statement terminator, and not as meaningless whitespace.

The required end of line rule is formalized as follows:

\begin{bnf*}
    \bnfprod{EOL}{
        \bnfts{EndOfLine}\bnfor
        \bnfts{CommentLine}\bnfor
        \bnfts{CommentBlock}
    }
\end{bnf*}

Documentation comments, though they include line breaks, do not count as a line
break because when attached to a declaration, as seen in the next section, they
too require being placed on a separate line from any previous definition.

\subsubsection{The Document}

The top level of a \Trilogy{} file is not considered to be written in any
of the sublanguages. This section of the program may only contain definitions.

A \Trilogy{} document \emph{should} end with a final line break, but files
without such a final line break may be accepted (with warning). This line break
is not represented in the grammar, but should be checked nonetheless.

As a notable exception, rule~\ref{bnf:empty} indicates that a truly empty
file \emph{is} accepted, regardless of the fact that it does not end with
a line break.

A byte order mark \emph{may} be accepted (with warning) at the start of
the file. It is optional to implement rule~\ref{bnf:bom}.

Interestingly, since documentation comments have specfic meaning in relation
to defined items, they are only permitted in some locations and are included
in the resulting syntax tree. These comments have no meaning to the program
as it runs, but may be used by other tools which are likely to be based on the
syntax tree, so having the documentation inside is simply useful.

\begin{bnf}
    \bnfprod*{Document}{
        \bnfpn{Preamble}
        \bnfsp
        \bnfpn{InnerDocumentation}
    } \\
    \bnfmore{
        \bnfpn{Definitions}
        \bnfsp
        \bnfpn{Postamble}
        \bnfor
    } \\
    \bnfmore{\label{bnf:empty}\bnfpn{Preamble}\bnfsp\bnfts{EndOfFile}} \\
    \bnfprod*{Preamble}{\bnfts{StartOfFile}\bnfor} \\
    \bnfmore{
        \label{bnf:bom}
        \bnfts{StartOfFile}
        \bnfsp
        \bnfts{ByteOrderMark}
    } \\
    \bnfprod*{Postamble}{\bnfts{EndOfFile}} \\
    \bnfprod*{InnerDocumentation}{
        \bnfpn{DocInner}
        \bnfsp
        \bnfpn{InnerDocumentation}
        \bnfor
        \bnfes
    } \\
    \bnfprod*{Definitions}{
        \bnfpn{Definition}
        \bnfsp
        \bnfpn{EOL}
        \bnfsp
        \bnfpn{Definitions}
        \bnfor
        \bnfpn{Definition}
    } \\
    \bnfprod*{Definition}{
        \bnfpn{OuterDocumentation}
        \bnfsp
        \bnfpn{DefinitionItem}
    } \\
    \bnfprod*{OuterDocumentation}{
        \bnfpn{DocOuter}
        \bnfsp
        \bnfpn{OuterDocumentation}
        \bnfor
        \bnfes
    } \\
    \bnfprod*{DefinitionItem}{
        \bnfpn{TypeDefinition}\bnfor
        \bnfpn{FunctionDefinition}\bnfor
    } \\
    \bnfmore*{
        \bnfpn{ProcedureDefinition}\bnfor
        \bnfpn{RuleDefinition}\bnfor
    } \\
    \bnfmore*{
        \bnfpn{SlotDefinition}\bnfor
    } \\
    \bnfmore*{
        \bnfpn{ExternProcedureDefinition}\bnfor
    } \\
    \bnfmore*{
        \bnfpn{ExternTypeDefinition}\bnfor
    } \\
    \bnfmore*{
        \bnfpn{Test}\bnfor
        \bnfpn{Import}\bnfor
        \bnfpn{Export}
    }
\end{bnf}

\subsubsection{Modules}

In \Trilogy{}, modules are defined using the \kw{type} keyword, and may someday
be expanded upon in ways that make them more similar to existing type systems.

Modules act as containers for definitions, including procedures, functions, rules,
and further submodules. Every \Trilogy{} document is implicitly an anonymous
module, meaning a document may export any of its defined items, and may be
imported by other modules that wish to make use of those definitions. Any item
defined at the top level of a module may be exported: procedures, functions,
rules, and submodules.

The \Trilogy{} module system is modelled after that of OCaml: modules may
be defined as functions which accept one or more values as parameters
to generate a new module. Unlike in OCaml, such modules functions are \emph{generative}:
if a module function is applied to the same arguments multiple times, it will
generate a distinct module. At this time, a document cannot specify parameters,
so such function modules may only be defined as a local submodule within some
existing module.

\begin{bnf*}
    \bnfprod{TypeDefinition}{
        \bnfts{\kw{type}}
        \bnfsp
        \bnfpn{TypeHead}
        \bnfsp
        \bnfts{\{}
        \bnfsp
        \bnfpn{Definitions}
        \bnfsp
        \bnfts{\}}
    } \\
    \bnfprod{TypeHead}{
        \bnfpn{Identifier}
        \bnfsp
        \bnfpn{TypeParameters}
    } \\
    \bnfprod{TypeParameters}{
        \bnfpn{Identifier}
        \bnfsp
        \bnfpn{TypeParameters}
        \bnfor
        \bnfes
    }
\end{bnf*}

\subsubsection{Imports and Exports}

Imported documents, defined using the \kw{import}-\texttt{String} construct
are resolved as documents located via the canonical absolute URL designated
by the (potentially relative) path \texttt{String} in rule~\ref{bnf:import}.
If two external module definitions paths resolve to the same canonical absolute
URL, those two modules will be considered identical, despite being ``defined''
in two places in the source code. The full details of the path resolution
algorithm are defined in \S\ref{sec:module-resolution}.

Modules can also be imported from using the \kw{import}-\texttt{Expression}
form, working in much the same way but for modules that are defined locally or
require passing parameters. The expression in this case must be a constant
expression.

\begin{bnf}
    \bnfprod{Import}{
        \label{bnf:import}
        \bnfts{\kw{import}}
        \bnfsp
        \bnfpn{String}
        \bnfsp
        \bnfpn{ImportAs}
        \bnfsp
        \bnfpn{ImportUse}
        \bnfor
    } \\
    \bnfmore*{
        \bnfts{\kw{import}}
        \bnfsp
        \bnfpn{Expression}
        \bnfsp
        \bnfpn{ImportAs}
        \bnfsp
        \bnfpn{ImportUse}
    } \\
    \bnfprod*{ImportUse}{
        \bnfts{\kw{use}}
        \bnfsp
        \bnfpn{NameList}
        \bnfor
        \bnfes
    } \\
    \bnfprod*{ImportAs}{
        \bnfts{\kw{as}}
        \bnfsp
        \bnfpn{Identifier}
        \bnfor
        \bnfes
    } \\
    \bnfprod*{Export}{
        \bnfts{\kw{export}}
        \bnfsp
        \bnfpn{NameList}
    } \\
    \bnfprod*{NameList}{
        \bnfpn{Name}
        \bnfsp
        \bnfts{,}
        \bnfsp
        \bnfpn{NameList}
        \bnfor
        \bnfpn{Name}
        \bnfor
        \bnfes
    } \\
    \bnfprod*{Name}{
        \bnfpn{Identifier}
        \bnfor
        \bnfpn{Identifier}
        \bnfsp
        \bnfts{\kw{as}}
        \bnfsp
        \bnfpn{Identifier}
    }
\end{bnf}

A \kw{type} definition puts into scope a namespace in which all \kw{export}ed
definitions contained within the module may be accessed. An \kw{import}-\kw{as}
puts such a namespace defined externally into scope, while the \kw{use} list
exposes the \kw{export}ed members into the current module's scope directly.
Otherwise, such members would need to be accessed using the module access
operator (\S\ref{sec:module-access}).

When a module is defined as a submodule (directly in the same file as its parent
module), the definitions within the module may access all definitions (including
private definitions) of the containing module. The reverse is not true; the
private members of a submodule remain private unless exported. Modules defined
externally also may not access members of the module in which they are declared.

\begin{prooftree}
    \AxiomC{$\Gamma,m_{1\hdots n},\Phi \vdash p$}
    \AxiomC{$\kw{type}\ m\ m_{1\hdots n}\ \block{K}$}
    \AxiomC{$K \Rightarrow \kw{export}\ p$}
    \LeftLabel{Export}
    \TrinaryInfC{$\Gamma \vdash m\ \text{exports}\ p$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\Phi \vdash p$}
    \AxiomC{$\kw{import}\ \sigma\ \kw{as}\ m$}
    \AxiomC{$\text{read}(\sigma) \Rightarrow \kw{export}\ p$}
    \LeftLabel{External Module}
    \TrinaryInfC{$\Gamma \vdash m\ \text{exports}\ p$}
\end{prooftree}

\begin{prooftree}
    \AxiomC{$\Phi \vdash p$}
    \AxiomC{$\Gamma \vdash m\ \text{exports}\ p$}
    \AxiomC{$\kw{import}\ m\ \kw{use}\ p$}
    \LeftLabel{Use}
    \TrinaryInfC{$\Gamma \vdash p$}
\end{prooftree}

\subsubsection{Slots}

Slots are the most basic type of definition, consisting of a name and an expression
to bind as the value for that name. The expression is evaluated once, at the time the
module in which the slot is declared is instantiated.

Slots may be declared as mutable, allowing the value in the slot to be reassigned later.

\begin{bnf*}
    \bnfprod{SlotDefinition}{
        \bnfts{\kw{slot}}
        \bnfsp
        \bnfpn{Identifier}
        \bnfsp
        \bnfts{=}
        \bnfsp
        \bnfpn{Expression}
        \bnfor
    } \\
    \bnfmore{
        \bnfts{\kw{slot}}
        \bnfsp
        \bnfts{\kw{mut}}
        \bnfsp
        \bnfpn{Identifier}
        \bnfsp
        \bnfts{=}
        \bnfsp
        \bnfpn{Expression}
    }
\end{bnf*}

\begin{prooftree}
    \AxiomC{$\Gamma \vdash E : \tau$}
    \AxiomC{$\kw{const}\ k\ \texttt{=}\ E$}
    \LeftLabel{Slot}
    \BinaryInfC{$\Gamma \vdash k : \tau$}
\end{prooftree}

Though there is no restriction on what value can be stored in a slot, the initial value
expression must be a valid ``constant expression''. Constant expressions may not involve
effect handlers, function calls, procedure calls, or comprehensions as those may perform
side effects which are not permitted at constant time. Only literals, basic operators, module
applications, module lookups may occur. References to other constants are also permitted, as
long as they do not cause a circular self-reference.

\subsubsection{Definitions}

The other types of definitions each hand off to their respective child
languages.

\begin{bnf*}
    \bnfprod{ProcedureDefinition}{
        \bnfts{\kw{proc}}
        \bnfsp
        \bnfpn{ProcedureHead}
        \bnfsp
        \bnfts{\{}
        \bnfsp
        \bnfpn{ProcedureBody}
        \bnfsp
        \bnfts{\}}
    } \\
    \bnfprod{FunctionDefinition}{
        \bnfts{\kw{func}}
        \bnfsp
        \bnfpn{FunctionHead}
        \bnfsp
        \bnfts{=}
        \bnfsp
        \bnfpn{FunctionBody}
    } \\
    \bnfprod{RuleDefinition}{\bnfts{\kw{rule}}\bnfsp\bnfpn{RuleHead}\bnfor} \\
    \bnfmore{\bnfts{\kw{rule}}\bnfsp\bnfpn{RuleHead}\bnfsp{\op{<-}}\bnfsp\bnfpn{RuleBody}}
\end{bnf*}

For name resolution purposes, defintions of all types are stored in the same
scope. For example, a procedure and a function defined in the same module may
not have the same name.

\subsubsection{External Definitions}

\begin{bnf*}
    \bnfprod{ExternTypeDefinition}{
        \bnfts{\kw{extern}}
        \bnfsp
        \bnfpn{String}
        \bnfsp
        \bnfts{\kw{type}}
        \bnfsp
        \bnfpn{TypeHead}
        \bnfsp
    } \\
    \bnfmore{
        \bnfts{\{}
        \bnfsp
        \bnfpn{ExternDefinitions}
        \bnfsp
        \bnfts{\}}
    } \\
    \bnfprod{ExternProcedureDefinition}{
        \bnfts{\kw{extern}}
        \bnfsp
        \bnfts{\kw{proc}}
        \bnfsp
        \bnfpn{ProcedureHead}
        \bnfsp
    } \\
    \bnfprod{ExternDefinitions}{
        \bnfpn{ExternDefinition}
        \bnfsp
        \bnfpn{ExternDefinitions}
        \bnfor
        \bnfes
    } \\
    \bnfprod{ExternDefinition}{
        \bnfpn{ExternProcedureDefinition}
    }
\end{bnf*}

Worth noting is the use of the \kw{extern} keyword: a type or procedure can be declared as
external indicating that it is not implemented within the current file but will be
available at compilation or link time from some externally provided native library.
The string following the \kw{extern} keyword names the calling convention by which the
externally defined function is to be called. Valid options are \texttt{"c"} or \texttt{"trilogy"}.

At this time, it is likely incorrect to use the \kw{extern} keyword in any user program,
but it is frequently used within the core library.

\subimport{law/}{index.tex}

\subimport{prose/}{index.tex}

\subimport{poetry/}{index.tex}

\subimport{effects/}{index.tex}

\subimport{tests/}{index.tex}