mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-10-26 21:42:45 +03:00
87 lines
2.0 KiB
TeX
87 lines
2.0 KiB
TeX
\input{../common/header}
|
|
|
|
\title{A type system for nix}
|
|
|
|
\begin{document}
|
|
|
|
\maketitle{}
|
|
|
|
\section{Types}
|
|
\begin{grammar}
|
|
<t> ::= \c/ \| \t/ $\bm{\rightarrow}$ \t/
|
|
\alt \t/ $\bm{\vee}$ \t/ \| \t/ $\bm{\wedge}$ \t/ \| \t/ $\bm{\backslash}$ \t/
|
|
\alt [\meta{R}]
|
|
\alt \{ \s/ = \u/; \ldots{}; \s/ = \u/; _ = \u/ \}
|
|
|
|
<u> ::= \t/ \| ?\t/
|
|
|
|
<R> ::= \t/ \| \meta{R^{\bm{+}}} \| \meta{R}?
|
|
\| \meta{R} $\bm{\vee}$ \meta{R} \| \meta{R} $\bm{\wedge}$ \meta{R}
|
|
|
|
<\τ> ::= \t/ % No polymorphism for now
|
|
\end{grammar}
|
|
|
|
\section{Typing rules}
|
|
\subsection{$\lambda\&$-calculus}
|
|
\begin{mathpar}
|
|
\inferrule{ }{\Gamma; x:\tau \vdash x:\tau}(Var)
|
|
|
|
\and
|
|
\inferrule{ }{\Gamma \vdash c:\mathcal{B}(c)}(Const)
|
|
|
|
\and
|
|
\inferrule{%
|
|
\Gamma \vdash e_1 : \tau_1 \\ \Gamma \vdash e_2 : \tau_2 \\
|
|
\tau_1 \subtype \zero \rightarrow \one \\
|
|
\tau_2 \subtype \dom(\tau_1)
|
|
}{%
|
|
\Gamma \vdash e_1 e_2 : \tau_1 \tau_2
|
|
}
|
|
(App)
|
|
|
|
\and
|
|
\inferrule{%
|
|
\forall (\sigma \rightarrow \tau) \in \mathbb{I}, \\
|
|
\Gamma; \ofTypeP{p}{\sigma} \vdash e: \tau' \\
|
|
\tau' \subtype \tau
|
|
}{%
|
|
\lambda^\mathbb{I}p.e : \text{TypeOf}(\mathbb{I})
|
|
}
|
|
(Abs)
|
|
|
|
\and
|
|
\inferrule{%
|
|
\Gamma \vdash e : \tau \\
|
|
% TODO: fix display of cases here
|
|
\begin{cases}
|
|
\tau \not\subtype \lnot t \Rightarrow \Gamma \vdash e_1 : \sigma_1 &
|
|
\tau \not\subtype t \Rightarrow \Gamma \vdash e_2 : \sigma_2
|
|
\end{cases}
|
|
}{%
|
|
\Gamma \vdash ((e \in t) ? e_1 : e_2) : \sigma_1 \vee \sigma_2
|
|
}
|
|
(Tcase)
|
|
|
|
\and
|
|
\inferrule{%
|
|
\forall i \in \discrete{0}{n},
|
|
\Gamma; x_i : \tau_{(1,i)}; \ldots; x_n: \tau_{(n,i)} \vdash e_i : \sigma_i \\
|
|
\forall (i,j) \in \discrete{0}{n} \times \discrete{1}{n},
|
|
\sigma_j \subtype \tau_{(i,j)}
|
|
}{%
|
|
\Gamma \vdash \text{let } x_1 = e_1; \ldots{}; x_n = e_n \text{ in } e_0 : \sigma_0
|
|
}
|
|
(Let)
|
|
\end{mathpar}
|
|
\subsection{Records}
|
|
\begin{mathpar}
|
|
\input{recordTypingRules}
|
|
\end{mathpar}
|
|
|
|
\subsection{Other builtin operators}
|
|
\todo{add rules for operators}
|
|
|
|
\todos
|
|
|
|
\end{document}
|