<commit_before>\lstMakeShortInline[keepspaces,basicstyle=\small\ttfamily]@
\section{Extensions}

\subsection{Algebraic Data Types}

Algebraic Data Types are a staple of functional programming and fit nicely
in our paradigm. Indeed, it is sufficient to check that the kinds of constructors
are strictly less than the kind of the datatype.
For instance, it is allowed to define a linear datatype containing unrestricted
parts.
On the contrary, it is forbidden to include affine elements in an unrestricted
datatype.
Here is the definition of a linear lists. The objects inside the list do not have to be linear.

\begin{lstlisting}
type ('a : 'k) llist : lin = Nil | Cons of ('a * 'a llist)
\end{lstlisting}

This extension is implemented in our prototype.

\subsection{Ad-hoc polymorphism and borrows}

In our formalization, we use two operators, $\borrow{x}$ and $\reborrow{x}$ to
distinguish between borrows and borrows of borrows.
Such a distinction is inconvenient for programming.
Using typeclass-like mechanisms, we can replace these operators
by a single one, $\borrow{x}$, which expects $x$ to be @Borrowable@ and
would then desugar to the more precise operators.
A similar solution is used in Rust through the @Borrow@ and @Defer@
traits.
It also allows method calls on objects without
explicit borrows, such as @foo.len()@ where len expects a shared borrow.

Ad-hoc polymorphism fits nicely in the framework of constrained
types and would preserve all the good properties of our language such
as principal type inference. Its soundness is orthogonal to linear types
and has been explored in the literature~\citep{DBLP:journals/scp/Jones94}.

\subsection{Non lexical lifetimes}

A recent important addition to Rust in the notion of ``non-lexical lifetimes''.
It allows code where borrowing doesn't follow
lexical scoping:

\begin{lstlisting}
let a = &x in
f a;
g (&!x)
\end{lstlisting}

Such patterns are dynamically safe, since $a$ is not used after
the second line.
Non-lexical lifetimes handles such patterns by ``removing'' the instructions
that do not mention $a$ from its region, here the last one.
%
In \lang, regions are purely lexical and marked by the
expressions $\region{b}{e}$.
During inference, region typing is only done when *existing* the region:
we modify the usage environment and introduce a kind constraint to prevent
escaping.

We can thus replace the lexical region by
an annotation on each subexpression indicating which borrowing it is associated
to. When exploring a subexpression, we compare the annotations, and automatically
apply the $\textsc{Region}$ rule when they differ.
%
This is equivalent to inlining the $\textsc{Region}$ rule in all the other
rules.

On the program above, the first two line will be annotated
to be ``in the region associated with @&x@'', but the last line will not.
When typing the sequence, since the annotations are different, we will apply
the region rule to the right hand side.

\lstDeleteShortInline@

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:<commit_msg>cosmetics<commit_after>\lstMakeShortInline[keepspaces,basicstyle=\small\ttfamily]@
\section{Extensions}

\subsection{Algebraic Data Types}

Algebraic data types are a staple of functional programming and fit nicely
in our paradigm. Indeed, it is sufficient to check that the kinds of constructors
are strictly less than the kind of the datatype.
For instance, we may define a linear datatype containing unrestricted
parts.
On the contrary, it is forbidden to include affine elements in an unrestricted
datatype.
Here is the definition of a linear lists. The objects inside the list do not have to be linear.

\begin{lstlisting}
type ('a : 'k) llist : lin = Nil | Cons of ('a * 'a llist)
\end{lstlisting}

This extension is implemented in our prototype.

\subsection{Ad-hoc Polymorphism and Borrows}

In our formalization, we use two operators, $\borrow{x}$ and $\reborrow{x}$ to
distinguish between borrows and borrows of borrows.
Such a distinction is inconvenient for programming.
Using a typeclass-like mechanism, we can replace these operators
by a single overloaded operator, $\borrow{x}$, which expects $x$ to be @Borrowable@ and
would then desugar to the more precise operators.
A similar solution is used in Rust through the @Borrow@ and @Defer@
traits.
This approach also enables method calls on objects without
explicit borrows, such as @foo.len()@ where len expects a shared borrow.

Ad-hoc polymorphism fits nicely in the framework of constrained
types and preserves all properties of our language such
as principal type inference. Its soundness is orthogonal to linear types
and has been explored in the literature~\citep{DBLP:journals/scp/Jones94}.

\subsection{Non-Lexical Lifetimes}

A recent important addition to Rust is the notion of non-lexical lifetimes.
With this feature code is acceptable even if borrowing does not respect
lexical scoping as in this example:

\begin{lstlisting}
let a = &x in
f a;
g (&!x)
\end{lstlisting}

Patterns like this one are dynamically safe because $a$ is not used after
the second line.
Non-lexical lifetimes handle such patterns by removing expressions
that do not mention $a$ from its region; in this example,  the
expression on the last line.
%
In \lang, regions are purely lexical and marked by the
expression $\region{b}{e}$.
During inference, region typing is only done when exiting the region:
we modify the usage environment and introduce a kind constraint to prevent
escaping.

We can thus replace the lexical region by
an annotation on each subexpression indicating which borrowing it is associated
to. When exploring a subexpression, we compare the annotations, and automatically
apply the $\textsc{Region}$ rule when they differ.
%
This approach is equivalent to inlining the $\textsc{Region}$ rule in all the other
rules.

Applied to the program above, only the first two lines would be annotated
to be ``in the region associated with @&x@'', but not the last line.
When typing the sequence, since the annotations are different, we will apply
the region rule to the right hand side.

\lstDeleteShortInline@

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
{'fraction_non_alphanumeric': 0.06392251815980629, 'fraction_numerical': 0.000645682001614205, 'mean_word_length': 4.850802644003777, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2186387', 'n_tokens_mistral': 1713, 'n_tokens_neox': 1607, 'n_words': 897}