diff --git a/popl-2017/Makefile b/popl-2017/Makefile index 89d77c6..b7bb608 100644 --- a/popl-2017/Makefile +++ b/popl-2017/Makefile @@ -1,14 +1,14 @@ PAPER=paper -all: setup ${PAPER}.pdf +all: ${PAPER}.pdf compiled/pearl_scrbl.zo: *.rkt *.scrbl raco make -v $(PAPER).scrbl -${PAPER}.pdf: pkg compiled/${PAPER}_scrbl.zo texstyle.tex +${PAPER}.pdf: pkg setup texstyle.tex scribble ++extra mathpartir.sty ++style texstyle.tex --pdf $(PAPER).scrbl -${PAPER}.tex: pkg compiled/${PAPER}_scrbl.zo texstyle.tex +${PAPER}.tex: pkg setup texstyle.tex scribble ++style texstyle.tex --latex $(PAPER).scrbl pkg: diff --git a/popl-2017/OUTLINE.md b/popl-2017/OUTLINE.md new file mode 100644 index 0000000..66be4db --- /dev/null +++ b/popl-2017/OUTLINE.md @@ -0,0 +1,47 @@ +Outline of paper +--- + + +0 intro.scrbl +--- +types, abstraction, +syntax extensions, +true refinement, +other promises + + +1 background.scrbl +--- +define typed racket, +explain macro API without the word "macro", +goals for extensions +correctness for extensions + + +2. examples.scrbl +--- +carefully explain 2 extensions +state guarantees +prove properties +evaluations + + +3. discussion.scrbl +--- +limits of the extensions (need a value), +suggestions to overcome limits (assertions, better analysis), +even more extensions + implications + + +4. friends.scrbl +--- +how to implement in +- typed clojure +- scala (macros or LMS) +- javascript +rust will be difficult + + +5. ending +--- + diff --git a/popl-2017/background.scrbl b/popl-2017/background.scrbl new file mode 100644 index 0000000..e8701d7 --- /dev/null +++ b/popl-2017/background.scrbl @@ -0,0 +1,21 @@ +#lang scribble/sigplan @onecolumn + +@require["common.rkt"] + +@title[#:tag "sec:background"]{If You Know What I Mean} + +% - language = untyped, in the end we're doing machine instructions +% - here is what a function does, here is my notation for describing such things +% - easy to make mistakes, so we have type systems to detect errors +% - run type system statically but it's not as good as running the program ya know +% - so, abstraction +% - we want to refine, here is what refinement means + +% this section will die soon but until then here's ideas + + +A programming language is used to describe a sequence of instructions that + may be carried out by a machine. + + + diff --git a/popl-2017/conclusion.scrbl b/popl-2017/conclusion.scrbl new file mode 100644 index 0000000..5fad408 --- /dev/null +++ b/popl-2017/conclusion.scrbl @@ -0,0 +1,10 @@ +#lang scribble/sigplan @onecolumn + +@require["common.rkt"] + +@title[#:tag "sec:conclusion"]{Out of Time} + +My old clock used to tell the time +and subdivide diurnity; +but now it's lost both hands and chime +and only tells eternity. diff --git a/popl-2017/discussion.scrbl b/popl-2017/discussion.scrbl new file mode 100644 index 0000000..14775f5 --- /dev/null +++ b/popl-2017/discussion.scrbl @@ -0,0 +1,10 @@ +#lang scribble/sigplan @onecolumn + +@require["common.rkt"] + +@title[#:tag "sec:discussion"]{Making Sense} + +Life makes senses +and who could doubt it, +if we have +no doubt about it. diff --git a/popl-2017/examples.scrbl b/popl-2017/examples.scrbl new file mode 100644 index 0000000..4af196f --- /dev/null +++ b/popl-2017/examples.scrbl @@ -0,0 +1,10 @@ +#lang scribble/sigplan @onecolumn + +@require["common.rkt"] + +@title[#:tag "sec:examples"]{Small Things and Great} + +He that lets +the small things bind him +leaves the great +undone behind him. diff --git a/popl-2017/friends.scrbl b/popl-2017/friends.scrbl new file mode 100644 index 0000000..3031d81 --- /dev/null +++ b/popl-2017/friends.scrbl @@ -0,0 +1,10 @@ +#lang scribble/sigplan @onecolumn + +@require["common.rkt"] + +@title[#:tag "sec:friends"]{Those Who Know} + +Those who always +know what’s best +are +a universal pest. diff --git a/popl-2017/intro.scrbl b/popl-2017/intro.scrbl index 6eb384e..ca42932 100644 --- a/popl-2017/intro.scrbl +++ b/popl-2017/intro.scrbl @@ -1,10 +1,44 @@ #lang scribble/sigplan @onecolumn - @require["common.rkt" (only-in scribble/base nested)] +@title[#:tag "sec:intro"]{Type Eleborators Need APIs} + +The implementations of richhly typed programming languages tend to employ +an elaboration pass. As the elaborator traverses the (parsed) synatx, it +simultaneously reconstructs types, checks their consistency according to +the underlying type theory, replaces many of the surface-syntax constructs +with constructs from the kernel language, and inserts type information to +create a (n often) fully annotated representation. + +Some (implementations of) programming languages also support a way to +programmatically direct the elaborator. For example, Rust and Scala come +with compiler plug-ins. Typed Racket and Types Clojure inherit the macro +mechanisms of their parent languages. + +In this paper, we show that such APIs allow programmers to tailor the +underlying type theories to their needs and that such tailorings look +highly promising (section 2). The ``tailor'' can ... correctness ... + + For convenience, we use Typed Racket and its +API to the elaborator (section 3). To illustrate the usefulness of the +idea, we implement two tailorings. The first one---chosen for the wide +familiarity of the domain---enriches the type-checking of +vector-referencing operations (section 4). The second example explains how +the implementor of a string-based embedded DSL---a regexp-matching +DSL---may tailor the types of the interpretation function (section 5). Our +evaluation validate that both tailorings reduce the number of casts that +the programmer or the elaborator have to insert. + + + + + + + + + -@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 diff --git a/popl-2017/paper.scrbl b/popl-2017/paper.scrbl index e3f1e5d..4762140 100644 --- a/popl-2017/paper.scrbl +++ b/popl-2017/paper.scrbl @@ -2,38 +2,38 @@ @(require "common.rkt") -@authorinfo["???" "???" ""] -@;@authorinfo["Ben Greenman and Stephen Chang" -@; "PLT @ Northeastern University, Boston, USA" -@; ""] - -@title{Breaking the Abstraction Barrier} +@title{Tailoring Type Theories (T.T.T)} +@authorinfo["Piet Hein" "Dutchman" "piet at hein.com"] @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. +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} +@; See OUTLINE.md for explanation @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/???/???"]. +@include-section{background.scrbl} +@include-section{examples.scrbl} +@include-section{discussion.scrbl} +@include-section{friends.scrbl} +@include-section{related-work.scrbl} +@include-section{conclusion.scrbl} @section[#:style 'unnumbered]{Acknowledgments} diff --git a/popl-2017/related-work.scrbl b/popl-2017/related-work.scrbl index bc2fb16..bdec2e1 100644 --- a/popl-2017/related-work.scrbl +++ b/popl-2017/related-work.scrbl @@ -1,8 +1,8 @@ -#lang scribble/sigplan +#lang scribble/sigplan @onecolumn + @require["common.rkt"] - -@title[#:tag "sec:rw"]{Related Work} +@title[#:tag "sec:related-work"]{Experts} 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