32f92cb · tix · git.iko.soy

git.iko.soy/tix

on master help sign in

static atomic types

32f92cbiko5 years ago

docs/paper.lhs+63−2

compare with master

unifiedsplit

@@ -120,7 +120,7 @@ Atomic types are described in table~\ref{tab:atomicTypes}.

120 \centering

121 \caption{Table of atomic Nix Expression Language types}

122 \begin{tabular}{ ||c||p{2cm}||p{4cm}|| } \hline

123− \textbf{Atomic type} & \textbf{Description} & \textbf{Example terms} \\ \hline

123+ \textbf{Atomic type} & \textbf{Description} & \textbf{Example terms} \\ \hline \hline

124 URI & A string literal representing a URI. Does not require quoting. & \texttt{https://example.com} \\ \hline

125 Path literal & A path literal referring to either a relative or absolute path. Does not require quoting. & \texttt{../../directory/file.txt} \\ \hline

126 Integer & The current C implementation of Nix allows values of 64-bit signed integers. & \texttt{69} \newline \texttt{-42} \\ \hline

@@ -559,6 +559,45 @@ The term \texttt{x: y: x // y} would field the following type:

559 \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma

560\end{equation}

561

562+\subsection{Atmoic types}

563+

564+Nix is a dynamic language, and as such, allows dynamic coercions between certain types. This means that we can not use the dynamic types from the interpreter to perform static type checking -- if we did that we would reject \emph{a lot} of valid programs.\footnote{``Valid'' not just in the sense that they would not produce runtime errors, but ``valid'' in the sense that the programmer would judge the program as being ``correct''.}

565+

566+For this reason, we will have to define a smaller set of static types that will be employed in our type system. The static types along with the corresponding dynamic types from table~\ref{tab:atomicTypes} are shown in table~\ref{tbl:staticTypes}.

567+

568+\begin{table}[hbp]

569+ \centering

570+ \caption{Mapping from static types to dynamic types}

571+ \begin{tabular}{ ||c||c|| } \hline

572+ \textbf{Static type} & \textbf{Dynamic types} \\ \hline \hline

573+ String & URI, Path literal, String \\ \hline

574+ Number & Integer, Float \\ \hline

575+ Bool & Bool \\ \hline

576+ Null & Null \\ \hline

577+ \end{tabular}

578+ \label{tbl:staticTypes}

579+\end{table}

580+

581+\subsection{Addition}

582+

583+Among all operators, addition (\texttt{+}) has semantics that stand out from the rest: addition can be applied to wither two \texttt{Number} operands or two \texttt{String} operands. All other operands are monomorphic in that they can only be applied to two operands of a predefined type. In that sense addition in polymorphic.

584+

585+Since our current implementation does not support sum types (see section~\ref{sec:sumTypes} for more detail), it is non-trivial to encode the type of addition in our current type system. We wanted to encode the type without having to resort to extending the type system too much (without implementing sum types).

586+

587+The simplest approach is to introduce a simple predicate which is satisfied only if the argument is either of type \texttt{Number} or \texttt{String}:

588+

589+\newcommand{\strOrNum}{(\text{String} || \text{Number})}

590+

591+\begin{equation}

592+ \strOrNum \sim \alpha

593+\end{equation}

594+

595+With this predicate the type of the addition operator (\texttt{+}) now becomes:

596+

597+\begin{equation}

598+ \forall \alpha. \; \strOrNum \sim \alpha \Rightarrow \alpha \rightarrow \alpha \rightarrow \alpha

599+\end{equation}

600+

562\subsection{Typing rules}

601\subsection{Typing rules}

563

602

564\begin{equation}

603\begin{equation}

@@ -612,7 +651,7 @@ The term \texttt{x: y: x // y} would field the following type:

612\begin{equation}

651\begin{equation}

613 \trfrac

652 \trfrac

614 {\Gamma \vdash e \optDot \text{x} = \tau}

653 {\Gamma \vdash e \optDot \text{x} = \tau}

615− {\Gamma \vdash (e \; \text{?} \; \text{x}) : Bool}

654+ {\Gamma \vdash (e \; \text{?} \; \text{x}) : \text{Bool}}

616\end{equation}

655\end{equation}

617

656

618\begin{equation}

657\begin{equation}

@@ -639,6 +678,24 @@ The term \texttt{x: y: x // y} would field the following type:

639 {\Gamma \vdash (\text{if} \; e_1 \; \text{then} \; e_2 \; \text{else} \; e_3) : \tau}

678 {\Gamma \vdash (\text{if} \; e_1 \; \text{then} \; e_2 \; \text{else} \; e_3) : \tau}

640\end{equation}

679\end{equation}

641

680

681+\begin{equation}

682+ \trfrac

683+ {\Gamma \vdash e : \tau \qquad \{\text{x} = e;\} \in \xi}

684+ {\Gamma \vdash (\Pi \xi).\text{x} = \tau}

685+\end{equation}

686+

687+\begin{equation}

688+ \trfrac

689+ {\text{x} \notin \xi}

690+ {(\Pi \xi) \optDot \text{x} = \tau}

691+\end{equation}

692+

693+\begin{equation}

694+ \trfrac

695+ {\Gamma, \xi \vdash e : \tau}

696+ {\Gamma \vdash (\text{with } (\Pi \xi)\text{; } e) : \tau}

697+\end{equation}

698+

642\section{Implementation} \label{sec:implementation}

699\section{Implementation} \label{sec:implementation}

643

700

644\cite{github-source}

701\cite{github-source}

@@ -690,6 +747,10 @@ The technique is not in applicable if the ``result'' of a predicate is not a typ

690

747

691Another limitation is that we can not remove predicates if their ``result'' type variable is not present in the head of the type like in type \ref{eq:optFieldPredExample}, since we would be losing typing information by doing so.

748Another limitation is that we can not remove predicates if their ``result'' type variable is not present in the head of the type like in type \ref{eq:optFieldPredExample}, since we would be losing typing information by doing so.

692

749

750+\subsection{Type hints}

751+

752+\subsection{Sum types} \label{sec:sumTypes}

753+

693\section{Conclusion}

754\section{Conclusion}

694

755

695Nix is a rapidly growing ecosystem. At the time of writing, nixpkgs, the Nix package registry, contains over 60000 packages\footnote{\url{https://github.com/NixOS/nixpkgs}} that can be either installed or used as dependencies in other projects. There is much interest in the approach used by Nix, and making the ever-growing codebase of configurations easier to manage and extend would be a welcome development.

756Nix is a rapidly growing ecosystem. At the time of writing, nixpkgs, the Nix package registry, contains over 60000 packages\footnote{\url{https://github.com/NixOS/nixpkgs}} that can be either installed or used as dependencies in other projects. There is much interest in the approach used by Nix, and making the ever-growing codebase of configurations easier to manage and extend would be a welcome development.