git.iko.soy/tix
on master help sign in
Added basic typing rules
e8cb401iko
docs/bibl.bib+14−10
compare with master
unifiedsplit
@@ -1,13 +1,18 @@
1%% This BibTeX bibliography file was created using BibDesk.
1%% This BibTeX bibliography file was created using BibDesk.
2%% https://bibdesk.sourceforge.io/
2%% https://bibdesk.sourceforge.io/
3
3
4−%% Created for Ilya at 2021-05-11 12:38:16 +0300
4+%% Created for Ilya at 2021-05-15 17:02:08 +0300
5
5
6
6
7%% Saved with string encoding Unicode (UTF-8)
7%% Saved with string encoding Unicode (UTF-8)
8
8
9
9
10
10
11+@webpage{github-source,
12+ date-added = {2021-05-15 17:00:09 +0300},
13+ date-modified = {2021-05-15 17:02:05 +0300},
14+ url = {https://github.com/ilyakooo0/tix}}
15+
11@article{goldberg2000mercury,
16@article{goldberg2000mercury,
12 author = {Goldberg, Ken and Gentner, Steve and Sutter, Carl and Wiegley, Jeff},
17 author = {Goldberg, Ken and Gentner, Steve and Sutter, Carl and Wiegley, Jeff},
13 date-added = {2021-04-25 18:35:16 +0300},
18 date-added = {2021-04-25 18:35:16 +0300},
@@ -202,12 +207,11 @@
202 year = {2008}}
207 year = {2008}}
203
208
204@article{wand1991type,
209@article{wand1991type,
210+ author = {Wand, Mitchell},
211+ journal = {Information and Computation},
212+ number = {1},
213+ pages = {1--15},
214+ publisher = {Elsevier},
205− title={Type inference for record concatenation and multiple inheritance},
215+ title = {Type inference for record concatenation and multiple inheritance},
206− author={Wand, Mitchell},
207− journal={Information and Computation},
208− volume={93},
216+ volume = {93},
209− number={1},
210− pages={1--15},
211− year={1991},
217+ year = {1991}}
212− publisher={Elsevier}
213−}
docs/default.nix+1−1
@@ -35,6 +35,6 @@ builtins.listToAttrs (map
35 [
35 [
36 { file = ./tech_spec.tex; }
36 { file = ./tech_spec.tex; }
37 { file = ./project_proposal.tex; }
37 { file = ./project_proposal.tex; }
38− { file = ./paper.lhs; extraFiles = [ ./bibl.bib ]; }
38+ { file = ./paper.lhs; extraFiles = [ ./bibl.bib ./trfrac.sty ]; }
39 ]
39 ]
40)
40)
docs/paper.lhs+85
@@ -4,6 +4,7 @@
4\usepackage{mathtools}
4\usepackage{mathtools}
5\usepackage{hyperref}
5\usepackage{hyperref}
6\usepackage{microtype}
6\usepackage{microtype}
7+\usepackage{trfrac}
7% \usepackage{caption}
8% \usepackage{caption}
8% \usepackage[main=english,russian]{babel}
9% \usepackage[main=english,russian]{babel}
9
10
@@ -40,6 +41,8 @@
40
41
41\begin{document}
42\begin{document}
42\maketitle
43\maketitle
44+\thispagestyle{plain}
45+\pagestyle{plain}
43
46
44\begin{abstract}
47\begin{abstract}
45 Configuring and building even the most straightforward software projects is often not simple -- it requires downloading and installing copious amounts of prerequisite software. This often makes reproducing builds of a project on different machines problematic. The Nix package manager aims to address this problem by providing a unified language for describing software packages in a purely functional way. This language is called the Nix Expression Language. Since all of the complexity of software configuration needs to be expressed in the Nix Expression Language, the expressions themselves often become quite complicated, making it difficult to understand and extend existing expressions without introducing errors. A widespread tool for easing the understandability and correctness of expressions in other languages is static type checking. This paper will explore the techniques that can be used to add static type checking to the Nix Expression Language.
48 Configuring and building even the most straightforward software projects is often not simple -- it requires downloading and installing copious amounts of prerequisite software. This often makes reproducing builds of a project on different machines problematic. The Nix package manager aims to address this problem by providing a unified language for describing software packages in a purely functional way. This language is called the Nix Expression Language. Since all of the complexity of software configuration needs to be expressed in the Nix Expression Language, the expressions themselves often become quite complicated, making it difficult to understand and extend existing expressions without introducing errors. A widespread tool for easing the understandability and correctness of expressions in other languages is static type checking. This paper will explore the techniques that can be used to add static type checking to the Nix Expression Language.
@@ -556,8 +559,90 @@ The term \texttt{x: y: x // y} would field the following type:
556 \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma
559 \forall \alpha \beta \gamma. \; \alpha \update \beta \sim \gamma \Rightarrow \alpha \rightarrow \beta \rightarrow \gamma
557\end{equation}
560\end{equation}
558
561
562+\subsection{Typing rules}
563+
564+\begin{equation}
565+ \trfrac
566+ {\Gamma \vdash e_1:\tau \quad \cdots \quad \Gamma \vdash e_n:\tau}
567+ {\Gamma \vdash [e_1 \; \cdots \; e_n ] : [\tau]}
568+\end{equation}
569+
570+\begin{equation}
571+ \trfrac
572+ {\Gamma \vdash e_3:\tau \qquad \Gamma \vdash e_1 \update e_2 \sim e_3}
573+ {\Gamma \vdash (e_2 \update e_2) : \tau}
574+\end{equation}
575+
576+\begin{equation}
577+ \trfrac
578+ {\Gamma \vdash e_1:\tau_1 \rightarrow \tau_2 \qquad \Gamma \vdash e_2 : \tau_1}
579+ {\Gamma \vdash (e_1 \; e_2) : \tau_2}
580+\end{equation}
581+
582+\begin{equation}
583+ \trfrac
584+ {\Gamma \vdash e_1:[\tau] \qquad \Gamma \vdash e_2 : [\tau]}
585+ {\Gamma \vdash (e_1 +\!\!+ \: e_2) : [\tau]}
586+\end{equation}
587+
588+\begin{equation}
589+ \trfrac
590+ {\Gamma \vdash e_1:\tau \qquad \Gamma \vdash e_2 : \tau \qquad \Gamma \vdash (\text{String} || \text{Number}) \sim \tau}
591+ {\Gamma \vdash (e_1 + e_2) : \tau}
592+\end{equation}
593+
594+\begin{equation}
595+ \trfrac
596+ {\Gamma \vdash e.\text{x} = \tau}
597+ {\Gamma \vdash (e.\text{x}) : \tau}
598+\end{equation}
599+
600+\begin{equation}
601+ \trfrac
602+ {\Gamma \vdash e.\text{x} = \tau}
603+ {\Gamma \vdash (e \optDot \text{x}) = \tau}
604+\end{equation}
605+
606+\begin{equation}
607+ \trfrac
608+ {\Gamma \vdash e_2 : \tau \qquad \Gamma \vdash e_1 \optDot \text{x} = \tau}
609+ {\Gamma \vdash (e.\text{x} \; \text{or} \; e_2) : \tau}
610+\end{equation}
611+
612+\begin{equation}
613+ \trfrac
614+ {\Gamma \vdash e \optDot \text{x} = \tau}
615+ {\Gamma \vdash (e \; \text{?} \; \text{x}) : Bool}
616+\end{equation}
617+
618+\begin{equation}
619+ \trfrac
620+ {\Gamma \vdash e_1 : \tau_1 \qquad \Gamma, (\text{x}: \forall \{\text{ftv}(\tau_1) - \text{ftv}(\Gamma)\}. \; \tau_1) \vdash e_2 : \tau_2}
621+ {\Gamma \vdash (\text{let} \; \text{x = } e_1; \; \text{in} \; e_2) : \tau_2}
622+\end{equation}
623+
624+\begin{equation}
625+ \trfrac
626+ {\Gamma \vdash e : \forall \alpha. \; \tau_1}
627+ {\Gamma \vdash e: [\alpha \rightarrow \tau_2] \tau_1}
628+\end{equation}
629+
630+\begin{equation}
631+ \trfrac
632+ {\Gamma, \text{x}: \tau_1 \vdash e : \tau_2}
633+ {\Gamma \vdash (\text{x: } e) : \tau_1 \rightarrow \tau_2}
634+\end{equation}
635+
636+\begin{equation}
637+ \trfrac
638+ {\Gamma \vdash e_1 : \text{Bool} \qquad \Gamma \vdash e_2 : \tau \qquad \Gamma \vdash e_3 : \tau}
639+ {\Gamma \vdash (\text{if} \; e_1 \; \text{then} \; e_2 \; \text{else} \; e_3) : \tau}
640+\end{equation}
641+
559\section{Implementation} \label{sec:implementation}
642\section{Implementation} \label{sec:implementation}
560
643
644+\cite{github-source}
645+
561\section{Possible improvements}
646\section{Possible improvements}
562
647
563\subsection{Making predicates more user-friendly}
648\subsection{Making predicates more user-friendly}
docs/trfrac.stynew file+193
@@ -0,0 +1,193 @@
1+%%
2+%% This is file `trfrac.sty',
3+%% generated with the docstrip utility.
4+%%
5+%% The original source files were:
6+%%
7+%% trfrac.dtx (with options: `file')
8+%%
9+%% This is a generated file.
10+%%
11+%% Copyright (C) 2009 by Kevin W. Hamlen
12+%%
13+%% This file may be distributed and/or modified under the conditions of
14+%% the LaTeX Project Public License, either version 1.3a of this license
15+%% or (at your option) any later version. The latest version of this
16+%% license is in:
17+%%
18+%% http://www.latex-project.org/lppl.txt
19+%%
20+%% and version 1.3a or later is part of all distributions of LaTeX version
21+%% 2004/10/01 or later.
22+%%
23+\newdimen\trtopgap\trtopgap\z@
24+\newdimen\trbotgap\trbotgap\z@
25+\newcommand\TRF@startp{31415926}
26+\newcommand\TRF@endp{27182818}
27+\newif\ifTRF@first
28+\newif\ifTRF@outer\TRF@outertrue
29+\newif\ifTRF@derivok\TRF@derivoktrue
30+\newdimen\TRF@lhang\TRF@lhang\z@
31+\newdimen\TRF@rhang\TRF@rhang\z@
32+\newdimen\TRF@lsave
33+\newdimen\TRF@ni
34+\newdimen\TRF@bi
35+\newdimen\TRF@bw
36+\newbox\TRF@numbox
37+\newbox\TRF@denombox
38+\newbox\TRF@eqbox
39+\newcommand\TRF@trfrac[3]{%
40+ \begingroup%
41+ \ifnum\lastpenalty=\TRF@startp\relax%
42+ \TRF@firsttrue%
43+ \else%
44+ \TRF@firstfalse%
45+ \fi%
46+ \TRF@lsave\TRF@lhang%
47+ \setbox\TRF@eqbox\hbox{\TRF@derivokfalse#1}%
48+ \ifdim\wd\TRF@eqbox>\z@%
49+ \setbox\TRF@eqbox\hbox{\kern\p@\unhbox\TRF@eqbox}%
50+ \fi%
51+ \TRF@lhang\z@%
52+ \setbox\TRF@numbox\hbox{%
53+ \TRF@outerfalse%
54+ \m@th$\strut%
55+ \penalty\TRF@startp\relax%
56+ #2%
57+ \ifnum\lastpenalty=\TRF@endp\relax\else%
58+ \global\TRF@rhang\z@%
59+ \fi%
60+ $%
61+ }%
62+ \setbox\TRF@denombox\hbox{%
63+ \TRF@derivokfalse%
64+ \m@th$\strut#3$%
65+ }%
66+ \dimen@\wd\TRF@numbox%
67+ \advance\dimen@-\TRF@rhang%
68+ \TRF@bw\dimen@%
69+ \advance\TRF@bw-\TRF@lhang%
70+ \ifdim\wd\TRF@denombox>\TRF@bw\TRF@bw\wd\TRF@denombox\fi%
71+ \advance\dimen@\TRF@lhang%
72+ \advance\dimen@-\wd\TRF@denombox%
73+ \TRF@ni\ifdim\dimen@>\z@\z@\else-.5\dimen@\fi%
74+ \TRF@bi\TRF@ni%
75+ \advance\TRF@bi\TRF@lhang%
76+ \TRF@lhang\ifdim\dimen@<\z@\z@\else.5\dimen@\fi%
77+ \ifdim\TRF@bi>\TRF@lhang\TRF@bi\TRF@lhang\fi%
78+ \TRF@rhang\TRF@ni%
79+ \advance\TRF@rhang\wd\TRF@numbox%
80+ \dimen@\TRF@bi%
81+ \advance\dimen@\TRF@bw%
82+ \advance\dimen@\wd\TRF@eqbox%
83+ \ifdim\dimen@>\TRF@rhang\TRF@rhang\dimen@\fi%
84+ \advance\TRF@rhang-\TRF@lhang%
85+ \advance\TRF@rhang-\wd\TRF@denombox%
86+ \global\TRF@rhang\TRF@rhang%
87+ \mathinner{%
88+ \ifTRF@outer%
89+ \raise\fontdimen22\textfont\tw@\vtop%
90+ \else%
91+ \vbox%
92+ \fi%
93+ {%
94+ \offinterlineskip%
95+ \hbox{%
96+ \vbox{%
97+ \dimen@\fontdimen8\textfont\tw@%
98+ \advance\dimen@-\fontdimen22\textfont\tw@%
99+ \advance\dimen@-.5\fontdimen8\textfont\thr@@%
100+ \advance\dimen@-\dp\TRF@numbox%
101+ \ifdim\dimen@<3\fontdimen8\textfont\thr@@%
102+ \dimen@3\fontdimen8\textfont\thr@@%
103+ \fi%
104+ \advance\dimen@\trtopgap%
105+ \hbox{\kern\TRF@ni\unhbox\TRF@numbox}%
106+ \kern\dimen@%
107+ \hbox{%
108+ \kern\TRF@bi%
109+ \vrule\@width\TRF@bw%
110+ \@height.5\fontdimen8\textfont\thr@@%
111+ \@depth.5\fontdimen8\textfont\thr@@%
112+ \vbox{%
113+ \dimen@.5\ht\TRF@eqbox%
114+ \advance\dimen@.5\dp\TRF@eqbox%
115+ \kern-\dimen@%
116+ \box\TRF@eqbox%
117+ \kern-\dimen@%
118+ }%
119+ }%
120+ }%
121+ }%
122+ \dimen@\fontdimen11\textfont\tw@%
123+ \advance\dimen@\fontdimen22\textfont\tw@%
124+ \advance\dimen@-.5\fontdimen8\textfont\thr@@%
125+ \advance\dimen@-\ht\TRF@denombox%
126+ \ifdim\dimen@<3\fontdimen8\textfont\thr@@%
127+ \dimen@3\fontdimen8\textfont\thr@@%
128+ \fi%
129+ \advance\dimen@\trbotgap%
130+ \kern\dimen@%
131+ \hbox{\kern\TRF@lhang\box\TRF@denombox}%
132+ }%
133+ }%
134+ \ifTRF@outer\else%
135+ \penalty\TRF@endp\relax%
136+ \fi%
137+ \global\TRF@lhang\ifTRF@first\TRF@lhang\else\TRF@lsave\fi%
138+ \endgroup%
139+}
140+\newcommand\trfrac[3][]{%
141+ \ifTRF@derivok%
142+ \ifmmode%
143+ \TRF@trfrac{#1}{#2}{#3}%
144+ \else%
145+ \TRF@mmerr%
146+ \fi%
147+ \else%
148+ \TRF@derr%
149+ \fi%
150+}
151+\newcommand\TRF@mmerr{%
152+ \PackageError{trfrac}{\protect\trfrac\space%
153+ only allowed in math mode}%
154+ {I encountered a \protect\trfrac\space%
155+ macro without first encountering a begin-math token.}%
156+}
157+\newcommand\TRF@derr{%
158+ \PackageError{trfrac}{\protect\trfrac\space%
159+ not allowed in the consequent of another \protect\trfrac}%
160+ {\protect\trfrac\space can only appear in the premise (numerator%
161+ ) of another \protect\trfrac, not in the consequent (denominator%
162+ ) of a \protect\trfrac.}%
163+}
164+\newcommand\TRF@next{}
165+\newcommand\TRF@sep{\futurelet\TRF@next\TRF@@sep}
166+\newcommand\TRF@@sep{%
167+ \ifx[\TRF@next%
168+ \let\TRF@next\TRF@separg%
169+ \else%
170+ \let\TRF@next\TRF@sepnoarg%
171+ \fi%
172+ \TRF@next%
173+}
174+\newcommand\TRF@separg{}
175+\def\TRF@separg[#1]{\cr\noalign{\kern#1}}
176+\newcommand\TRF@sepnoarg{\cr}
177+\newenvironment{trgather}{%
178+ \vbox\bgroup%
179+ \let\\\TRF@sep%
180+ \ialign\bgroup\hfil{\m@th$##$}\hfil\cr%
181+}{%
182+ \crcr\egroup\egroup%
183+}
184+\newenvironment{tralign}{%
185+ \vbox\bgroup%
186+ \let\\\TRF@sep%
187+ \ialign\bgroup\hfil{\m@th$##\null$}&{\m@th$\null##$}\hfil\cr%
188+}{%
189+ \crcr\egroup\egroup%
190+}
191+\endinput
192+%%
193+%% End of file `trfrac.sty'.