<commit_before>\chapter{Introduction}

Unicorns are $\mathbb{PRETTY}$.


\section{Ideas and Concerns}

\subsection{Design by Contract}
Semantic types are often used to label values that have a special property. For example, a list may be sorted, a file may be open and a matrix may be symmetric. Many of these properties can be checked quite easily. We can apply this observation to the notion of \textbf{design by contract} as follows: For a semantic type that is added to a specific value type, we can specify a function that checks whether the semantic type may be applied in the context of a specific value. These functions are applied during development and testing, may be optionally turned on in production, and lead to runtime errors if the contract is violated.

\subsection{Type Modes and Covariant, Part Type Parameters}
Suppose we have a type \type{A} with exactly two modes of existence \type{M1} and \type{M2}, which are defined as simple label types. Values of \type{A} can only exist in mode 1 or mode 2, but \textbf{not} stand alone. How can we encode this in the type system?\footnote{\textbf{Intersection types} are of no use here, because we can neither limit the other type used with \type{A} in an intersection type, nor can we require that \type{A} must always be used in an intersection type.}

One way to do this would utilise parametric types. Consider the following code:

\begin{lstlisting}
    label type M1
    label type M2
    type M = M1 | M2
    class A[covariant m <: M] { ... }
\end{lstlisting}

We can instantiate \type{A} only as \type{A[M1]} or \type{A[M2]}.\footnote{This is only true, because the sum type can't be extended outside its definition, so we can't create more \textit{direct} subtypes of \type{M}.} Because \type{A} is covariant in \type{m}, we have that $\type{A[M1]} < \type{A[M]}$ and $\type{A[M2]} < \type{A[M]}$. However, \type{A[M]} is not necessarily abstract. This means we couldn't define an abstract function for \type{A[M]}. 

A \textit{quick fix} is to introduce a new keyword for type parameters that make the containing type abstract if they are themselves abstract. We'll call this a \texttt{part}-type parameter:

\begin{lstlisting}
    class A[part covariant m <: M] { ... }
\end{lstlisting}

We can then finally define the abstract function and the two concrete functions, one for each mode, as such:

\begin{lstlisting}
    function do(a: A[M]): Unit = ...
    function do(a: A[M1]): Unit = ...
    function do(a: A[M2]): Unit = ...
\end{lstlisting}

Multiple-dispatch will then dispatch to the correct function depending on the runtime type of a value \texttt{a : A[M]}.


<commit_msg>Add abstract type definition idea.<commit_after>\chapter{Introduction}

Unicorns are $\mathbb{PRETTY}$.



\section{Ideas and Concerns}

\subsection{Design by Contract}
Semantic types are often used to label values that have a special property. For example, a list may be sorted, a file may be open and a matrix may be symmetric. Many of these properties can be checked quite easily. We can apply this observation to the notion of \textbf{design by contract} as follows: For a semantic type that is added to a specific value type, we can specify a function that checks whether the semantic type may be applied in the context of a specific value. These functions are applied during development and testing, may be optionally turned on in production, and lead to runtime errors if the contract is violated.


\subsection{Type Modes and Covariant, Part Type Parameters}
Suppose we have a type \type{A} with exactly two modes of existence \type{M1} and \type{M2}, which are defined as simple label types. Values of \type{A} can only exist in mode 1 or mode 2, but \textbf{not} stand alone. How can we encode this in the type system?\footnote{\textbf{Intersection types} are of no use here, because we can neither limit the other type used with \type{A} in an intersection type, nor can we require that \type{A} must always be used in an intersection type.}

One way to do this would utilise parametric types. Consider the following code:

\begin{lstlisting}
    label type M1
    label type M2
    type M = M1 | M2
    class A[covariant m <: M] { ... }
\end{lstlisting}

We can instantiate \type{A} only as \type{A[M1]} or \type{A[M2]}.\footnote{This is only true, because the sum type can't be extended outside its definition, so we can't create more \textit{direct} subtypes of \type{M}.} Because \type{A} is covariant in \type{m}, we have that $\type{A[M1]} < \type{A[M]}$ and $\type{A[M2]} < \type{A[M]}$. However, \type{A[M]} is not necessarily abstract. This means we couldn't define an abstract function for \type{A[M]}. 

A \textit{quick fix} is to introduce a new keyword for type parameters that make the containing type abstract if they are themselves abstract. We'll call this a \texttt{part}-type parameter:

\begin{lstlisting}
    class A[part covariant m <: M] { ... }
\end{lstlisting}

We can then finally define the abstract function and the two concrete functions, one for each mode, as such:

\begin{lstlisting}
    function do(a: A[M]): Unit = ...
    function do(a: A[M1]): Unit = ...
    function do(a: A[M2]): Unit = ...
\end{lstlisting}

Multiple-dispatch will then dispatch to the correct function depending on the runtime type of a value \texttt{a : A[M]}.


\subsection{Definition of Abstract Types}
An abstract type is a type for which the following holds: Let $I_\tau$ be the set of instantiable values of a type $\tau$. Let $I_{sub} = \bigcup_{\sigma < \tau} values(\sigma)$ be the set of instantiable values of all subtypes of $\tau$. Type $\tau$ is abstract, if and only if $I_\tau - I_{sub} = \emptyset$.






{'fraction_non_alphanumeric': 0.09110057925223802, 'fraction_numerical': 0.004914867474109181, 'mean_word_length': 3.998245614035088, 'pattern_counts': {'":': 0, '<': 12, '<?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': '5792923', 'n_tokens_mistral': 1649, 'n_tokens_neox': 1570, 'n_words': 834}