suzanne.soy/trivial
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[popl-2017] checkpoint: getting organized

Browse Source
This commit is contained in:
Ben Greenman 2016-05-23 23:50:14 -04:00
parent 911d376361
commit 86634e83e2
14 changed files with 2665 additions and 69 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -6,3 +6,4 @@ doc
*~
\.\#*
popl-2017/icfp-2016

14
popl-2017/.gitignore vendored Normal file
View File

@ -0,0 +1,14 @@
*.aux
*.bbl
*.blg
*.cls
*.log
*.out
*.pdf
paper.tex
pearl.tex
benchmark/
compiled/
*.swp
*.swo

22
popl-2017/Makefile Normal file
View File

@ -0,0 +1,22 @@
PAPER=paper
all: setup ${PAPER}.pdf
compiled/pearl_scrbl.zo: *.rkt *.scrbl
raco make -v $(PAPER).scrbl
${PAPER}.pdf: pkg compiled/${PAPER}_scrbl.zo texstyle.tex
scribble ++extra mathpartir.sty ++style texstyle.tex --pdf $(PAPER).scrbl
${PAPER}.tex: pkg compiled/${PAPER}_scrbl.zo texstyle.tex
scribble ++style texstyle.tex --latex $(PAPER).scrbl
pkg:
raco pkg install --skip-installed trivial
setup:
raco make ${PAPER}.scrbl
clean:
rm -r compiled

18
popl-2017/README.md Normal file
View File

@ -0,0 +1,18 @@
vdt
===
"Value Dependent Types"
Prepping for POPL 2017
Run `make` to build `paper.pdf`.
For later
---
Can't do any analysis/optimizations on variables bound by user input.
But could we compile ``small'' circuits such that one input is given,
we send it to the circuit and quickly detect errors that would occur late
in the program?

1733
popl-2017/bib.rkt Normal file
View File

File diff suppressed because it is too large Load Diff

143
popl-2017/common.rkt Normal file
View File

@ -0,0 +1,143 @@
#lang at-exp racket/base
(provide (all-from-out "bib.rkt")
(all-from-out scriblib/footnote)
(all-from-out scriblib/figure)
(all-from-out scribble/eval)
(all-from-out scriblib/autobib)
(except-out (all-from-out scribble/manual)
author)
~cite
citet
second
etal
exact
generate-bibliography
nrightarrow
parag
sf
id
todo
)
(require "bib.rkt"
racket/class
racket/require
scribble/core
scribble/eval
scribble/manual
scriblib/autobib
scriblib/figure
scriblib/footnote
setup/main-collects
scribble/html-properties
scribble/latex-properties)
(define autobib-style-extras
(let ([abs (lambda (s)
(path->main-collects-relative
(collection-file-path s "scriblib")))])
(list
(make-css-addition (abs "autobib.css"))
(make-tex-addition (abs "autobib.tex")))))
(define bib-single-style (make-style "AutoBibliography" autobib-style-extras))
(define bibentry-style (make-style "Autobibentry" autobib-style-extras))
(define colbibnumber-style (make-style "Autocolbibnumber" autobib-style-extras))
(define colbibentry-style (make-style "Autocolbibentry" autobib-style-extras))
(define small-number-style
(new
(class object%
(define/public (bibliography-table-style) bib-single-style)
(define/public (entry-style) colbibentry-style)
(define/public (disambiguate-date?) #f)
(define/public (collapse-for-date?) #f)
(define/public (get-cite-open) "[")
(define/public (get-cite-close) "]")
(define/public (get-group-sep) ", ")
(define/public (get-item-sep) ", ")
(define/public (render-citation date-cite i)
(make-element
(make-style "Thyperref" (list (command-extras (list (make-label i)))))
(list (number->string i))))
(define/public (render-author+dates author dates) dates)
(define (make-label i)
(string-append "autobiblab:" (number->string i)))
(define/public (bibliography-line i e)
(list (make-paragraph plain
(make-element colbibnumber-style
(list
(make-element (make-style "label" null)
(make-label i))
"[" (number->string i) "]")))
e))
(super-new))))
(define author+date-style/link
(new
(class object%
(define/public (bibliography-table-style) bib-single-style)
(define/public (entry-style) bibentry-style)
(define/public (disambiguate-date?) #t)
(define/public (collapse-for-date?) #t)
(define/public (get-cite-open) "(")
(define/public (get-cite-close) ")")
(define/public (get-group-sep) "; ")
(define/public (get-item-sep) ", ")
(define/public (render-citation date-cite i)
(make-element
(make-style "Thyperref" (list (command-extras (list (make-label i)))))
date-cite))
(define/public (render-author+dates author dates)
(list* author " " dates))
(define (make-label i)
(string-append "autobiblab:" (number->string i)))
(define/public (bibliography-line i e)
(list (make-compound-paragraph
plain
(list (make-paragraph plain (list (make-element (make-style "label" null)
(make-label i))))
e))))
(super-new))))
(define-cite ~cite citet generate-bibliography
;; change this to small-number-style if you want the other way
#:style small-number-style
)
(define etal "et al.")
(define nrightarrow (elem #:style "mynra"))
(define (sf x) (elem #:style "sfstyle" x))
(define (parag . x) (apply elem #:style "paragraph" x))
(define (exact . items)
(make-element (make-style "relax" '(exact-chars))
items))
(define (mt-line) (parag))
(define (def #:term (term #false) . x)
(make-paragraph plain
(list
(mt-line)
(bold "Definition")
(cons (if term (element #f (list " (" (defterm term) ") ")) " ") x)
(mt-line))))
;; Format an identifier
;; Usage: @id[x]
(define (id x)
(make-element plain @format["~a" x]))
(define (todo . x*)
(make-element 'bold (cons "TODO:" x*)))
(define (second)
(make-element (make-style "relax" '(exact-chars))
"$2^\\emph{nd}$"))

143
popl-2017/intro.scrbl Normal file
View File

@ -0,0 +1,143 @@
#lang scribble/sigplan @onecolumn
@require["common.rkt" (only-in scribble/base nested)]
@title[#:tag "sec:intro"]{Introduction}
Typecheckers for polymorphic languages like Haskell incredibly wasteful.
Given an AST, they immediately throw away the rich @emph{syntax} of expression
and value forms in favor of a @emph{type} abstraction.
So whereas any novice programmer can tell that the expression @tt{(/ 1 0)}
will go wrong, the typechecker cannot because all it sees is @tt{(/ @emph{Num} @emph{Num})}.
These typecheckers are also incredibly stubborn, and cannot handle basic
forms of polymorphism that are not part of their type algebra.
For instance, the behavior of the function @tt{map} can be stated in clear
English:
@nested[@elem[#:style 'italic]{
@tt{(map proc lst ...+) → list?}
Applies @tt{proc} to the elements of the @tt{lsts} from the first elements to the last.
The @tt{proc} argument must accept the same number of arguments as the number
of supplied @tt{lsts}, and all @tt{lsts} must have the same number of elements.
The result is a list containing each result of @tt{proc} in order.
}]
But the Haskell typechecker can only validate indexed versions of @tt{map}
defined for a fixed number of lists.
Programmers are thus forced to choose between @tt{map}, @tt{zipWith}, and @tt{zipWith3}
depending on the number of lists they want to map over.@note{Maybe need a better
example than @tt{map} because polydots handle it. @tt{curry}?}
There are a few solutions to these problems. Blah blah.
They all require migrating to a new programming language or instrumenting call
sites across the program, neither of which are desirable solutions for the
working programmer.
We propose @emph{extending} a language's type system with
@emph{introspective} typing rules that capture value information as well as type
information.
Given a proof theory @exact|{$\Progn \vDash {\tt P}$}| for inferring propositions
@tt{P} from the program text @exact{$\Progn$}, the rule for division would be:
@exact|{
\begin{mathpar}
\inferrule*[]{
\Gamma; \Progn \vdash n_1 : \tnum
\\
\Gamma; \Progn \vdash n_2 : \tnum
\\\\
\Progn \vDash n_2 \neq 0
}{
\Gamma; \Progn \vdash {\tt /}~n_1~n_2 : \tnum
}
\end{mathpar}
}|
and the rule for @tt{map} would be:
@exact|{
\begin{mathpar}
\inferrule*{
\Gamma; \Progn \vdash f : \overline{\tvar{A}} \rightarrow \tvar{B}
\\
\Gamma; \Progn \vdash \overline{x} : \overline{\tlist{A}}
\\\\
\Progn \vDash {\tt length}(\overline{\tvar{A}}) = {\tt length}(\overline{\tlist{A}})
}{
\Gamma; \Progn \vdash {\tt map}~f~\overline{x} : \tlist{B}
}
\end{mathpar}
}|
These rules would augment---not replace---the existing rules for division
and @tt{map}.
In the case that no information about subterms can be inferred from the program
text, we defer to the division rule that admits runtime errors and the @tt{map}
rule that can only be called with a single list.
@; =============================================================================
@parag{Contributions}
@itemlist[
@item{
We propose ``typechecking modulo theories'' (or something):
using the text of the program to refine typechecking judgments.
}
@item{
As a proof of concept, we implement a simple theory within the Racket
macro expander and use it enhance the user experience of Typed Racket.
The implementation is just a library; we suspect Typed Clojure and TypeScript
programmers could build similar libraries using Clojure's macros and sweet.js.
}
@item{
Our Racket implementation leverages a novel class of macros.
We define the class, state proof conditions for a new macro
to enter the class, and prove our macros are in the class.
}
]
@; =============================================================================
@parag{Guarantees}
@itemlist[
@item{
Refinement of the existing type system.
Adding @exact{$\Progn \vDash$} only rejects programs that would go
wrong dynamically and/or accept programs that are ill-typed, but go
right dynamically.
}
@item{
Errors reported by our implementation are in terms of the source program,
not of expanded/transformed code.
}
]
@; =============================================================================
@parag{Applications}
This table summarizes the ICFP pearl.
We infer values from various syntactic domains and use the inferred data to
justify small program transformations.
@tabular[#:style 'boxed
#:sep @hspace[2]
#:row-properties '(bottom-border ())
#:column-properties '(right right right)
(list (list @bold{Domain} @bold{Infers} @bold{Use})
(list "format strings" "arity + type" "guard input")
(list "regexp strings" "# groups" "prove output")
(list "λ" "arity" "implement curry_i")
(list "numbers" "value" "constant folding")
(list "vectors" "size" "guard, optimize")
(list "sql schema" "types" "guard input, prove output"))]
@; =============================================================================
@parag{Lineage}
Herman and Meunier used macros for partial evaluation of string DSLs@~cite[hm-icfp-2004].
Lorenzen and Erdweg defined criteria for sane deguarings@~cite[le-popl-2016].

456
popl-2017/mathpartir.sty Normal file
View File

@ -0,0 +1,456 @@
% Mathpartir --- Math Paragraph for Typesetting Inference Rules
%
% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
%
% Author : Didier Remy
% Version : 1.2.1
% Bug Reports : to author
% Web Site : http://pauillac.inria.fr/~remy/latex/
%
% Mathpartir is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
%
% Mathpartir is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details
% (http://pauillac.inria.fr/~remy/license/GPL).
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File mathpartir.sty (LaTeX macros)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{mathpartir}
[2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
%%
%% Identification
%% Preliminary declarations
\RequirePackage {keyval}
%% Options
%% More declarations
%% PART I: Typesetting maths in paragraphe mode
%% \newdimen \mpr@tmpdim
%% Dimens are a precious ressource. Uses seems to be local.
\let \mpr@tmpdim \@tempdima
% To ensure hevea \hva compatibility, \hva should expands to nothing
% in mathpar or in inferrule
\let \mpr@hva \empty
%% normal paragraph parametters, should rather be taken dynamically
\def \mpr@savepar {%
\edef \MathparNormalpar
{\noexpand \lineskiplimit \the\lineskiplimit
\noexpand \lineskip \the\lineskip}%
}
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
\let \MathparLineskip \mpr@lineskip
\def \mpr@paroptions {\MathparLineskip}
\let \mpr@prebindings \relax
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
\def \mpr@goodbreakand
{\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
\def \mpr@and {\hskip \mpr@andskip}
\def \mpr@andcr {\penalty 50\mpr@and}
\def \mpr@cr {\penalty -10000\mpr@and}
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
\def \mpr@bindings {%
\let \and \mpr@andcr
\let \par \mpr@andcr
\let \\\mpr@cr
\let \eqno \mpr@eqno
\let \hva \mpr@hva
}
\let \MathparBindings \mpr@bindings
% \@ifundefined {ignorespacesafterend}
% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
\newenvironment{mathpar}[1][]
{$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
\noindent $\displaystyle\fi
\MathparBindings}
{\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
\newenvironment{mathparpagebreakable}[1][]
{\begingroup
\par
\mpr@savepar \parskip 0em \hsize \linewidth \centering
\mpr@prebindings \mpr@paroptions #1%
\vskip \abovedisplayskip \vskip -\lineskip%
\ifmmode \else $\displaystyle\fi
\MathparBindings
}
{\unskip
\ifmmode $\fi \par\endgroup
\vskip \belowdisplayskip
\noindent
\ignorespacesafterend}
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
%%% HOV BOXES
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
\vbox \bgroup \tabskip 0em \let \\ \cr
\halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
\egroup}
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
\box0\else \mathvbox {#1}\fi}
%% Part II -- operations on lists
\newtoks \mpr@lista
\newtoks \mpr@listb
\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
\mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
\mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
\def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
\mpr@flatten \mpr@all \mpr@to \mpr@one
\expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
\mpr@all \mpr@stripend
\ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
\ifx 1\mpr@isempty
\repeat
}
\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
\def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
%% Part III -- Type inference rules
\newif \if@premisse
\newbox \mpr@hlist
\newbox \mpr@vlist
\newif \ifmpr@center \mpr@centertrue
\def \mpr@htovlist {%
\setbox \mpr@hlist
\hbox {\strut
\ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
\unhbox \mpr@hlist}%
\setbox \mpr@vlist
\vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
\else \unvbox \mpr@vlist \box \mpr@hlist
\fi}%
}
% OLD version
% \def \mpr@htovlist {%
% \setbox \mpr@hlist
% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
% \setbox \mpr@vlist
% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
% \else \unvbox \mpr@vlist \box \mpr@hlist
% \fi}%
% }
\def \mpr@item #1{$\displaystyle #1$}
\def \mpr@sep{2em}
\def \mpr@blank { }
\def \mpr@hovbox #1#2{\hbox
\bgroup
\ifx #1T\@premissetrue
\else \ifx #1B\@premissefalse
\else
\PackageError{mathpartir}
{Premisse orientation should either be T or B}
{Fatal error in Package}%
\fi \fi
\def \@test {#2}\ifx \@test \mpr@blank\else
\setbox \mpr@hlist \hbox {}%
\setbox \mpr@vlist \vbox {}%
\if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
\let \@hvlist \empty \let \@rev \empty
\mpr@tmpdim 0em
\expandafter \mpr@makelist #2\mpr@to \mpr@flat
\if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
\def \\##1{%
\def \@test {##1}\ifx \@test \empty
\mpr@htovlist
\mpr@tmpdim 0em %%% last bug fix not extensively checked
\else
\setbox0 \hbox{\mpr@item {##1}}\relax
\advance \mpr@tmpdim by \wd0
%\mpr@tmpdim 1.02\mpr@tmpdim
\ifnum \mpr@tmpdim < \hsize
\ifnum \wd\mpr@hlist > 0
\if@premisse
\setbox \mpr@hlist
\hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
\else
\setbox \mpr@hlist
\hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
\fi
\else
\setbox \mpr@hlist \hbox {\unhbox0}%
\fi
\else
\ifnum \wd \mpr@hlist > 0
\mpr@htovlist
\mpr@tmpdim \wd0
\fi
\setbox \mpr@hlist \hbox {\unhbox0}%
\fi
\advance \mpr@tmpdim by \mpr@sep
\fi
}%
\@rev
\mpr@htovlist
\ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
\fi
\egroup
}
%%% INFERENCE RULES
\@ifundefined{@@over}{%
\let\@@over\over % fallback if amsmath is not loaded
\let\@@overwithdelims\overwithdelims
\let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
\let\@@above\above \let\@@abovewithdelims\abovewithdelims
}{}
%% The default
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
$\displaystyle {#1\mpr@over #2}$}}
\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
$\displaystyle {#1\@@atop #2}$}}
\let \mpr@fraction \mpr@@fraction
%% A generic solution to arrow
\def \mpr@@fractionaboveskip {0ex}
\def \mpr@@fractionbelowskip {0.22ex}
\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
\def \mpr@tail{#1}%
\def \mpr@body{#2}%
\def \mpr@head{#3}%
\setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
\setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
\dimen0\ht3\advance\dimen0 by \dp3\relax
\dimen0 0.5\dimen0\relax
\advance \dimen0 by \mpr@@fractionaboveskip
\setbox1=\hbox {\raise \dimen0 \box1}\relax
\dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0
\advance \dimen0 by \mpr@@fractionbelowskip
\setbox2=\hbox {\lower \dimen0 \box2}\relax
\setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}%
\dimen0=\wd0\box0
\box0 \hskip -\dimen0\relax
\hbox to \dimen0 {$%\color{blue}
\mathrel{\mpr@tail}\joinrel
\xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
$}}}
%% Old stuff should be removed in next version
\def \mpr@@nothing #1#2
{$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
\def \mpr@@reduce #1#2{\hbox
{$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
\def \mpr@@rewrite #1#2#3{\hbox
{$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
\def \mpr@empty {}
\def \mpr@inferrule
{\bgroup
\ifnum \linewidth<\hsize \hsize \linewidth\fi
\mpr@rulelineskip
\let \and \qquad
\let \hva \mpr@hva
\let \@rulename \mpr@empty
\let \@rule@options \mpr@empty
\let \mpr@over \@@over
\mpr@inferrule@}
\newcommand {\mpr@inferrule@}[3][]
{\everymath={\displaystyle}%
\def \@test {#2}\ifx \empty \@test
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
\else
\def \@test {#3}\ifx \empty \@test
\setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
\else
\setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
\fi \fi
\def \@test {#1}\ifx \@test\empty \box0
\else \vbox
%%% Suggestion de Francois pour les etiquettes longues
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
{\hbox {\RefTirName {#1}}\box0}\fi
\egroup}
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
% They are two forms
% \inferrule [label]{[premisses}{conclusions}
% or
% \inferrule* [options]{[premisses}{conclusions}
%
% Premisses and conclusions are lists of elements separated by \\
% Each \\ produces a break, attempting horizontal breaks if possible,
% and vertical breaks if needed.
%
% An empty element obtained by \\\\ produces a vertical break in all cases.
%
% The former rule is aligned on the fraction bar.
% The optional label appears on top of the rule
% The second form to be used in a derivation tree is aligned on the last
% line of its conclusion
%
% The second form can be parameterized, using the key=val interface. The
% folloiwng keys are recognized:
%
% width set the width of the rule to val
% narrower set the width of the rule to val\hsize
% before execute val at the beginning/left
% lab put a label [Val] on top of the rule
% lskip add negative skip on the right
% left put a left label [Val]
% Left put a left label [Val], ignoring its width
% right put a right label [Val]
% Right put a right label [Val], ignoring its width
% leftskip skip negative space on the left-hand side
% rightskip skip negative space on the right-hand side
% vdots lift the rule by val and fill vertical space with dots
% after execute val at the end/right
%
% Note that most options must come in this order to avoid strange
% typesetting (in particular leftskip must preceed left and Left and
% rightskip must follow Right or right; vdots must come last
% or be only followed by rightskip.
%
%% Keys that make sence in all kinds of rules
\def \mprset #1{\setkeys{mprset}{#1}}
\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
\define@key {mprset}{lineskip}[]{\lineskip=#1}
\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip}
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
\define@key {mprset}{center}[]{\mpr@centertrue}
\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\define@key {mprset}{sep}{\def\mpr@sep{#1}}
\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}}
\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}}
\newbox \mpr@right
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
\define@key {mpr}{center}[]{\mpr@centertrue}
\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{width}{\hsize #1}
\define@key {mpr}{sep}{\def\mpr@sep{#1}}
\define@key {mpr}{before}{#1}
\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
\define@key {mpr}{narrower}{\hsize #1\hsize}
\define@key {mpr}{leftskip}{\hskip -#1}
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
\define@key {mpr}{rightskip}
{\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
\define@key {mpr}{right}
{\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{RIGHT}
{\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{Right}
{\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
\newcommand \mpr@inferstar@ [3][]{\setbox0
\hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
\setbox \mpr@right \hbox{}%
$\setkeys{mpr}{#1}%
\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
\mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
\box \mpr@right \mpr@vdots$}
\setbox1 \hbox {\strut}
\@tempdima \dp0 \advance \@tempdima by -\dp1
\raise \@tempdima \box0}
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
\newcommand \mpr@err@skipargs[3][]{}
\def \mpr@inferstar*{\ifmmode
\let \@do \mpr@inferstar@
\else
\let \@do \mpr@err@skipargs
\PackageError {mathpartir}
{\string\inferrule* can only be used in math mode}{}%
\fi \@do}
%%% Exports
% Envirnonment mathpar
\let \inferrule \mpr@infer
% make a short name \infer is not already defined
\@ifundefined {infer}{\let \infer \mpr@infer}{}
\def \TirNameStyle #1{\small \textsc{#1}}
\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
\let \TirName \tir@name
\let \DefTirName \TirName
\let \RefTirName \TirName
%%% Other Exports
% \let \listcons \mpr@cons
% \let \listsnoc \mpr@snoc
% \let \listhead \mpr@head
% \let \listmake \mpr@makelist
\endinput

50
popl-2017/paper.scrbl Normal file
View File

@ -0,0 +1,50 @@
#lang scribble/sigplan @onecolumn @preprint
@(require "common.rkt")
@authorinfo["???" "???" ""]
@;@authorinfo["Ben Greenman and Stephen Chang"
@; "PLT @ Northeastern University, Boston, USA"
@; ""]
@title{Breaking the Abstraction Barrier}
@abstract{
A static type system is a compromise between precision and usability.
Improving the ability of a type system to distinguish correct and erroneous
programs typically requires that programmers restructure their code or
provide more type annotations, neither of which are desirable tasks.
This paper presents an elaboration-based technique for refining the
analysis of an existing type system on existing code
without changing the type system or the code.
As a proof of concept, we have implemented the technique as a Typed Racket library.
From the programmers' viewpoint, simply importing the library makes the type
system more perceptive---no annotations or new syntax are required.
}
@;@category["D.3.3" "Programming Languages" "Language Constructs and Features"]
@;@terms{Performance, Experimentation, Measurement}
@;@keywords{Gradual typing, performance evaluation}
@include-section{intro.scrbl}
@; @section{Code}
@;
@; Our implementation is available as a Racket package.
@; To install the library, download Racket and then run @racket[raco pkg install ???].
@; The source code is on Github at: @url["https://github.com/???/???"].
@section[#:style 'unnumbered]{Acknowledgments}
To appear
@;We thank
@;Sam Tobin-Hochstadt for reminding us that Typed Racket is macro-extensible,
@;Ryan Culpepper for divulging secrets of the Racket macro system,
@;Asumu Takikawa and Leif Andersen for rejecting some earlier designs,
@;Justin R. Slepak for teaching us the term ``textualist''.
@;ICFP reviewers for thoughtful comments
@;and Northeastern PLT for comments on an earlier draft.
@generate-bibliography[#:sec-title "References"]

11
popl-2017/pre-popl/.gitignore vendored
View File

@ -1,11 +0,0 @@
*.aux
*.bbl
*.blg
*.cls
*.log
*.out
*.pdf
*.css
*.html
*.js

2
popl-2017/pre-popl/Makefile
View File

@ -1,2 +0,0 @@
all:
scribble --html pre-popl.scrbl

56
popl-2017/pre-popl/pre-popl.scrbl
View File

@ -1,56 +0,0 @@
#lang scribble/manual
@title{Do You See What I See, in review}
Rejected at ICFP, making ready for a POPL submission.
@section{SoundX}
@subsection{What is SoundX?}
@hyperlink["http://conf.researchr.org/event/POPL-2016/popl-2016-papers-sound-type-dependent-syntactic-language-extension"]{SoundX} is a system for:
@itemlist[
@item{
@emph{Modeling} programming languages.
}
@item{
Writing type-sound extensions to a base language.
The extensions are new type derivations expressed in terms of the base language's type system.
}
]
@; TODO possible to run soundx programs?
@subsection{Key Features of SoundX}
@itemlist[
@item{
Proposes a new idea: desugarings act on type derivations are are guaranteed
to produce only well-typed terms.
}
@item{
Detailed metatheory (may be useful reference for others)
}
@item{
Models a subset of Java and implements Scala-inspired extensions.
(Everyone loves Java and nobody @emph{really} trusts Scala.)
}
]
@subsection{Lessons from SoundX}
@itemlist[
@item{
Errors must be reported in terms of the source language, not the desugared result
}
@item{
Type errors in code produced by a desugaring must reflect USER type errors,
not errors in the desugaring rules.
}
@item{
Desugarings should have access to type information.
}
]
@section{Our Contribution}

34
popl-2017/related-work.scrbl Normal file
View File

@ -0,0 +1,34 @@
#lang scribble/sigplan
@require["common.rkt"]
@title[#:tag "sec:rw"]{Related Work}
SoundX is a system for modeling programming languages and defining type-sound
extensions, e.g. defining a type derivation for @tt{let} in terms of a type
derivation for @tt{λ} expressions.
However, it is not possible to define new binding forms like @tt{letrec} if
they cannot be expressed in terms of a core language binding form.
All language extensions are desugared @emph{after} the source program is type-checked
and all desugarings are @emph{guaranteed} to produce only well-typed terms.
For an extended example, the authors model a subset of Java and extend the model
with Scala-style for comprehensions.
Type correctness is a relatively shallow notion of correctness for a language
extension, but still their ideas are pretty cool.
We propose a deeper notion of correctness for our syntactic transformations, but
keep in mind SoundX's criteria:
@itemlist[
@item{
Errors must be reported in terms of the source language, not the desugared result
}
@item{
Type errors in code produced by a desugaring must reflect USER type errors,
not errors in the desugaring rules.
}
@item{
Desugarings should have access to type information.
}
]
Though we fail on the third point.

51
popl-2017/texstyle.tex Normal file
View File

@ -0,0 +1,51 @@
% Better horizontal rules
\usepackage{booktabs}
\usepackage{listings}
\usepackage{stmaryrd}
\usepackage{mathpartir}
\lstset{language=ML}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage{multicol}
\usepackage{tikz}
% Override Scribble's default SecRef to numeric only
\renewcommand{\SecRef}[2]{~#1}
\hypersetup{hidelinks}
\usepackage[scaled=0.95]{zi4}
\usepackage[T1]{fontenc}
% For bib style
\newcommand{\Thyperref}[2]{\hyperref[#2]{#1}}
%% To show overfull, turn off for production!!!
\overfullrule=1mm
%% balance last page columns
\usepackage{flushend}
%% for figure 2
\let\ulcorner\relax
\let\urcorner\relax
\let\llcorner\relax
\let\lrcorner\relax
\usepackage{amssymb}
\newcommand{\interp}{\mathcal{I}}
\newcommand{\untyped}[1]{{\,#1}_\flat}
\newcommand{\trans}{\mathcal{T}}
\newcommand{\elab}{\mathcal{E}}
\newcommand{\elabfe}[1]{\llbracket #1 \rrbracket}
\newcommand{\elabf}{\elabfe{\cdot}}
\newcommand{\subt}{\mathbf{<:\,}}
\newcommand{\tos}{\mathsf{types_of_spec}}
\newcommand{\trt}[1]{\emph{#1}}
\newcommand{\tprintf}{\mathsf{t_printf}}
\newcommand{\mod}[1]{$\mathsf{#1}$}
\newcommand{\evalsto}{\RktMeta{}\RktSym{=={\Stttextmore}}\RktMeta{}\mbox{\hphantom{\Scribtexttt{x}}}}
\newcommand{\tvar}[1]{\mathsf{#1}}
\newcommand{\tint}{\tvar{Int}}
\newcommand{\tnum}{\tvar{Num}}
\newcommand{\tlist}[1]{\tvar{List~#1}}
\newcommand{\Progn}{\mathcal{P}}