From ea5ccc57c6fafe801f88798f86ab45b5b6033c2b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jasper=20Clemens=20Gr=C3=A4flich?= <jasper.graeflich@ptb.de>
Date: Fri, 12 Aug 2022 16:05:21 +0200
Subject: [PATCH] Begin 1.2.2
---
preamble.tex | 1 +
thesis/1-introduction.tex | 121 ++++++++++++++++++++++++++++++++++----
thesis/thesis.pdf | 4 +-
3 files changed, 114 insertions(+), 12 deletions(-)
diff --git a/preamble.tex b/preamble.tex
index a32c2f5..8c2183b 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -124,6 +124,7 @@ morekeywords=[2]{bool,i8,i16,i32,i64,i128,isize,u8,u16,u32,u64,u128,usize,f32,f6
\usepackage{mathtools}
\usepackage{amssymb}
\usepackage{unicode-math}
+\usepackage{braket} % \Set macro
%%%
% Graphics
diff --git a/thesis/1-introduction.tex b/thesis/1-introduction.tex
index f3fd6a9..6e33fbf 100644
--- a/thesis/1-introduction.tex
+++ b/thesis/1-introduction.tex
@@ -478,7 +478,7 @@ This pattern—calling a method with an exclusive reference but also using share
Right now, a \ac{TPB} may only happen in a few specific places, namely when calling a method with \inline{&mut self} as first argument and with assignment operators (\inline{+=}, \inline{*=}, …), and the other references can only be shared. There are several ways in which the requirements can be relaxed and which are discussed in the RFC and Issue \#49434\footnote{\url{https://github.com/rust-lang/rust/issues/49434}}.
-Currently, the only place an exclusive reference is allowed is in the \inline{&mut self} position. This means that it is not possible to use an exclusive reference twice, and a reborrow is also not possible because the references have no names. One could relax this and allow exclusive references everywhere, and also mix shared and exclusive references. This poses the difficulty that a shared reference (or one during reservation) can observe change. Resolving this makes the model more complicated.
+Currently, the only place an exclusive reference is allowed is in \inline{&mut self} position. This means that it is not possible to use an exclusive reference twice, and a reborrow is also not possible because the references have no names. One could relax this and allow exclusive references everywhere, and also mix shared and exclusive references. This poses the difficulty that a shared reference (or one during reservation) can observe change. Resolving this makes the model more complicated.
In a similar vein, \ac{TPB} could be expanded to all function calls or even in inline code, as shown in \autoref{lst:inline-tpb}. Here, creating a shared reference is not allowed because an exclusive one already exists and is live. With generalized \ac{TPB} it would be okay, though, since \inline{xm} is only in reservation phase at that point.
@@ -633,12 +633,104 @@ In this section, we will focus on two related approaches of specifying contracts
\item Higher-order contracts (\href{https://www2.ccs.neu.edu/racket/pubs/icfp2002-ff.pdf}{Findler, Felleisen})
\item Loop invariants
\end{enumerate}
+
\subsection{Refinement Types}
-\begin{enumerate}
- \item Independent Refinement Types
- \item Dependent Refinement Types/Refined Function Types
- \item Refinement Types are “first-classâ€
-\end{enumerate}
+
+Since the inception of set theory, mathematicians used \emph{set comprehension} to build sets. For example,
+
+\[
+ \Set{ n | n \text{ is a prime number}}
+\]
+
+\noindent denotes the set of all prime numbers. On the left-hand side of the $|$ is a comprehension variable and on the right-hand side is a predicate. The above is an example of \emph{unrestricted comprehension} because $n$ can stand for any mathematical object. Allowing unrestricted comprehension leads to Russel’s paradox, though, which is why it is not used in modern mathematics anymore. There is a weaker version of comprehension which works well, \emph{restricted comprehension}. In it, the variable has to be restricted to a set, like the following:
+
+\[
+ \Set{ n ∈ ℕ | n \text{ is a prime number}}
+\]
+
+\noindent This means that for every set $X$ and every predicate $P$,
+
+\[
+ \Set{x ∈ X | P(x)} ⊆ X
+\]
+
+\noindent which circumvents the paradox. \emph{Refinement types} are the type theoretic analogue to restricted comprehension. Some programming languages allow for refinement types. For example, in the Lean theorem prover, the introductory example would translate to
+
+\begin{lstlisting}
+{ n : nat // prime n }
+-- Syntactic sugar for:
+subtype nat prime
+\end{lstlisting}
+
+\inline{subtype} is a type constructor, that is a generic type, with two arguments. The first argument \inline{nat} is a type, but the second argument \inline{prime} is a value of function type. Rust has limited support for types depending on values with \emph{const generics}, but it does not support functions as const generics, which means that refinement types can’t be implemented in Rust this way.\todo{More on full dependent types, Pi and Sigma types, lambda cube?} There have been proposals for introducing more const generic capabilities to Rust\footnote{\url{https://github.com/ticki/rfcs/blob/pi-types/text/0000-pi-types.md}}, but they are put into cold storage indefinitely. We can still imagine what the equivalent Rust code would be if it could be written:
+
+\begin{lstlisting}[language=Rust]
+struct Prop<const B: Bool>;
+
+impl<const B: bool> Prop<B> {
+ const fn new() -> Self {
+ if B {
+ Self
+ } else {
+ panic!()
+ }
+ }
+}
+
+struct Subtype<T, const pred: fn(T) -> bool> {
+ val: T,
+ proof: Prop<pred(val)>
+}
+
+impl<T, const pred: fn(T) -> bool> Subtype<T, pred> {
+ const fn new(val: T) -> Self {
+ Self {
+ val,
+ proof: Prop::new::<pred(val)>()
+ }
+ }
+}
+
+// Also implement `Deref` and `DerefMut` so that a
+// `Subtype<T, pred>` can be used in any place where a
+// `T` is expected.
+
+\end{lstlisting}
+
+\noindent\inline{Prop} is a helper type which can only be created from a true value. We need this so that we can proof that \inline{val} makes \inline{prop} true. This would now allow us to create constants that have certain proven properties like in \autoref{lst:proven-const}.
+
+\begin{lstlisting}[language=Rust, caption={Constants with proven properties}, label={lst:proven-const}]
+const PRIME: Subtype<i32, is_prime> = Subtype::new(17);
+const SMALL: Subtype<u32, |x| x <= 255> = Subtype::new(9);
+\end{lstlisting}
+
+\noindent Because this is cumbersome, it would also be nice to extend the syntax for easier definition of a refinement type and let the compiler automatically insert the \inline{Subtype::new}.
+
+\begin{lstlisting}[language=Rust, caption={Constants with proven properties}, label={lst:proven-const-pretty}]
+const PRIME: Subtype where is_prime = 17;
+const SMALL: Subtype where |x| x <= 255 = 9;
+\end{lstlisting}
+
+\noindent Refinements could of course only be checked at compiletime for constants. If a user wants to create a runtime value, the checks are also at runtime.
+
+\subsubsection{Refinement Types in Functions}
+
+In the previous example, the predicate only took one input, namely the comprehension variable itself. And as long as only simple types are refined, this is the only possibility. But refinement types really shine when they depend on multiple inputs. The prime example is a function concatenating two arrays:
+
+\begin{lstlisting}[language=Rust, caption={Concatenate two arrays, with a deprendent output type}, label={lst:concat-refined}]
+fn concat<T, const N: usize, const M: usize>(
+ first: &[T; N],
+ second: &[T; M],
+) -> [T; N + M] {
+ // ...
+}
+\end{lstlisting}
+
+\noindent Here, the type of the return value depends on the generic values of the inputs. This, again, only works if \inline{N} and \inline{M} are known at compile time.
+
+\todo[inline]{Runtime dependent function (e. g. reverse?)}
+\todo[inline]{Intersection types}
+
\subsection{Liquid Types and SMT Solving}
\begin{enumerate}
\item Refinement Types are not decidable
@@ -647,7 +739,7 @@ In this section, we will focus on two related approaches of specifying contracts
\item Liquid Types = $\{ T : \text{RefinementType } | \text{ decidable } T \}$
\item SMT-LIB2 and Z3
\end{enumerate}
-\subsection{Hybrid Type Checking}
+\subsection{Hybrid Contract Checking}
\begin{enumerate}
\item Idea: Combine Contracts and Liquid Types
\item Sprinkle in casts everywhere an assertion is made
@@ -691,8 +783,17 @@ In this section, we will focus on two related approaches of specifying contracts
\item Refinements $\cap$ Effects
\end{enumerate}
-\todo[inline]{Full dependent types, Lambda Cube}
-
\todo[inline]{Proof objects, proof search, provable pointers, existential types, proof for non-aliasing à la ATS and an improved borrow checker?}
-\todo[inline]{Unsafe Rust, Raw}
\ No newline at end of file
+\todo[inline]{Intermediate Representations and MIR}
+
+\todo[inline]{Flow-sensitive typing; for example: \inline{extract: \{x: Option<T> | x.is_some()\} -> T} or the \inline{?} operator using extract if possible}
+\begin{lstlisting}[language=Rust]
+// Note that the return type is `()`
+fn do_stuff_if_some<T : Debug>(x : Option<T>) {
+ if x.is_none() {
+ return;
+ }
+ println!("{:?}", x?); // Infallible at this point
+}
+\end{lstlisting}
\ No newline at end of file
diff --git a/thesis/thesis.pdf b/thesis/thesis.pdf
index 6ad4f6d..491fc48 100644
--- a/thesis/thesis.pdf
+++ b/thesis/thesis.pdf
@@ -1,3 +1,3 @@
version https://git-lfs.github.com/spec/v1
-oid sha256:833840517a216c1a830947b08ff1b8efdf469e7b3a5908812fc6a8911f7af4ef
-size 165241
+oid sha256:bff4b7d999a03caf0f89924fbe37cd4155ca0591dff8b7eaf0c2a442702dd548
+size 177647
--
GitLab