Remove old prototypes

.gitignore

@@ -1,28 +1,4 @@
-# Generated by Cargo
-# will have compiled files and executables
-/target/
-
-# Remove Cargo.lock from gitignore if creating an executable, leave it for libraries
-# More information here http://doc.crates.io/guide.html#cargotoml-vs-cargolock
-Cargo.lock
-target
-Cargo.lock
-
 *~
-/node_modules
-/redex/compiled
-
-# OCaml & BS
-*.cmi
-*.cmo
-*.cmj
-*.cmt
-*.cmti
-*.js
-/bs/node_modules/
-/bs/test
-/bs/_build
-/bs/bsconfig.json
-Parser.ml
-Parser.mli
-Lexer.ml
+/compiled
+README.html
+SweetT.zip

README.md

@@ -1 +1,322 @@
-# judgmental-resugaring
+# SweetT: Resugaring Type Systems
+
+This is the artifact for the paper "Inferring Type Rules for Syntactic
+Sugar" by Justin Pombrio and Shriram Krishnamurthi.
+
+------
+
+Type systems and syntactic sugar are both valuable to programmers, but
+sometimes at odds. While sugar is a valuable mechanism for
+implementing realistic languages, the expansion process obscures
+program source structure. As a result, type errors can reference terms
+the programmers did not write (and even constructs they do not know),
+baffling them. The language developer must also manually construct
+type rules for the sugars, to give a typed account of the surface
+language. We address these problems by presenting a process for
+automatically reconstructing type rules for the surface language using
+rules for the core. We have implemented this theory, and show several
+interesting case studies.
+
+
+## Installation Instructions
+
+1. Install [DrRacket, version 6.10.1](https://download.racket-lang.org/all-versions.html).
+   SweetT should also work fine with later versions of DrRacket. If it
+   does not, please open a github issue and I'll see if I can fix it.
+2. If you're on Linux, you can start DrRacket by running
+   `/usr/racket/bin/drracket`. You can also add it to your path:
+
+         PATH=/usr/racket/bin:$PATH
+         export PATH
+3. Try running the `arith.rkt` test in the `examples` directory by
+   opening it in DrRacket and hitting "Run". You should see a popup 
+   showing resugared type rules for the sugars defined in the file.
+   You can browse them by clicking "Prev Derivation" and "Next Derivation".
+
+## Usage Guide
+
+SweetT takes as input:
+
+1. A grammar for a core language,
+2. A set of type rules for that core language, and
+3. A set of desugaring rules that target that core language.
+
+And it produces a set of type rules for the sugars.
+
+To see how to use SweetT, let's walk through a small demo (found in
+`examples/demo.rkt`):
+
+    #lang racket
+
+    (require redex)
+    (require "../resugar.rkt")
+
+    ;; This is a super-simple resugaring demo to demonstrate the API.
+
+    (define-resugarable-language demo
+      #:keywords(if true false Bool)
+      (e ::= ....
+         (if e e e))
+      (v ::= ....
+         true
+         false)
+      (t ::= ....
+         Bool)
+      (s ::= ....
+         (not s)))
+
+    (define-core-type-system demo
+      [(⊢ Γ e_1 t_1)
+       (⊢ Γ e_2 t_2)
+       (⊢ Γ e_3 t_3)
+       (con (t_1 = Bool))
+       (con (t_2 = t_3))
+       ------ t-if
+       (⊢ Γ (if e_1 e_2 e_3) t_3)]
+
+      [------ t-true
+       (⊢ Γ true Bool)]
+
+      [------ t-false
+       (⊢ Γ false Bool)])
+
+    (define rule_not
+      (ds-rule "not" #:capture()
+               (not ~a)
+               (if ~a false true)))
+
+    (view-sugar-type-rules demo ⊢ (list rule_not))
+
+The first line says that this file is written in the Racket language,
+since DrRacket is an editor for many different languages. The next two
+lines say that we're going to use
+[redex](https://docs.racket-lang.org/redex/), which SweetT is built
+on, and `resugar.rkt`, which is the main import for SweetT.
+
+    #lang racket
+
+    (require redex)
+    (require "../resugar.rkt")
+
+Next we define the language with `define-resugarable-language`. This
+takes a language name (`demo`), a list of keywords (to help SweetT
+tell the difference between a keyword and a variable), and a set of
+extensions to productions in the language grammar. (This builds
+upon a very basic language defined in `base-lang.rkt`; this base
+language contains things like the `calc-type` feature described in the
+paper.) In this case, we extend expressions `e` with `if` expressions,
+values `v` with `true` and `false`, types `t` with `Bool`, and surface
+expressions `s` with `(not s)`, which will be a sugar.
+
+    (define-resugarable-language demo
+      #:keywords(if true false Bool)
+      (e ::= ....
+         (if e e e))
+      (v ::= ....
+         true
+         false)
+      (t ::= ....
+         Bool)
+      (s ::= ....
+         (not s)))
+
+Next we define the type system for the `demo` language, using
+[Redex's type judgement notation](https://docs.racket-lang.org/redex/redex2015.html#%28part._tue-aft%29).
+There is one important restriction, described in the paper: the rules
+must be "written using equality constraints: if two premises in a type
+rule would traditionally describe equality by repeating a type
+variable, SweetT instead requires that the rule be written using two
+different type variables, with an equality constraint between them -
+thus making the unification explicit." Thus in the `t-if` rule, we
+write the equality constraints `(con (t_1 = Bool))` and `(con (t_2 =
+t_3))` (`con` stands for "constraint").
+
+    (define-core-type-system demo
+      [(⊢ Γ e_1 t_1)
+       (⊢ Γ e_2 t_2)
+       (⊢ Γ e_3 t_3)
+       (con (t_1 = Bool))
+       (con (t_2 = t_3))
+       ------ t-if
+       (⊢ Γ (if e_1 e_2 e_3) t_3)]
+
+      [------ t-true
+       (⊢ Γ true Bool)]
+
+      [------ t-false
+       (⊢ Γ false Bool)])
+
+Now we're ready to write a desugaring rule. This is done with the
+`ds-rule` function, which takes a rule name (`not`), a set of
+variables to capture (typically the empty set), a left-hand-side `(not
+~a`, and a right-hand-side `(if ~a false true)`. Pattern variables are
+written with a tilde, so `~a` is a pattern variable. This rule does
+not contain any regular variables, but they would be written without a
+tilde. Since `false` and `true` appeared in the keyword list above,
+they are interpreted as keywords rather than variables.
+
+    (define rule_not
+      (ds-rule "not" #:capture()
+               (not ~a)
+               (if ~a false true)))
+
+Finally, we can resugar this rule and view the resulting type rules.
+`view-sugar-type-rules` expects a language name (`demo`), a type judgement
+relation (which will always be `⊢`), and a list of rewrite rules to
+resugar `(list rule_not)`. It then displays the inferred type rule for
+`not` in a popup.
+
+    (view-sugar-type-rules demo ⊢ (list rule_not))
+
+To see the type derivation that led to this type rule, use
+`view-sugar-derivations` instead.
+
+### How to Read the Type Rules
+
+Basics:
+
+    (bind x t Γ)  means  x:t, Γ
+    ~A            means  a pattern variable
+    A             means  a variable (or type variable)
+
+Calctype (described in section 4.1):
+
+    (calctype e as t in e2)  means  assert that 'e' has type 't', and evaluate e2
+
+Sequences (described in section 4.5):
+
+    ϵ            means an empty list or empty record
+    (cons e e*)  means cons e onto the front of the sequence e*
+
+Not described in paper:
+
+    (field x e eRec)          means add the field x:e to record eRec
+    (bind* x* t* Γ)           means  x_1:t_1, ..., x_n:t_n, Γ
+    (calctype* e* as t* in e) means  (calctype e_1 as t_1 in ... (calctype e_n as t_n in e) ...)
+
+
+# Artifact Evaluation Instructions
+
+1. Follow the installation instructions above.
+2. Get a sense of what SweetT is for and how it works by reading the
+   paper (section 2 in particular should be a good overview), and by
+   looking at the "Usage Guide" above.
+3. Check that SweetT conforms to the claims of the paper. We walk
+   through all of the claims we believe the paper makes next, and
+   describe how to verify them.
+
+## Evaluation: Type Systems (section 6.1 from the paper)
+
+There are test cases for SweetT on the following type system features
+from TAPL (Types and Programming Languages, Benjamin Pierce). These
+can be found in the `examples` directory.
+
+    booleans    - TAPL pg.93
+    numbers     - TAPL pg.93
+    stlc        - TAPL pg.103
+    unit        - TAPL pg.119
+    ascription  - TAPL pg.122
+    let         - TAPL pg.124
+    pairs       - TAPL pg.126
+    tuples      - TAPL pg.128
+    records     - TAPL pg.129
+    sums        - TAPL pg.132 (uniq typing on pg. 135 irrelevant w/ T.I.)
+    variants    - TAPL pg.136
+    fixpoint    - TAPL pg.144
+    lists       - TAPL pg.147
+    exceptions  - TAPL pg.175 (skipping the tiny pre-version)
+    alg-subty   - TAPL pg.212
+    existential - TAPL pg.366
+
+Instead of having 16 separate type systems each with one feature
+(which would be unweildy), we grouped these features into five type
+systems:
+
+    examples/arith.rkt:
+      booleans, numbers, unit
+    examples/lambda.rkt:
+      lambda (i.e. stlc), unit, ascription, fixpoint
+    examples/data.rkt:
+      let, pairs, tuples, records, sums, variants, lists, exceptions
+    examples/exists.rkt:
+      existentials
+    examples/subtype.rkt:
+      algorithmic subtyping
+
+We say in the paper: "We tested each type system by picking one or
+more sugars that made use of its features, resugaring them to obtain
+type rules, and validating the resulting type rules by hand. All of
+them resugared successfully. The full version of the paper will
+provide an appendix with complete details."
+
+You can verify that:
+
+1. For each type system feature from TAPL (e.g. booleans), the example
+   file that includes that feature has a sugar that uses it
+   (e.g. `examples/arith.rkt` is the file that implements booleans,
+   and it contains a `not` sugar that uses booleans).
+2. Each of the sugars given has the type rule that you would expect it
+   to have.
+
+
+
+## Case Studies (section 6.2 from the paper)
+
+For each sugar in the case studies, you can verify that:
+
+1. The sugar definition matches what the paper says. (Note that the
+   syntax will be superficially different, however. The implementation
+   must represent everything as Redex terms which, e.g., require every
+   AST node to be wrapped in parentheses. In contrast, the paper uses
+   whichever syntax we think is most appropriate, e.g. the syntax used
+   in TAPL for the TAPL examples, or Haskell syntax for the Haskell
+   examples.)
+2. The resugared type rule matches what's shown in the paper.
+3. When the paper also shows the full type derivation that led to that
+   type rule, the resugared type rule matches what's shown in the
+   paper.
+
+### Foreach
+
+The `foreach` loop can be found as the `rule_foreach` sugar given in
+`examples/data.rkt`. The paper presents this sugar in psuedocode that
+we believed would be a bit easier to read than the `rule_foreach` code
+(which had to be expressed as a Redex term), but the correspondence
+should be clear.
+
+### Haskell List Comprehensions
+
+The Haskell List Comprehension sugars can also be found in
+`examples/data.rkt`. They are named `rule_hlc-guard`,
+`rule_hlc-gen`, and `rule_hlc-let`. The syntax mapping between the
+Redex terms (in the implementation) and Haskell (in the paper) is:
+
+    Redex         Haskell
+    ~~~~~         ~~~~~~~
+    [e | Q]       (hlc e Q)
+    b, Q          (hlc/guard b Q)
+    p <- l, Q     (hlc/gen p l Q)
+    let x = e, Q  (hlc/let x = e in Q)
+
+### Newtype
+
+The newtype sugar is named `rule_newtype` and can be found in
+`examples/exists.rkt`. The syntax matches the paper quite closely.
+
+### Figure 6: Letrec, λret, and Upcast
+
+The "upcast" example is named `rule_upcast` in `examples/subtype.rkt`.
+
+The "letrec" example is named `rule_letrec` in `examples/lambda.rkt`.
+
+The "rule_λret" example is named `rule_λret` in `examples/data.rkt`.
+
+### Examples in the paper
+
+Additionally, there are a few examples of type resugaring described in
+prose in the paper:
+
+* `t-and` from section 2 is tested in `examples/arith.rkt`.
+* `t-or` from section 2 is tested in `examples/arith.rkt`.
+* `sugar-or-1` and `sugar-or-2` from section 4.5 are tested in
+  `examples/multi.rkt`.