merge

.github/workflows/ci.yml

@@ -3,7 +3,16 @@ jobs:
     build:
         runs-on: ubuntu-latest
         steps:
-          - run: sudo apt-get update
-          - run: sudo apt-get install --no-install-recommends -y biber latexmk lmodern texlive-bibtex-extra texlive-latex-extra texlive-science
-          - uses: actions/checkout@v2
-          - run: make
+          - name: Setup
+            run: sudo apt-get update && sudo apt-get install --no-install-recommends -y biber latexmk lmodern texlive-bibtex-extra texlive-latex-extra texlive-science
+          - name: Checkout
+            uses: actions/checkout@v2
+          - name: Change to python edition
+            run: sed -i 's|\\def\\edition{0}|\\def\\edition{1}|g' book.tex
+          - name: Build PDF
+            run: make
+          - name: Release
+            uses: softprops/action-gh-release@v1
+            if: startsWith(github.ref, 'refs/tags/')
+            with:
+              files: book.pdf

.gitignore

@@ -13,3 +13,7 @@ auto/
 *.run.xml
 *.synctex.gz
 *.toc
+*.fls
+*latexmk
+book.pdf
+

Makefile

@@ -12,7 +12,9 @@ continuous:
 
 clean:
 	$(LATEXMK) -C book
-	rm -f book.log book.aux book.bbl book.lof book.out book.toc book.blg book.pdf book.ilg book.ind book.lot book.run.xml book.bcf book.fls book.fdb_latexmk authors.idx athors.ilg authors.ind subject.idx subject.ilg subject.ind
+	rm -f book.pdf *.log *.aux *.bbl \
+	      *.lof *.out *.toc *.blg *.ilg *.ind *.idx \
+	      *.lot *.run.xml *.bcf *.fls *.fdb_latexmk
 
 # Build with a fixed snapshot of NixPkgs 17.03.  Known-to-work.
 # For a very clean version, run git clean -fxd followed by this:

book.bib

@@ -1,3 +1,43 @@
+@article{Pierce:2000,
+author = {Pierce, Benjamin C. and Turner, David N.},
+title = {Local Type Inference},
+year = 2000,
+issue_date = {Jan. 2000},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = 22,
+number = 1,
+issn = {0164-0925},
+url = {https://doi.org/10.1145/345099.345100},
+doi = {10.1145/345099.345100},
+abstract = {We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices by a statistical analysis of the uses of type inference in a sizable body of existing ML code.},
+journal = {ACM Trans. Program. Lang. Syst.},
+month = {jan},
+pages = {1–44},
+numpages = 44,
+keywords = {subtyping, polymorphism, type inference}
+}
+
+@article{Dunfield:2021,
+author = {Dunfield, Jana and Krishnaswami, Neel},
+title = {Bidirectional Typing},
+year = 2021,
+issue_date = {June 2022},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = 54,
+number = 5,
+issn = {0360-0300},
+url = {https://doi.org/10.1145/3450952},
+doi = {10.1145/3450952},
+abstract = {Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to support features for which inference is undecidable; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner’s local type inference to the present day, and provide guidance for future investigations.},
+journal = {ACM Comput. Surv.},
+month = {may},
+articleno = 98,
+numpages = 38,
+keywords = {type inference, Type checking}
+}
+
 @inproceedings{Hatcliff:1994ea,
 	address = {New York, NY, USA},
 	author = {John Hatcliff and Olivier Danvy},

defs.tex

@@ -99,6 +99,8 @@
 \newcommand{\FType}{\itm{ftype}}
 \newcommand{\Instr}{\itm{instr}}
 \newcommand{\Block}{\itm{block}}
+\newcommand{\Blocks}{\itm{blocks}}
+\newcommand{\Params}{\itm{params}}
 \newcommand{\Tail}{\itm{tail}}
 \newcommand{\Prog}{\itm{prog}}
 \newcommand{\Arg}{\itm{arg}}
@@ -108,7 +110,9 @@
 \newcommand{\Var}{\itm{var}}
 \newcommand{\Op}{\itm{op}}
 \newcommand{\key}[1]{\texttt{#1}}
+\newcommand{\skey}[1]{\texttt{'#1'}}
 \newcommand{\code}[1]{\texttt{#1}}
+\newcommand{\scode}[1]{\texttt{'#1'}}
 
 \newcommand{\LP}{\key{(}}
 \newcommand{\RP}{\key{)}}
@@ -256,7 +260,7 @@
 \newcommand{\ALLOC}[2]{\LP\key{Allocate}~#1~#2\RP}
 \newcommand{\ALLOCCLOS}[3]{\LP\key{AllocateClosure}~#1~#2~#3\RP}
 
-\newcommand{\VOID}[1]{\key{(Void)}}
+\newcommand{\VOID}{\key{(Void)}}
 \newcommand{\FUNREFARITY}[2]{\key{(FunRefArity}~#1~#2\code{)}}
 \newcommand{\CFUNREFARITY}[2]{\key{(fun-ref-arity}~#1~#2\code{)}}
 \newcommand{\CGLAMBDA}[3]{\LP\key{lambda:}\,#1\,#2~\Exp\RP}
@@ -280,11 +284,13 @@
 \newcommand{\FUNDEF}[5]{\key{(Def}~#1~#2~#3~#4~#5\code{)}}
 \fi
 \if\edition\pythonEd
-\newcommand{\LAMBDA}[2]{\key{Lambda}\LP#1\key{, }#2\RP}
+\newcommand{\LAMBDA}[2]{\key{Lambda}\LP#1\code{, }#2\RP}
 \newcommand{\CLAMBDA}[2]{\key{lambda}\,#1\,\key{:}\,#2}
-\newcommand{\TAILCALL}[2]{\key{TailCall}\LP#1\code{,}#2\RP}
+\newcommand{\TAILCALL}[2]{\key{TailCall}\LP#1\code{, }#2\RP}
 \newcommand{\CASSIGN}[2]{#1~\key{=}~#2}
 \newcommand{\ASSIGN}[2]{\key{Assign}\LP\LS #1\RS\key{, }#2\RP}
+\newcommand{\CANNASSIGN}[3]{#1~\key{:}~#2~\key{=}~#3}
+\newcommand{\ANNASSIGN}[3]{\key{AnnAssign}\LP#1\key{, }#2\key{, }#3\key{, 0}\RP}
 \newcommand{\IFSTMT}[3]{\key{If}\LP #1 \code{, } #2 \code{, } #3 \RP}
 \newcommand{\CIFSTMT}[3]{\key{if}~#1\code{:}~#2~\code{else:}~#3}
 \newcommand{\CBEGIN}[2]{\key{begin:}~#1~#2}
@@ -294,7 +300,7 @@
 \newcommand{\CRETURN}[1]{\key{return}~#1}
 \newcommand{\GOTO}[1]{\key{Goto}\LP #1 \RP}
 \newcommand{\CGOTO}[1]{\key{goto}~#1}
-\newcommand{\FUNDEF}[5]{\key{FunctionDef}\LP#1\key{, }#2\key{, }#3\key{, }#5\RP}
+\newcommand{\FUNDEF}[5]{\key{FunctionDef}\LP#1\key{, }#2\key{, }#3\key{, None}\key{, }#5\key{, None}\RP}
 \fi
 
 \newcommand{\SEQ}[2]{\key{(Seq}~#1~#2\key{)}}
@@ -305,9 +311,9 @@
 \newcommand{\DEREF}[2]{\key{(Deref}~#1~#2\key{)}}
 \newcommand{\BININSTR}[3]{\key{(Instr}~#1~\key{(}#2~#3\key{))}}
 \newcommand{\UNIINSTR}[2]{\key{(Instr}~#1~\key{(}#2\key{))}}
-\newcommand{\CALLQ}[2]{\key{(Callq}~#1~#2\key{)}}
-\newcommand{\PUSHQ}[1]{\key{(Pushq}~#1\key{)}}
-\newcommand{\POPQ}[1]{\key{(Popq}~#1\key{)}}
+\newcommand{\CALLQ}[2]{\LP\key{Callq}~#1~#2\RP}
+\newcommand{\PUSHQ}[1]{\LP\key{Instr}~\key{pushq}~\LP#1\RP\RP}
+\newcommand{\POPQ}[1]{\LP\key{Instr}~\key{popq}~\LP#1\RP\RP}
 \newcommand{\JMP}[1]{\key{(Jmp}~#1\key{)}}
 \newcommand{\JMPIF}[2]{\key{(JmpIf}~#1~#2\key{)}}
 \newcommand{\RETQ}{\key{(Retq)}}
@@ -327,8 +333,8 @@
 \newcommand{\BININSTR}[3]{\key{Instr}\LP #1 \key{,} \LS #2 \key{,} #3 \RS \RP}
 \newcommand{\UNIINSTR}[2]{\key{Instr}\LP #1 \key{,} \LS #2 \RS \RP}
 \newcommand{\CALLQ}[2]{\key{Callq}\LP #1 \key{,} #2 \RP}
-\newcommand{\PUSHQ}[1]{\key{Instr}\LP \code{pushq} \key{,} \LS #1 \RS \RP}
-\newcommand{\POPQ}[1]{\key{Instr}\LP \code{popq} \key{,} \LS #1 \RS \RP}
+\newcommand{\PUSHQ}[1]{\key{Instr}\LP \scode{pushq} \key{,} \LS #1 \RS \RP}
+\newcommand{\POPQ}[1]{\key{Instr}\LP \scode{popq} \key{,} \LS #1 \RS \RP}
 \newcommand{\JMP}[1]{\key{Jump}\LP #1 \RP}
 \newcommand{\JMPIF}[2]{\key{JumpIf}\LP #1 \key{,} #2 \RP}
 \newcommand{\RETQ}{\key{Retq}\LP\RP}