diff --git a/.gitignore b/.gitignore index 3f2ecf4ff0d85ee2365fe27af3fcd57bf67b7d07..679b11d29ff8768e84b846aee8bf0554c6d126e9 100644 --- a/.gitignore +++ b/.gitignore @@ -26,4 +26,7 @@ __pycache__/ /**/target -/**/mir_dump \ No newline at end of file +/**/mir_dump + +/**/_minted* +*.pygtex \ No newline at end of file diff --git a/preamble.tex b/preamble.tex index 8c2183b5dad65db93361b4c23c5ae4e1fc2571ac..9758ceffa929bd0566616f0b0d49899f642024bc 100644 --- a/preamble.tex +++ b/preamble.tex @@ -51,6 +51,10 @@ ]{markdown} \usepackage{xcolor} +\usepackage{minted} +\setminted{autogobble, mathescape} + + \usepackage{listings} \lstdefinelanguage{Rust}{% sensitive,% diff --git a/thesis/1-introduction.tex b/thesis/1-introduction.tex index 6e33fbf2287939809029781c6284bcd23137d434..71e2dc6b2f6a27a862c6bef7b245af29bc5e05a2 100644 --- a/thesis/1-introduction.tex +++ b/thesis/1-introduction.tex @@ -656,46 +656,52 @@ Since the inception of set theory, mathematicians used \emph{set comprehension} \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} +\begin{listing}[H] + \begin{minted}[mathescape]{lean} + { n : $\BbbN$ // prime n } + -- Syntactic sugar for: + subtype nat prime + \end{minted} + \caption{Refinement types in Lean} + \label{lst:lean-subtype} +\end{listing} \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!() +\begin{listing} + \begin{minted}{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)>() + struct Subtype<T, const pred: fn(T) -> bool> { + val: T, + proof: Prop<pred(val)> } - } -} -// Also implement `Deref` and `DerefMut` so that a -// `Subtype<T, pred>` can be used in any place where a -// `T` is expected. + impl<T, const pred: fn(T) -> bool> Subtype<T, pred> { + const fn new(val: T) -> Self { + Self { + val, + proof: Prop::new::<pred(val)>() + } + } + } -\end{lstlisting} + // Also implement `Deref` and `DerefMut` so that a + // `Subtype<T, pred>` can be used in any place where a + // `T` is expected. + \end{minted} + \caption{The Rusty equivalent.} +\end{listing} \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}. diff --git a/thesis/thesis.pdf b/thesis/thesis.pdf index 491fc486abf4a33cde5a10fdd918fd602f52fac6..6b33b65bde1a534be40dfd5ec94657984b19a619 100644 --- a/thesis/thesis.pdf +++ b/thesis/thesis.pdf @@ -1,3 +1,3 @@ version https://git-lfs.github.com/spec/v1 -oid sha256:bff4b7d999a03caf0f89924fbe37cd4155ca0591dff8b7eaf0c2a442702dd548 -size 177647 +oid sha256:b8ea16b1a321761b04168b48217eb15326676d5422e82621f0f743fa107f1ade +size 177576 diff --git a/thesis/thesis.tex b/thesis/thesis.tex index fda686631f2de1daf81fd5597775d244fd716a8a..23243965bf78bc047420d62f5e278b5a4d6a9e9d 100644 --- a/thesis/thesis.tex +++ b/thesis/thesis.tex @@ -1,7 +1,7 @@ -% arara: lualatex +% arara: lualatex: {shell: true} % arara: biber -% arara: lualatex -% arara: lualatex +% arara: lualatex: {shell: true} +% arara: lualatex: {shell: true} \documentclass[a4paper, oneside, article]{memoir}