e8cb401 · tix · git.iko.soy

git.iko.soy/tix

Added basic typing rules

commite8cb401660e239f3c66acd319815fb94b372b930 authoriko <ilyakooo0@gmail.com> dateSat 15 May 2021, 19:09 (5 years ago) parente39071b

4 files changed+293−11

compare with master

unifiedsplit

docs/bibl.bib+14−10 docs/default.nix+1−1 docs/paper.lhs+85 docs/trfrac.sty+193

docs/bibl.bib+14−10

@@ -1,13 +1,18 @@

11%% This BibTeX bibliography file was created using BibDesk.

22%% https://bibdesk.sourceforge.io/

4−%% Created for Ilya at 2021-05-11 12:38:16 +0300

4+%% Created for Ilya at 2021-05-15 17:02:08 +0300

77%% Saved with string encoding Unicode (UTF-8)

1010

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+

1116@article{goldberg2000mercury,

1217 author = {Goldberg, Ken and Gentner, Steve and Sutter, Carl and Wiegley, Jeff},

1318 date-added = {2021-04-25 18:35:16 +0300},

@@ -202,12 +207,11 @@

202207 year = {2008}}

203208

204209@article{wand1991type,

205− title={Type inference for record concatenation and multiple inheritance},

206− author={Wand, Mitchell},

207− journal={Information and Computation},

208− volume={93},

209− number={1},

210− pages={1--15},

211− year={1991},

212− publisher={Elsevier}

213−}

210+ author = {Wand, Mitchell},

211+ journal = {Information and Computation},

212+ number = {1},

213+ pages = {1--15},

214+ publisher = {Elsevier},

215+ title = {Type inference for record concatenation and multiple inheritance},

216+ volume = {93},

217+ year = {1991}}

docs/default.nix+1−1

@@ -35,6 +35,6 @@ builtins.listToAttrs (map

3535 [

3636 { file = ./tech_spec.tex; }

3737 { file = ./project_proposal.tex; }

38− { file = ./paper.lhs; extraFiles = [ ./bibl.bib ]; }

38+ { file = ./paper.lhs; extraFiles = [ ./bibl.bib ./trfrac.sty ]; }

3939 ]

4040)

docs/paper.lhs+85

@@ -4,6 +4,7 @@

44\usepackage{mathtools}

55\usepackage{hyperref}

66\usepackage{microtype}

7+\usepackage{trfrac}

78% \usepackage{caption}

89% \usepackage[main=english,russian]{babel}

910

@@ -40,6 +41,8 @@

4041

4142\begin{document}

4243\maketitle

44+\thispagestyle{plain}

45+\pagestyle{plain}

4346

4447\begin{abstract}

4548 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:

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

557560\end{equation}

558561

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+

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

560643

644+\cite{github-source}

645+

561646\section{Possible improvements}

562647

563648\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+%%

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'.