commit c1ab7311aff1bc7b2f9a4c4881616b16fb664be6
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Mon, 20 Mar 2017 16:08:41 +0100
Initial commit.
Diffstat:
15 files changed, 1563 insertions(+), 0 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,6 @@
+*~
+\#*
+.\#*
+.DS_Store
+compiled/
+/doc/
diff --git a/.travis.yml b/.travis.yml
@@ -0,0 +1,63 @@
+language: c
+
+# Based from: https://github.com/greghendershott/travis-racket
+
+# Optional: Remove to use Travis CI's older infrastructure.
+sudo: false
+
+env:
+ global:
+ # Supply a global RACKET_DIR environment variable. This is where
+ # Racket will be installed. A good idea is to use ~/racket because
+ # that doesn't require sudo to install and is therefore compatible
+ # with Travis CI's newer container infrastructure.
+ - RACKET_DIR=~/racket
+ matrix:
+ # Supply at least one RACKET_VERSION environment variable. This is
+ # used by the install-racket.sh script (run at before_install,
+ # below) to select the version of Racket to download and install.
+ #
+ # Supply more than one RACKET_VERSION (as in the example below) to
+ # create a Travis-CI build matrix to test against multiple Racket
+ # versions.
+ #- RACKET_VERSION=6.0
+ #- RACKET_VERSION=6.1
+ #- RACKET_VERSION=6.1.1
+ #- RACKET_VERSION=6.2
+ #- RACKET_VERSION=6.3
+ #- RACKET_VERSION=6.4
+ #- RACKET_VERSION=6.5
+ #- RACKET_VERSION=6.6
+ #- RACKET_VERSION=6.7
+ - RACKET_VERSION=6.8
+ - RACKET_VERSION=HEAD
+
+matrix:
+ allow_failures:
+# - env: RACKET_VERSION=HEAD
+ fast_finish: true
+
+before_install:
+- git clone https://github.com/greghendershott/travis-racket.git ~/travis-racket
+- cat ~/travis-racket/install-racket.sh | bash # pipe to bash not sh!
+- export PATH="${RACKET_DIR}/bin:${PATH}" #install-racket.sh can't set for us
+
+install:
+ - raco pkg install --deps search-auto
+
+before_script:
+
+# Here supply steps such as raco make, raco test, etc. You can run
+# `raco pkg install --deps search-auto` to install any required
+# packages without it getting stuck on a confirmation prompt.
+script:
+ - raco test -x -p thesis
+ - raco setup --check-pkg-deps --pkgs thesis
+ - make
+
+#after_success:
+# - raco pkg install --deps search-auto cover cover-coveralls
+# - raco cover -b -f coveralls -d $TRAVIS_BUILD_DIR/coverage .
+
+after_success:
+- sh ./auto-push-gh-pages.sh
diff --git a/LICENSE-more.md b/LICENSE-more.md
@@ -0,0 +1,24 @@
+anaphoric
+Copyright (c) 2016-2017 Georges Dupéron
+
+
+
+This package is in distributed under the Creative Commons CC0 license
+https://creativecommons.org/publicdomain/zero/1.0/, as specified by
+the LICENSE.txt file.
+
+
+
+The CC0 license is equivalent to a dedication to the Public Domain
+in most countries, but is also effective in countries which do not
+recognize explicit dedications to the Public Domain.
+
+
+
+In order to avoid any potential licensing issues, this package is explicitly
+distributed under the Creative Commons CC0 license
+https://creativecommons.org/publicdomain/zero/1.0/, or under the GNU Lesser
+General Public License (LGPL) https://opensource.org/licenses/LGPL-3.0, or
+under the Apache License Version 2.0
+https://opensource.org/licenses/Apache-2.0, or under the MIT license
+https://opensource.org/licenses/MIT, at your option.
diff --git a/LICENSE.txt b/LICENSE.txt
@@ -0,0 +1,116 @@
+CC0 1.0 Universal
+
+Statement of Purpose
+
+The laws of most jurisdictions throughout the world automatically confer
+exclusive Copyright and Related Rights (defined below) upon the creator and
+subsequent owner(s) (each and all, an "owner") of an original work of
+authorship and/or a database (each, a "Work").
+
+Certain owners wish to permanently relinquish those rights to a Work for the
+purpose of contributing to a commons of creative, cultural and scientific
+works ("Commons") that the public can reliably and without fear of later
+claims of infringement build upon, modify, incorporate in other works, reuse
+and redistribute as freely as possible in any form whatsoever and for any
+purposes, including without limitation commercial purposes. These owners may
+contribute to the Commons to promote the ideal of a free culture and the
+further production of creative, cultural and scientific works, or to gain
+reputation or greater distribution for their Work in part through the use and
+efforts of others.
+
+For these and/or other purposes and motivations, and without any expectation
+of additional consideration or compensation, the person associating CC0 with a
+Work (the "Affirmer"), to the extent that he or she is an owner of Copyright
+and Related Rights in the Work, voluntarily elects to apply CC0 to the Work
+and publicly distribute the Work under its terms, with knowledge of his or her
+Copyright and Related Rights in the Work and the meaning and intended legal
+effect of CC0 on those rights.
+
+1. Copyright and Related Rights. A Work made available under CC0 may be
+protected by copyright and related or neighboring rights ("Copyright and
+Related Rights"). Copyright and Related Rights include, but are not limited
+to, the following:
+
+ i. the right to reproduce, adapt, distribute, perform, display, communicate,
+ and translate a Work;
+
+ ii. moral rights retained by the original author(s) and/or performer(s);
+
+ iii. publicity and privacy rights pertaining to a person's image or likeness
+ depicted in a Work;
+
+ iv. rights protecting against unfair competition in regards to a Work,
+ subject to the limitations in paragraph 4(a), below;
+
+ v. rights protecting the extraction, dissemination, use and reuse of data in
+ a Work;
+
+ vi. database rights (such as those arising under Directive 96/9/EC of the
+ European Parliament and of the Council of 11 March 1996 on the legal
+ protection of databases, and under any national implementation thereof,
+ including any amended or successor version of such directive); and
+
+ vii. other similar, equivalent or corresponding rights throughout the world
+ based on applicable law or treaty, and any national implementations thereof.
+
+2. Waiver. To the greatest extent permitted by, but not in contravention of,
+applicable law, Affirmer hereby overtly, fully, permanently, irrevocably and
+unconditionally waives, abandons, and surrenders all of Affirmer's Copyright
+and Related Rights and associated claims and causes of action, whether now
+known or unknown (including existing as well as future claims and causes of
+action), in the Work (i) in all territories worldwide, (ii) for the maximum
+duration provided by applicable law or treaty (including future time
+extensions), (iii) in any current or future medium and for any number of
+copies, and (iv) for any purpose whatsoever, including without limitation
+commercial, advertising or promotional purposes (the "Waiver"). Affirmer makes
+the Waiver for the benefit of each member of the public at large and to the
+detriment of Affirmer's heirs and successors, fully intending that such Waiver
+shall not be subject to revocation, rescission, cancellation, termination, or
+any other legal or equitable action to disrupt the quiet enjoyment of the Work
+by the public as contemplated by Affirmer's express Statement of Purpose.
+
+3. Public License Fallback. Should any part of the Waiver for any reason be
+judged legally invalid or ineffective under applicable law, then the Waiver
+shall be preserved to the maximum extent permitted taking into account
+Affirmer's express Statement of Purpose. In addition, to the extent the Waiver
+is so judged Affirmer hereby grants to each affected person a royalty-free,
+non transferable, non sublicensable, non exclusive, irrevocable and
+unconditional license to exercise Affirmer's Copyright and Related Rights in
+the Work (i) in all territories worldwide, (ii) for the maximum duration
+provided by applicable law or treaty (including future time extensions), (iii)
+in any current or future medium and for any number of copies, and (iv) for any
+purpose whatsoever, including without limitation commercial, advertising or
+promotional purposes (the "License"). The License shall be deemed effective as
+of the date CC0 was applied by Affirmer to the Work. Should any part of the
+License for any reason be judged legally invalid or ineffective under
+applicable law, such partial invalidity or ineffectiveness shall not
+invalidate the remainder of the License, and in such case Affirmer hereby
+affirms that he or she will not (i) exercise any of his or her remaining
+Copyright and Related Rights in the Work or (ii) assert any associated claims
+and causes of action with respect to the Work, in either case contrary to
+Affirmer's express Statement of Purpose.
+
+4. Limitations and Disclaimers.
+
+ a. No trademark or patent rights held by Affirmer are waived, abandoned,
+ surrendered, licensed or otherwise affected by this document.
+
+ b. Affirmer offers the Work as-is and makes no representations or warranties
+ of any kind concerning the Work, express, implied, statutory or otherwise,
+ including without limitation warranties of title, merchantability, fitness
+ for a particular purpose, non infringement, or the absence of latent or
+ other defects, accuracy, or the present or absence of errors, whether or not
+ discoverable, all to the greatest extent permissible under applicable law.
+
+ c. Affirmer disclaims responsibility for clearing rights of other persons
+ that may apply to the Work or any use thereof, including without limitation
+ any person's Copyright and Related Rights in the Work. Further, Affirmer
+ disclaims responsibility for obtaining any necessary consents, permissions
+ or other rights required for any use of the Work.
+
+ d. Affirmer understands and acknowledges that Creative Commons is not a
+ party to this document and has no duty or obligation with respect to this
+ CC0 or use of the Work.
+
+For more information, please see
+<http://creativecommons.org/publicdomain/zero/1.0/>
diff --git a/Makefile b/Makefile
@@ -0,0 +1,3 @@
+.PHONY: all
+all:
+ raco setup --doc-pdf doc/pdf/ --pkgs thesis
diff --git a/README.md b/README.md
@@ -0,0 +1,3 @@
+thesis
+======
+README text here.
diff --git a/auto-push-gh-pages.sh b/auto-push-gh-pages.sh
@@ -0,0 +1,36 @@
+#!/bin/sh
+set -e
+set -x
+if test "$(git config remote.origin.url)" != "https://github.com/jsmaniac/phc-thesis.git"
+ echo "Not on official repo, will not deploy gh-pages."
+elif test "$TRAVIS_PULL_REQUEST" != "false"; then
+ echo "This is a Pull Request, will not deploy gh-pages."
+elif test "$TRAVIS_BRANCH" = "master"; then
+ echo "Not on master branch, will not deploy gh-pages."
+elif test -z "${encrypted_1b66487e02e5_key:-}" -o -z "${encrypted_1b66487e02e5_iv:-}"; then
+ echo "Travis CI secure environment variables are unavailable, will not deploy gh-pages."
+else
+ echo "Automatic push to gh-pages"
+
+ # Git configuration:
+ git config --global user.name "$(git log --format="%aN" HEAD -1) (Travis CI automatic commit)"
+ git config --global user.email "(git log --format="%aE" HEAD -1)"
+
+ # SSH configuration
+ if test openssl aes-256-cbc -K $encrypted_1b66487e02e5_key -iv $encrypted_1b66487e02e5_iv -in travis-deploy-key-id_rsa.enc -out travis-deploy-key-id_rsa -d >/dev/null 2>&1; then
+ echo "Error while decrypting key."
+ fi
+ chmod 600 travis-deploy-key-id_rsa
+ eval `ssh-agent -s`
+ ssh-add travis-deploy-key-id_rsa
+
+ if test -e $TRAVIS_GH_PAGES_DIR; then rm -rf $TRAVIS_GH_PAGES_DIR; fi
+ mv -i doc $TRAVIS_GH_PAGES_DIR
+ git init $TRAVIS_GH_PAGES_DIR
+ #rm -f $TRAVIS_GH_PAGES_DIR/MathJax
+ #mkdir $TRAVIS_GH_PAGES_DIR/MathJax
+ #echo 'document.write("<script src=\"http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=default\"></script>");' > $TRAVIS_GH_PAGES_DIR/MathJax/MathJax.js
+ touch $TRAVIS_GH_PAGES_DIR/.nojekyll
+ (cd $TRAVIS_GH_PAGES_DIR && git add -A . && git commit -m "Auto-publish to gh-pages")
+ (cd $TRAVIS_GH_PAGES_DIR; git push --force --quiet "https://${GH_TOKEN}@github.com/jsmaniac/phc-thesis.git" master:gh-pages >/dev/null 2>&1 || true) >/dev/null 2>&1 # redirect to /dev/null to avoid showing credentials.
+fi
+\ No newline at end of file
diff --git a/info.rkt b/info.rkt
@@ -0,0 +1,14 @@
+#lang info
+(define collection "thesis")
+(define deps '("base"
+ "rackunit-lib"))
+(define build-deps '("scribble-lib"
+ "racket-doc"
+ "typed-racket-lib"
+ "at-exp-lib"
+ "scribble-enhanced"
+ "scribble-math"))
+(define scribblings '(("scribblings/thesis.scrbl" ())))
+(define pkg-desc "Description Here")
+(define version "0.0")
+(define pkg-authors '(georges))
diff --git a/main.rkt b/main.rkt
@@ -0,0 +1,35 @@
+#lang racket/base
+
+(module+ test
+ (require rackunit))
+
+;; Notice
+;; To install (from within the package directory):
+;; $ raco pkg install
+;; To install (once uploaded to pkgs.racket-lang.org):
+;; $ raco pkg install <<name>>
+;; To uninstall:
+;; $ raco pkg remove <<name>>
+;; To view documentation:
+;; $ raco docs <<name>>
+;;
+;; For your convenience, we have included a LICENSE.txt file, which links to
+;; the GNU Lesser General Public License.
+;; If you would prefer to use a different license, replace LICENSE.txt with the
+;; desired license.
+;;
+;; Some users like to add a `private/` directory, place auxiliary files there,
+;; and require them in `main.rkt`.
+;;
+;; See the current version of the racket style guide here:
+;; http://docs.racket-lang.org/style/index.html
+
+;; Code here
+
+(module+ test
+ ;; Tests to be run with raco test
+ )
+
+(module+ main
+ ;; Main entry point, executed when run with the `racket` executable or DrRacket.
+ )
diff --git a/scribblings/abbreviations.rkt b/scribblings/abbreviations.rkt
@@ -0,0 +1,27 @@
+#lang at-exp racket
+(provide typedracket Typedracket csharp CAML CLOS NIT CPP)
+
+(require scribble/base
+ scribble/core
+ scribble/latex-properties
+ scriblib/render-cond)
+
+(define csharp-tex-addition
+ (string->bytes/utf-8
+ @string-append{
+ \def\csharpAbbrev#1{
+ \texorpdfstring{C\kern0.1ex\protect\raisebox{0.3ex}{\smaller $\#$}}{C\#}}}))
+
+(define csharp
+ (cond-element
+ [html "C#"]
+ [latex (elem #:style (style "csharpAbbrev"
+ (list (tex-addition csharp-tex-addition))) "")]
+ [else "C#"]))
+
+(define typedracket "Typed Racket")
+(define Typedracket "Typed Racket")
+(define CAML "CAML")
+(define CLOS "CLOS")
+(define NIT "NIT")
+(define CPP "C++")
diff --git a/scribblings/bibliography.bib b/scribblings/bibliography.bib
@@ -0,0 +1,714 @@
+
+@article{bobrow_common_1988,
+ title = {Common lisp object system specification},
+ volume = {23},
+ url = {http://dl.acm.org/citation.cfm?id=885632},
+ number = {SI},
+ urldate = {2017-02-02},
+ journal = {ACM Sigplan Notices},
+ author = {Bobrow, Daniel G. and DeMichiel, Linda G. and Gabriel, Richard P. and Keene, Sonya E. and Kiczales, Gregor and Moon, David A.},
+ year = {1988},
+ pages = {1--142}
+}
+
+
+@inproceedings{torlak_growing_rosette_2013,
+ title = {Growing solver-aided languages with {Rosette}},
+ url = {http://dl.acm.org/citation.cfm?id=2509586},
+ urldate = {2017-02-02},
+ booktitle = {Proceedings of the 2013 {ACM} international symposium on {New} ideas, new paradigms, and reflections on programming \& software},
+ publisher = {ACM},
+ author = {Torlak, Emina and Bodik, Rastislav},
+ year = {2013},
+ pages = {135--152},
+}
+
+@inproceedings{flatt_scheme_classes_2006,
+ title = {Scheme with classes, mixins, and traits},
+ url = {http://link.springer.com/chapter/10.1007/11924661_17},
+ urldate = {2017-02-02},
+ booktitle = {Asian {Symposium} on {Programming} {Languages} and {Systems}},
+ publisher = {Springer},
+ author = {Flatt, Matthew and Findler, Robert Bruce and Felleisen, Matthias},
+ year = {2006},
+ pages = {270--289},
+}
+
+@inproceedings{practical_types_for_clojure_2016,
+ title = {Practical optional types for {Clojure}},
+ url = {http://link.springer.com/chapter/10.1007/978-3-662-49498-1_4},
+ urldate = {2017-02-02},
+ booktitle = {European {Symposium} on {Programming} {Languages} and {Systems}},
+ publisher = {Springer},
+ author = {Bonnaire-Sergeant, Ambrose and Davies, Rowan and Tobin-Hochstadt, Sam},
+ year = {2016},
+ pages = {68--94},
+}
+
+@inproceedings{brown_alloy_2009,
+ title = {Alloy: fast generic transformations for {Haskell}},
+ isbn = {978-1-60558-508-6},
+ shorttitle = {Alloy},
+ url = {http://doi.acm.org/10.1145/1596638.1596652},
+ doi = {10.1145/1596638.1596652},
+ urldate = {2017-02-01},
+ booktitle = {Proceedings of the 2nd {ACM} {SIGPLAN} {Symposium} on {Haskell}, {Haskell} 2009, {Edinburgh}, {Scotland}, {UK}, 3 {September} 2009},
+ publisher = {ACM},
+ author = {Brown, Neil C. C. and Sampson, Adam T.},
+ editor = {Weirich, Stephanie},
+ year = {2009},
+ pages = {105--116},
+}
+
+@misc{vollmerm-typed-nanopass-experiments,
+ title = {typed-nanopass-experiments},
+ author = {Vollmer, Michael and Carter, Kyle},
+ url = {https://github.com/vollmerm/typed-nanopass-experiments},
+ urldate = {2017-02-02},
+ publisher = {GitHub},
+}
+
+@misc{leifandersen-typed-nanopass-model,
+ title = {typed-nanopass-model, a Redex model for a typed version of Nanopass},
+ author = {Andersen, Leif},
+ url = {https://github.com/LeifAndersen/typed-nanopass-model},
+ urldate = {2017-02-02},
+ publisher = {GitHub},
+}
+
+@techreport{sampson_generics_2008,
+ title = {Generics in {Small} {Doses}: {Nanopass} {Compilation} with {Haskell}},
+ shorttitle = {Generics in {Small} {Doses}},
+ url = {http://offog.org/publications/fita200811-generics.pdf},
+ urldate = {2017-02-01},
+ institution = {Technical report},
+ author = {Brown, Neil C. C. and Sampson, Adam T.},
+ year = {2008},
+}
+
+@article{ramsey_applicative_2006,
+ series = {Proceedings of the {ACM}-{SIGPLAN} {Workshop} on {ML} ({ML} 2005)},
+ title = {An {Applicative} {Control}-{Flow} {Graph} {Based} on {Huet}'s {Zipper}},
+ volume = {148},
+ issn = {1571-0661},
+ url = {http://www.sciencedirect.com/science/article/pii/S1571066106001289},
+ doi = {10.1016/j.entcs.2005.11.042},
+ number = {2},
+ urldate = {2017-01-31},
+ journal = {Electronic Notes in Theoretical Computer Science},
+ author = {Ramsey, Norman and Dias, João},
+ month = mar,
+ year = {2006},
+ keywords = {applicative data structures, compilers, control-flow graphs, dataflow analysis, optimization},
+ pages = {105--126},
+}
+
+@article{fluet_phantom_types_as_subtyping_2006,
+ title = {Phantom types and subtyping},
+ volume = {16},
+ number = {06},
+ journal = {Journal of Functional Programming},
+ author = {Fluet, Matthew and Pucella, Riccardo},
+ year = {2006},
+ pages = {751--791},
+}
+
+@inproceedings{refinement_types_2014,
+ address = {New York, NY, USA},
+ series = {{PLPV} '14},
+ title = {Refinement {Types} for {Haskell}},
+ isbn = {978-1-4503-2567-7},
+ url = {http://doi.acm.org/10.1145/2541568.2541569},
+ doi = {10.1145/2541568.2541569},
+ urldate = {2017-01-02},
+ booktitle = {Proceedings of the {ACM} {SIGPLAN} 2014 {Workshop} on {Programming} {Languages} {Meets} {Program} {Verification}},
+ publisher = {ACM},
+ author = {Vazou, Niki and Seidel, Eric L. and Jhala, Ranjit and Vytiniotis, Dimitrios and Peyton-Jones, Simon},
+ year = {2014},
+ keywords = {abstract interpretation, dependent types, haskell, liquid types, refinement types, smt, type inference},
+ pages = {27--27},
+}
+
+@inproceedings{tobin-hochstadt_languages_as_libraries_2011,
+ title = {Languages as libraries},
+ volume = {46},
+ url = {http://dl.acm.org/citation.cfm?id=1993514},
+ urldate = {2017-01-31},
+ booktitle = {{ACM} {SIGPLAN} {Notices}},
+ publisher = {ACM},
+ author = {Tobin-Hochstadt, Sam and St-Amour, Vincent and Culpepper, Ryan and Flatt, Matthew and Felleisen, Matthias},
+ year = {2011},
+ pages = {132--141},
+}
+
+@inproceedings{chang2017type-systems-as-macros,
+ title={Type systems as macros},
+ author={Chang, Stephen and Knauth, Alex and Greenman, Ben},
+ booktitle={Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
+ pages={694--705},
+ year={2017},
+ organization={ACM}
+}
+
+% number={10},
+@inproceedings{pluggable-types-andreae2006framework,
+ title={A framework for implementing pluggable type systems},
+ author={Andreae, Chris and Noble, James and Markstrum, Shane and Millstein, Todd},
+ booktitle={ACM SIGPLAN Notices},
+ volume={41},
+ pages={57--74},
+ year={2006},
+ organization={ACM}
+}
+
+@inproceedings{bracha2004pluggable-types,
+ title={{Pluggable Type Systems}},
+ author={Bracha, Gilad},
+ booktitle={OOPSLA workshop on revival of dynamic languages},
+ citeulike-article-id = {516210},
+ volume={4},
+ year={2004},
+ month = oct,
+ day = {25},
+}
+
+@article{tobin-hochstadt_design_2008,
+ title = {The design and implementation of typed scheme},
+ volume = {43},
+ url = {http://dl.acm.org/citation.cfm?id=1328486},
+ number = {1},
+ urldate = {2017-01-31},
+ journal = {ACM SIGPLAN Notices},
+ author = {Tobin-Hochstadt, Sam and Felleisen, Matthias},
+ year = {2008},
+ pages = {395--406},
+}
+
+@inproceedings{types-for-flexible-objects,
+ series = {Lecture {Notes} in {Computer} {Science}},
+ title = {Types for {Flexible} {Objects}},
+ copyright = {©2014 Springer International Publishing Switzerland},
+ isbn = {978-3-319-12735-4 978-3-319-12736-1},
+ url = {http://link.springer.com/chapter/10.1007/978-3-319-12736-1_6},
+ language = {en},
+ urldate = {2017-01-03},
+ booktitle = {Programming {Languages} and {Systems}},
+ publisher = {Springer International Publishing},
+ author = {Palmer, Zachary and Menon, Pottayil Harisanker and Rozenshteyn, Alexander and Smith, Scott},
+ editor = {Garrigue, Jacques},
+ month = nov,
+ year = {2014},
+ note = {DOI: 10.1007/978-3-319-12736-1\_6},
+ keywords = {Logics and Meanings of Programs, Mathematical Logic and Formal Languages, Programming Languages, Compilers, Interpreters, Software Engineering},
+ pages = {99--119},
+}
+
+@article{flatt2016binding,
+ title={Binding as sets of scopes},
+ author={Flatt, Matthew},
+ journal={ACM SIGPLAN Notices},
+ volume={51},
+ number={1},
+ pages={705--717},
+ year={2016},
+ publisher={ACM}
+}
+
+@article{flatt2012macros,
+ title={Macros that work together},
+ author={Flatt, Matthew and Culpepper, Ryan and Darais, David and Findler, Robert Bruce},
+ journal={Journal of Functional Programming},
+ volume={22},
+ number={02},
+ pages={181--216},
+ year={2012},
+ publisher={Cambridge Univ Press}
+}
+
+
+@inproceedings{nilsson1993lazy,
+ title={Lazy algorithmic debugging: Ideas for practical implementation},
+ author={Nilsson, Henrik and Fritzson, Peter},
+ booktitle={International Workshop on Automated and Algorithmic Debugging},
+ pages={117--134},
+ year={1993},
+ organization={Springer}
+}
+
+@article{wadler1998functional,
+ title={Functional Programming},
+ author={Wadler, Philip},
+ journal={SIGPLAN Notices},
+ volume={33},
+ number={8},
+ pages={23--27},
+ year={1998}
+}
+
+@article{morris1982real,
+ title={Real programming in functional languages},
+ author={Morris, James H},
+ journal={Functional Programming and Its Applications: An Advanced Course},
+ pages={129--176},
+ year={1982},
+ publisher={CUP Archive}
+}
+
+@inproceedings{adams2008efficient,
+ title={Efficient nondestructive equality checking for trees and graphs},
+ author={Adams, Michael D and Dybvig, R Kent},
+ booktitle={ACM Sigplan Notices},
+ volume={43},
+ number={9},
+ pages={179--188},
+ year={2008},
+ organization={ACM}
+}
+
+@article{cardelli1985understanding,
+ title={On understanding types, data abstraction, and polymorphism},
+ author={Cardelli, Luca and Wegner, Peter},
+ journal={ACM Computing Surveys (CSUR)},
+ volume={17},
+ number={4},
+ pages={471--523},
+ year={1985},
+ publisher={ACM},
+ url={http://lucacardelli.name/papers/onunderstanding.a4.pdf}
+}
+
+@book{minsky2013real,
+ title={Real World OCaml: functional programming for the masses},
+ author={Minsky, Yaron and Madhavapeddy, Anil and Hickey, Jason},
+ year={2013},
+ publisher={" O'Reilly Media, Inc."}
+}
+
+
+
+
+
+; From jfla2015--myreferences.bib
+@inproceedings{clement1986simple,
+ title={{A simple applicative language: Mini-ML}},
+ author={Dominique Cl{\'e}ment and Thierry Despeyroux and Gilles Kahn
+ and Jo{\"e}lle Despeyroux},
+ booktitle={Proceedings of the ACM conference on LISP and functional programming},
+ pages={13--27},
+ year=1986,
+ organization={ACM}
+}
+
+@article{erwig2001inductive,
+ title={Inductive graphs and functional graph algorithms},
+ author={Martin Erwig},
+ journal={Journal of Functional Programming},
+ volume=11,
+ number=05,
+ pages={467--492},
+ year=2001,
+ publisher={Cambridge University Press}
+}
+
+@inproceedings{oliveira2012functional,
+ title={Functional programming with structured graphs},
+ author={Bruno C.d.S. Oliveira and William R. Cook},
+ booktitle={ACM SIGPLAN Notices},
+ volume=47,
+ pages={77--88},
+ year=2012,
+ organization={ACM}
+}
+
+
+
+
+% From tapas-sas--bib.bib
+
+@inproceedings{might2006gcfa,
+ author = {Matthew Might and Olin Shivers},
+ title = {Improving {F}low {A}nalyses via {$\Gamma$CFA}: {A}bstract {G}arbage {C}ollection and {C}ounting},
+ booktitle = {Proceedings of the 11th {ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming ({ICFP} 2006)},
+ address = {Portland, Oregon},
+ month = {September},
+ year = {2006}
+}
+
+@InProceedings{might2010mcfa,
+ author = {Matthew Might and Yannis Smaragdakis and David Van Horn},
+ title = {Resolving and exploiting the k-CFA paradox: Illuminating functional vs. object-oriented program analysis.},
+ booktitle = {Proceedings of the 31st {C}onference on {P}rogramming {L}anguage {D}esign and {I}mplementation ({PLDI} 2006)},
+ year = {2010},
+ pages = {305--315},
+ address = {Toronto, Canada},
+ month = {June}
+}
+
+@PhdThesis{shivers91a,
+ Author = {Shivers, Olin Grigsby},
+ Title = {Control-Flow Analysis of Higher-Order Languages or Taming Lambda},
+ School = {Carnige-Mellon Univeristy},
+ Month = {May},
+ Year = {1991}
+}
+
+
+
+
+
+
+
+
+
+
+
+
+@techreport{ducournau-meta-model, TITLE = {{Modules and Class Refinement: A Meta-modeling Approach to Object-Oriented Programming}}, AUTHOR = {Ducournau, Roland and Morandat, Flor{\'e}al and Privat, Jean}, URL = {http://hal-lirmm.ccsd.cnrs.fr/lirmm-00180214}, NUMBER = {RR 07021}, PAGES = 66, YEAR = 2007, MONTH = Aug, KEYWORDS = {Object-oriented programming ; Design tools and techniques-modules and interfaces ; Software Architectures-information hiding ; Reusable Software-reusable models ; reusable libraries ; C++ ; Java ; Eiffel ; Smalltalk ; Clos ; Prm ; Language constructs and features- classes and objects ; inheritance ; modules and packages aspects ; classes ; crosscutting concerns ; expression problem ; hierarchies ; import ; linearization ; meta-modeling ; mixins ; modules ; multiple inheritance ; overloading ; redefinition ; refinement ; static typing}, PDF = {http://hal-lirmm.ccsd.cnrs.fr/lirmm-00180214/file/RD-FM-JP-TOPLAS-07-v09.pdf}, HAL_ID = {lirmm-00180214}, HAL_VERSION = {v1}, institution = {LIRMM}} % ducournau:lirmm-00180214
+
+@inproceedings{floreal-oopsla-btd-tables, author = {Ducournau, Roland and Morandat, Flor{\'e}al and Privat, Jean}, title = {Empirical Assessment of Object-oriented Implementations with Multiple Inheritance and Static Typing}, booktitle = {Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications}, series = {OOPSLA '09}, year = {2009}, isbn = {978-1-60558-766-0}, location = {Orlando, Florida, USA}, pages = {41--60}, numpages = {20}, url = {http://doi.acm.org/10.1145/1640089.1640093}, doi = {10.1145/1640089.1640093}, acmid = {1640093}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {binary tree dispatch, closed-world assumption, coloring, downcast, dynamic loading, interfaces, late binding, method tables, multiple inheritance, multiple subtyping, open-world assumption, perfect hashing, single inheritance, subtype test, type analysis, virtual function table}} % Ducournau:2009:EAO:1640089.1640093,
+
+@inproceedings{coloring89, author = {Dixon, R. and McKee, T. and Vaughan, M. and Schweizer, P.}, title = {A Fast Method Dispatcher for Compiled Languages with Multiple Inheritance}, booktitle = {Conference Proceedings on Object-oriented Programming Systems, Languages and Applications}, series = {OOPSLA '89}, year = {1989}, isbn = {0-89791-333-7}, location = {New Orleans, Louisiana, USA}, pages = {211--214}, numpages = {4}, url = {http://doi.acm.org/10.1145/74877.74900}, doi = {10.1145/74877.74900}, acmid = {74900}, publisher = {ACM}, address = {New York, NY, USA}} % Dixon:1989:FMD:74877.74900,
+
+@article{ducournau-coloring11, TITLE = {{Coloring, a Versatile Technique for Implementing Object-Oriented Languages}}, AUTHOR = {Ducournau, Roland}, URL = {http://hal-lirmm.ccsd.cnrs.fr/lirmm-00596802}, JOURNAL = {{Software: Practice and Experience}}, PUBLISHER = {{Wiley}}, VOLUME = {41}, NUMBER = {6}, PAGES = {627-659}, YEAR = {2011}, HAL_ID = {lirmm-00596802}, HAL_VERSION = {v1}} % ducournau:lirmm-00596802,
+
+
+@Comment @article{Parametric-Shape-Analysis-via-3-Valued-Logic, title={Parametric shape analysis via 3-valued logic}, author={Sagiv, Mooly and Reps, Thomas and Wilhelm, Reinhard}, journal={ACM Transactions on Programming Languages and Systems (TOPLAS)}, volume=24, number=3, pages={217--298}, year=2002, publisher={ACM}}
+
+@Comment @book{introduction-to-lattices-and-order, title = {Introduction to lattices and order}, added-at = {2011-12-23T01:05:17.000+0100}, address = {Cambridge}, author = {Davey, Brian A. and Priestley, Hilary A.}, biburl = {http://www.bibsonomy.org/bibtex/2df19796e33c1e2c861b613e3c8a86f58/sdo}, description = {Introduction to Lattices and Order: B. A. Davey, H. A. Priestley: 9780521367660: Englische Bücher}, interhash = {7255554003c02eb6ddf14a6fcb9b9f72}, intrahash = {df19796e33c1e2c861b613e3c8a86f58}, isbn = {0521365848 9780521365840 0521367662 9780521367660}, keywords = {fca introduction lattice order}, publisher = {Cambridge University Press}, refid = {471812885}, timestamp = {2011-12-23T01:05:17.000+0100}, url = {http://www.worldcat.org/search?qt=worldcat_org_all&q=0521367662}, year = 1990}
+
+@inproceedings{chambers1989customization, title={Customization: Optimizing compiler technology for SELF, a dynamically-typed object-oriented programming language}, author={Chambers, Craig and Ungar, David}, booktitle={ACM SIGPLAN Notices}, volume={24}, pages={146--160}, year={1989}, organization={ACM}} % Comment number={7},
+
+% polycopié de Master Informatique
+@article{ducournau-cours-lots,
+ title={Programmation par Objets: les concepts fondamentaux},
+ author={Ducournau, Roland},
+ journal={Universit{\'e} de Montpellier},
+ biblatex___pagetotal={237},
+ year={2014}
+}
+
+@techreport{ecma-cli,
+ author={ECMA},
+ title={{ECMA-335: Common Language Infrastructure (CLI), \nth{6} edition}},
+ _edition={Sixth},
+ institution={ECMA, Geneva (CH)},
+ month= jun,
+ year=2012
+}
+
+@phdthesis{sallenave2012phd,
+ title={Contribution {\`a} l'efficacit{\'e} des programmes orient{\'e}s objet pour processeurs embarqu{\'e}s},
+ author={Sallenave, Olivier},
+ year={2012},
+ school={Montpellier 2}
+}
+
+@misc{enum-balanced-parenthesis-blog,
+ title={Generating strings of balanced parentheses},
+ author={Dominus, Mark Jason},
+ year=2006,
+ month=feb,
+ day=08,
+ url={http://blog.plover.com/CS/parentheses.html},
+ howpublished = {\small\url{http://blog.plover.com/CS/parentheses.html}},
+ note={Accessed: 2016-04-28.\\Archived by
+ WebCite\textsuperscript{\textregistered} at
+ \small\url{http://www.webcitation.org/6h6TmzTIq}}
+}
+
+% Arnold:1980:URG:357084.357091
+@article{uniform-balanched-parenthesis,
+ author = {Arnold, D. B. and Sleep, M. R.},
+ title = {Uniform Random Generation of Balanced Parenthesis Strings},
+ journal = {ACM Trans. Program. Lang. Syst.},
+ issue_date = {Jan. 1980},
+ volume = {2},
+ number = {1},
+ month = jan,
+ year = {1980},
+ issn = {0164-0925},
+ pages = {122--128},
+ numpages = {7},
+ url = {http://doi.acm.org/10.1145/357084.357091},
+ doi = {10.1145/357084.357091},
+ acmid = {357091},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+@book{taocp-4-4-trees,
+ title = {{The Art of Computer Programming, Volume 4, Fascicle 4: Generating All Trees; History of Combinatorial Generation}},
+ author = {Knuth, Donald E.},
+ original-key = citeulike:1272058,
+ citeulike-article-id = {1272058},
+ citeulike-linkout-0 = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20\&path=ASIN/0321335708},
+ citeulike-linkout-1 = {http://www.amazon.de/exec/obidos/redirect?tag=citeulike01-21\&path=ASIN/0321335708},
+ citeulike-linkout-2 = {http://www.amazon.fr/exec/obidos/redirect?tag=citeulike06-21\&path=ASIN/0321335708},
+ citeulike-linkout-3 = {http://www.amazon.jp/exec/obidos/ASIN/0321335708},
+ citeulike-linkout-4 = {http://www.amazon.co.uk/exec/obidos/ASIN/0321335708/citeulike00-21},
+ citeulike-linkout-5 = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20\&path=ASIN/0321335708},
+ citeulike-linkout-6 = {http://www.worldcat.org/isbn/0321335708},
+ citeulike-linkout-7 = {http://books.google.com/books?vid=ISBN0321335708},
+ citeulike-linkout-8 = {http://www.amazon.com/gp/search?keywords=0321335708\&index=books\&linkCode=qs},
+ citeulike-linkout-9 = {http://www.librarything.com/isbn/0321335708},
+ day = {16},
+ edition = {1},
+ howpublished = {Paperback},
+ isbn = {0321335708},
+ keywords = {combinatorics, computerscience, ownit},
+ month = feb,
+ posted-at = {2007-05-02 15:28:20},
+ priority = {2},
+ publisher = {Addison-Wesley Professional},
+ series = {The Art of Computer Programming},
+ _url = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20\&path=ASIN/0321335708},
+ year = {2006}
+}
+
+@misc{dotnet-native-video,
+ title={Inside {.NET} Native},
+ author={Torre, Charles and Ramaswamy, Mani and Farkas, Shawn},
+ year=2014,
+ month=Apr,
+ day=02,
+ howpublished={\\\small\url{https://channel9.msdn.com/Shows/Going+Deep/Inside-NET-Native}},
+ note={\\Video. Accessed: 2016-04-28.}
+}
+
+% TODO: not 100% read yet
+@misc{msdn-dotnet-native-compilation,
+ key={MSDN dn807190},
+ year=2014,
+ title={{.NET} Native and Compilation},
+ howpublished={\\{\small\url{https://msdn.microsoft.com/en-us/library/dn807190(v=vs.110).aspx}}},
+ note={\\Accessed: 2016-04-28.\\Archived by
+ WebCite\textsuperscript{\textregistered} at
+ \small\url{http://www.webcitation.org/6h6wHyHX8}},
+}
+
+% TODO: not 100% read yet
+@misc{msdn-dotnet-native-main,
+ key={MSDN dn584397},
+ year=2014,
+ title={Compiling Apps with {.NET} Native},
+ howpublished={\\{\small\url{https://msdn.microsoft.com/en-us/library/dn584397(v=vs.110).aspx}}},
+ note={\\Accessed: 2016-04-28.\\Archived by
+ WebCite\textsuperscript{\textregistered} at
+ \small\url{http://www.webcitation.org/6h6wUwxCB}},
+}
+
+@misc{mono-cecil-website,
+ title={Mono.Cecil documentation},
+ author={Köplinger, Alexander and Evain, Jean-Baptiste and others},
+ howpublished={\\\small\url{http://www.mono-project.com/docs/tools+libraries/libraries/Mono.Cecil}},
+ year=2014,
+ month=Jun,
+ day=05,
+}
+
+@misc{mono-cecil-source,
+ title={Mono.Cecil library},
+ author={Evain, Jean-Baptiste and others},
+ howpublished={\\\small\url{https://github.com/jbevain/cecil}},
+ year=2008,
+ month=Oct,
+ day=06,
+}
+
+@misc{mono-website,
+ title={Mono project webpage},
+ author={{Mono Project}},
+ howpublished={\\\small\url{http://www.mono-project.com/}},
+ note={\\Accessed: 2016-04-28.\\Archived by
+ WebCite\textsuperscript{\textregistered} at
+ \small\url{http://www.webcitation.org/6h720IReK}},
+ year=2004,
+ month=Jun,
+ day=30,
+}
+
+@misc{mono-source,
+ title={Mono project GIT repository},
+ author={de Icaza, Miguel and others},
+ howpublished={\\\small\url{https://github.com/mono/mono}},
+ year=2004,
+ month=Jun,
+ day=30,
+}
+
+@inproceedings{nanopass-2013,
+ title = {A nanopass framework for commercial compiler development},
+ volume = {48},
+ booktitle = {{ACM} {SIGPLAN} {Notices}},
+ publisher = {ACM},
+ author = {Keep, Andrew W and Dybvig, R Kent},
+ year = {2013},
+ pages = {343--350}
+}
+
+@inproceedings{nanopass-2004,
+ title = {A nanopass infrastructure for compiler education},
+ volume = {39},
+ booktitle = {{ACM} {SIGPLAN} {Notices}},
+ publisher = {ACM},
+ author = {Sarkar, Dipanwita and Waddell, Oscar and Dybvig, R Kent},
+ year = {2004},
+ pages = {201--212}
+}
+
+% Roslyn CTP red-green trees:
+@misc{overbey2013immutable,
+ title={{Immutable Source-Mapped Abstract Syntax Tree: A Design
+ Pattern for Refactoring Engine APIs}},
+ author={Jeffrey Overbey},
+ year=2013,
+ publisher={Hillside}
+}
+
+@article{huet1997zipper,
+ title={{The Zipper}},
+ author={G{\'e}rard Huet},
+ journal={Journal of Functional Programming},
+ volume=7,
+ number=5,
+ pages={549--554},
+ year=1997,
+ publisher={Cambridge University Press}
+}
+
+% chlipala_parametric_2008
+@book{phoas,
+ title = {Parametric {Higher}-{Order} {Abstract} {Syntax} for {Mechanized} {Semantics}},
+ author = {Chlipala, Adam},
+ year = {2008},
+}
+
+@ARTICLE{Knuth84literateprogramming,
+ author = {Donald E. Knuth},
+ title = {Literate programming},
+ journal = {THE COMPUTER JOURNAL},
+ year = {1984},
+ volume = {27},
+ pages = {97--111}
+}
+
+@inproceedings{tip_scalable_2000,
+ title = {Scalable propagation-based call graph construction algorithms},
+ booktitle = {In {Conference} on {Object}-{Oriented} {Programming} {Systems}, {Languages}, and {Applications}},
+ author = {Tip, Frank},
+ year = {2000},
+ pages = {281--293},
+}
+
+
+@article{probst_demand-driven_2002,
+ title = {A demand-driven solver for constraint-based control flow analysis},
+ author = {Probst, Christian W.},
+ year = {2002},
+}
+
+@article{grove_framework_2001,
+ title = {A {Framework} for {Call} {Graph} {Construction} {Algorithms}},
+ volume = {23},
+ issn = {0164-0925},
+ url = {http://doi.acm.org/10.1145/506315.506316},
+ doi = {10.1145/506315.506316},
+ number = {6},
+ urldate = {2016-05-31},
+ journal = {ACM Trans. Program. Lang. Syst.},
+ author = {Grove, David and Chambers, Craig},
+ month = nov,
+ year = {2001},
+ keywords = {Call graph construction, control flow analysis, interprocedural analysis},
+ pages = {685--746},
+}
+
+@phdthesis{tobin-hochstadt_typed_2010,
+ title = {Typed scheme: {From} scripts to programs},
+ shorttitle = {Typed scheme},
+ author = {Tobin-Hochstadt, Sam},
+ year = {2010},
+}
+
+
+@inproceedings{bacon_fast_1996,
+ address = {New York, NY, USA},
+ series = {{OOPSLA} '96},
+ title = {Fast {Static} {Analysis} of {C}++ {Virtual} {Function} {Calls}},
+ isbn = {978-0-89791-788-9},
+ url = {http://doi.acm.org/10.1145/236337.236371},
+ doi = {10.1145/236337.236371},
+ urldate = {2016-05-31},
+ booktitle = {Proceedings of the 11th {ACM} {SIGPLAN} {Conference} on {Object}-oriented {Programming}, {Systems}, {Languages}, and {Applications}},
+ publisher = {ACM},
+ author = {Bacon, David F. and Sweeney, Peter F.},
+ year = {1996},
+ pages = {324--341},
+}
+
+@techreport{bacon_rapid_1996,
+ title = {Rapid {Type} {Analysis} for {C}++},
+ number = {pending},
+ institution = {IBM Thomas J. Watson Reseach Center},
+ author = {{Bacon, David F.} and {Wegman, M.} and {Zadeck, K.}},
+ year = {1996},
+ keywords = {c, optimization},
+}
+
+
+@article{gentzen_untersuchungen_1935_1,
+ title = {Untersuchungen über das logische {Schließen}. {I}},
+ volume = {39},
+ issn = {0025-5874, 1432-1823},
+ url = {http://link.springer.com.gate6.inist.fr/article/10.1007/BF01201353},
+ doi = {10.1007/BF01201353},
+ language = {de},
+ number = {1},
+ urldate = {2016-05-31},
+ journal = {Mathematische Zeitschrift},
+ author = {Gentzen, Gerhard},
+ month = dec,
+ year = {1935},
+ keywords = {Mathematics, general},
+ pages = {176--210},
+}
+
+@article{gentzen_untersuchungen_1935_2,
+ title = {Untersuchungen über das logische {Schließen}. {II}},
+ volume = {39},
+ issn = {0025-5874, 1432-1823},
+ url = {http://link.springer.com.gate6.inist.fr/article/10.1007/BF01201363},
+ doi = {10.1007/BF01201363},
+ language = {de},
+ number = {1},
+ urldate = {2016-05-31},
+ journal = {Mathematische Zeitschrift},
+ author = {Gentzen, Gerhard},
+ month = dec,
+ year = {1935},
+ keywords = {Mathematics, general},
+ pages = {405--431},
+}
+
+@techreport{flatt_plt_1997,
+ title = {{PLT} {MzScheme}: language manual},
+ institution = {Citeseer},
+ author = {Flatt, Matthew and {others}},
+ year = {1997},
+}
+
+@article{reactive_survey_2013,
+ title = {A {Survey} on {Reactive} {Programming}},
+ volume = {45},
+ issn = {0360-0300},
+ url = {http://doi.acm.org/10.1145/2501654.2501666},
+ doi = {10.1145/2501654.2501666},
+ number = {4},
+ urldate = {2016-06-01},
+ journal = {ACM Comput. Surv.},
+ author = {Bainomugisha, Engineer and Carreton, Andoni Lombide and Cutsem, Tom van and Mostinckx, Stijn and Meuter, Wolfgang de},
+ month = aug,
+ year = {2013},
+ keywords = {dataflow programming, event-driven applications, functional reactive programming, interactive applications, Reactive programming, reactive systems},
+ pages = {52:1--52:34},
+}
+\ No newline at end of file
diff --git a/scribblings/state-of-the-art.scrbl b/scribblings/state-of-the-art.scrbl
@@ -0,0 +1,405 @@
+#lang scribble/manual
+
+@require["util.rkt"]
+@(use-mathjax)
+
+@title[#:style (with-html5 manual-doc-style)]{State of the art}
+
+@asection{
+ @atitle{Extending the type system via macros (type-expander)}
+
+ Our work explores one interesting use of macros: their use to extend a
+ programming language's type system.
+
+ Chang, Knauth and Greenman@~cite{chang2017type-systems-as-macros} took
+ the decision to depart from Typed Racket, and implemented a new approach,
+ which allows type systems to be implemented as macros. Typing information
+ about identifiers is threaded across the program at compile-time, and macros
+ can decide whether a term is well-typed or not.
+
+ Another related project is Cur@note{@url{https://github.com/wilbowma/cur}}, a
+ dependent type system implemented using Racket macros.
+
+ Bracha suggests that pluggable type systems should be
+ used@~cite{bracha2004pluggable-types}. Such a system, JavaCOP is presented by
+ Andreae, Noble, Markstrum and
+ Shane@~cite{pluggable-types-andreae2006framework} as a tool which ``enforces
+ user-defined typing constraints written in a declarative and expressive rule
+ language''.
+
+ In contrast, Typed Racket@~cite{tobin-hochstadt_design_2008} was
+ implemented using macros on top of ``untyped'' Racket, but was not
+ designed as an extensible system: new rules in the type system must be
+ added to the core implementation, a system which is complex to approach.
+
+ Following work by Asumu
+ Takikawa@note{@url{https://github.com/racket/racket/pull/604}}, we
+ extended Typed Racket with support for macros in the type declarations and
+ annotations. We call this sort of macro ``type expanders'', following the
+ commonly-used naming convention (e.g. ``match expanders'' are macros which
+ operate within patterns in pattern-matching forms). These type expanders
+ allow users to easily extend the type system with new kinds of types, as
+ long as these can be translated back to the types offered natively by
+ Typed Racket.
+
+ While the Type Systems as Macros by Chang, Knauth and
+ Greenman@~cite{chang2017type-systems-as-macros} allows greater flexibility
+ by not relying on a fixed set of core types, it also places on the
+ programmer the burden of ensuring that the type checking macros are
+ sound. In contrast, our type expanders rely on Typed Racket's type
+ checker, which will still catch type errors in the fully-expanded
+ types. In other words, writing type expanders is safe, because they do not
+ require any specific trust, and translate down to plain Typed Racket
+ types, where any type error would be caught at that level.
+
+ An interesting aspect of our work is that the support for type expanders
+ was implemented without any change to the core of Typed Racket. Instead,
+ the support for type expanders itself is available as a library, which
+ overrides special forms like @tt{define}, @tt{lambda} or
+ @tt{cast}, enhancing them by pre-processing type expanders, and
+ translating back to the ``official'' forms from Typed Racket. It is worth
+ noting that Typed Racket itself is implemented in a similar way: special
+ forms like @tt{define} and @tt{lambda} support plain type
+ annotations, and translate back to the ``official'' forms from so-called
+ ``untyped'' Racket. In both cases, this approach goes with the Racket
+ spirit of implementing languages as
+ libraries@~cite{tobin-hochstadt_languages_as_libraries_2011}}
+
+ @asection{
+ @atitle{Algebraic datatypes for compilers (phc-adt)}
+ The @tt{phc-adt} library implements algebraic datatypes (variants and
+ structures) which are adapted to compiler-writing.
+
+ There is an existing ``simple'' datatype library for Typed/Racket (source
+ code available at @url{https://github.com/pnwamk/datatype}). It differs
+ from our library on several points:
+ @itemlist[
+ @item{``datatype'' uses nominal typing, while we use structural typing
+ (i.e. two identical type declarations in distinct modules yield the same
+ type in our case). This avoids the need to centralize the type
+ definition of ASTs.}
+ @item{``datatype'' uses closed variants, where a constructor can only
+ belong to one variant. We simply define variants as a union of
+ constructors, where a constructor can belong to several variants. This
+ allows later passes in the compiler to add or remove cases of variants,
+ without the need to duplicate all the constructors under slightly
+ different names.}
+ @item{``datatype'' does not support row polymorphism, or similarly the
+ update and extension of its product types with values for existing and
+ new fields, regardless of optional fields. We implement the
+ latter.@htodo{ Probably the former too.}}]
+
+ @asection{
+ @atitle{The case for bounded row polymorphism}
+ @todo{Explain the ``expression problem''.}
+
+ We strive to implement compilers using many passes. A pass should be
+ able to accept a real-world AST, and produce accordingly a real-world
+ transformed AST as its output. It should also be possible to use
+ lightweight ``mock'' ASTs, containing only the values relevant to the
+ passes under test (possibly only the pass being called, or multiple
+ passes tested from end to end). The pass should then return a
+ corresponding simplified output AST, omitting the fields which are
+ irrelevant to this pass (and were not part of the input). Since the
+ results of the pass on a real input and on a test input are equivalent
+ modulo the irrelevant fields, this allows testing the pass in isolation
+ with simple data, without having to fill in each irrelevant field with
+ @tt{null} (and hope that they are indeed irrelevant, without a
+ comforting guarantee that this is the case), as is commonly done when
+ creating ``mocks'' to test object-oriented programs.
+
+ This can be identified as a problem similar to the ``expression
+ problem''. In our context, we do not strive to build a compiler which
+ can be extended in an ``open world'', by adding new node types to the
+ AST, or new operations handling these nodes. Rather, the desired outcome
+ is to allow passes to support multiple known subsets of the same AST
+ type, from the start.
+
+ We succinctly list below some of the different sorts of polymorphism,
+ and argue that row polymorphism is well-suited for our purpose. More
+ specifically, bounded row polymorphism gives the flexibility needed when
+ defining passes which keep some fields intact (without reading their
+ value), but the boundedness ensures that changes in the input type of a
+ pass do not go unnoticed, so that the pass can be amended to handle the
+ new information, or its type can be updated to ignore this new
+ information.
+
+ @subsubsub*section{Subtyping, polymorphism and alternatives}
+ @|~|@(linebreak)
+ @~cite{ducournau-cours-lots}. @htodo{The course includes a couple of
+ other kinds of polymorphism and subtyping (or makes finer distinctions
+ than in the list below). Refine and augment the list below using
+ Roland's classification.} @htodo{Probably also cite:}
+ @~cite{cardelli1985understanding} @htodo{(apparently does not cover
+ ``Higher-Kinded Polymorphism'', ``Structural Polymorphism'' and ``Row
+ Polymorphism'')}
+ @itemlist[
+ @item{Subtyping (also called inclusion polymorphism, subtype
+ polymorphism, or nominal subtyping ?): Subclasses and interfaces in
+ @csharp and Java, sub-structs and union types in Typed Racket,
+ polymorphic variants in @CAML @~cite[#:precision @list{chap. 6, sec. Polymorphic Variants}]{minsky2013real}}
+ @; https://realworldocaml.org/v1/en/html/variants.html
+
+ @; See also: use of exceptions as dynamically extensible sum types:
+ @; http://caml-list.inria.narkive.com/VJcoGfvp/dynamically-extensible-sum-types
+ @;
+ @; quote: I need a dynamically extensible sum type. I can think of three approaches:
+ @; quote:
+ @; quote: (1) Use polymorphic variants: `Foo of a * b, `Bar of c * d * e, etc
+ @; quote:
+ @; quote: (2) Use exceptions: exception Foo of a * b, exception Bar of c * d * e, etc
+ @; quote:
+ @; quote: (3) Use thunks: (fun () -> foo a b), (fun () -> bar c d e), etc
+ @; quote:
+ @; quote: Using exceptions seems somewhat sneaky to me. Does it have any advantages over
+ @; quote: polymorphic variants? The polymorphic variants seem like they might be better
+ @; quote: since you could actually limit the domain of certain functions... thus, one
+ @; quote: part of your program could be constrained to a subrange of the sum type, while
+ @; quote: other parts could be opened up fully.
+ @; quote:
+ @; quote: Until now I have been using the thunking approach in an event-based
+ @; quote: architecture (each event on the queue is a unit->unit thunk). This seems to
+ @; quote: work pretty well. But now I'm thinking that the other approaches would allow
+ @; quote: arbitrary filters to be applied to events; i.e., the thunk approach imposes a
+ @; quote: "read once" discipline on elements of the sum type, and in some applications
+ @; quote: you might want "read multiple".
+ @; quote:
+ @; quote: I'm not asking the question solely in terms of event-based architectures,
+ @; quote: though, and I'm interested in others experience with the different approaches
+ @; quote: to dynamically extensible sum types, and what led you to choose one approach
+ @; quote: over the others. Thanks!
+ @item{Multiple inheritance. @NIT, @CLOS, @CPP, @csharp interfaces, Java
+ interfaces. As an extension in ``untyped'' Racket with Alexis King's
+ safe multimethods@note{@url{https://lexi-lambda.github.io/blog/2016/02/18/simple-safe-multimethods-in-racket/}}.
+
+ This in principle could help in our case: AST nodes would have
+ @tt{.withField(value)} methods returning a copy of the node with
+ the field's value updated, or a node of a different type with that
+ new field, if it is not present in the initial node type. This would
+ however require the declaration of many such methods in advance, so
+ that they can be used when needed (or with a recording mechanism
+ like the one we use, so that between compilations the methods called
+ are remembered and generated on the fly by a macro). Furthermore,
+ @typedracket lacks support for multiple inheritance on structs. It
+ supports multiple inheritance for classes @todo{?}, but classes
+ currently lack the ability to declare immutable fields, which in
+ turn causes problems with occurrence typing (see the note in the
+ ``row polymorphism'' point below).}
+ @item{Parametric polymorphism: Generics in @csharp and Java,
+ polymorphic types in @CAML and @typedracket}
+ @item{F-bounded polymorphism: Java, @csharp, @CPP, Eiffel. Possible
+ to mimic to some extent in @typedracket with (unbounded) parametric
+ polymorphism and intersection types.
+ @todo{Discuss how it would work/not work in our case.}}
+ @item{Operator overloading (also called overloading polymorphism?) and
+ multiple dispatch:
+ @itemlist[
+ @item{Operator overloading in @csharp}
+ @item{Nothing in Java aside from the built-in cases for arithmetic and string concatenation, but those are not extensible}
+ @item{@CPP}
+ @item{typeclasses in Haskell? @todo{I'm not proficient enough in Haskell to
+ be sure or give a detailed description, I have to ask around to double-check.}}
+ @item{LISP (CLOS): has multiple dispatch}
+ @item{nothing built-in in @|typedracket|.}
+ @item{@|CAML|?}]}
+ @item{Coercion polymorphism (automatic casts to a given type). This
+ includes Scala's implicits, @csharp implicit coercion operators
+ (user-extensible, but at most one coercion operator is applied
+ automatically, so if there is a coercion operator @${A → B},
+ and a coercion operator @${B → C}, it is still impossible to
+ supply an @${A} where a @${C} is expected without manually coercing the
+ value), and @CPP's implicit conversions, where single-argument
+ constructors are treated as implicit conversion operators, unless
+ annotated with the @tt{explicit} keyword. Similarly to @csharp,
+ @CPP allows only one implicit conversion, not two or more in a chain.
+
+ Struct type properties in untyped Racket can somewhat be used to that
+ effect, although they are closer to Java's interfaces than to coercion
+ polymorphism. Struct type properties are unsound in @typedracket and are
+ not represented within the type system, so their use is subject to caution
+ anyway.}
+ @item{Coercion (downcasts). Present in most typed languages. This
+ would not help in our case, as the different AST types are
+ incomparable (especially since @typedracket lacks multiple inheritance)}
+
+
+ @item{Higher-kinded polymorphism: Type which is parameterized by a
+ @${\mathit{Type} → \mathit{Type}} function. Scala, Haskell. Maybe
+ @|CAML|?
+
+ The type expander library which we developed for @typedracket
+ supports @${Λ}, used to describe anonymous type-level
+ macros. They enable some limited form of
+ @${\mathit{Type} → \mathit{Type}} functions, but are
+ actually applied at macro-expansion time, before typechecking is
+ performed, which diminishes their use in some cases. For example,
+ they cannot cooperate with type inference. Also, any recursive use
+ of type-level macros must terminate, unless the type ``function''
+ manually falls back to using @${\mathit{Rec}} to create a regular
+ recursive type. This means that a declaration like
+ @${F(X) := X × F(F(X))} is not possible using anonymous type-level
+ macros only.
+ @; See https://en.wikipedia.org/wiki/Recursive_data_type#Isorecursive_types
+ @; Is this a matter of isorecursive vs equirecursive ?
+
+ As an example of this use of the type expander library, our
+ cycle-handling code uses internally a ``type traversal'' macro. In
+ the type of a node, it performs a substitution on some subparts of
+ the type. It is more or less a limited form of application of a
+ whole family of type functions @${aᵢ → bᵢ}, which have the same inputs
+ @${aᵢ …}, part of the initial type, but different outputs @${bᵢ …} which
+ are substituted in place of the @${aᵢ …} in the resulting type. The
+ ``type traversal'' macro expands the initial type into a standard
+ polymorphic type, which accepts the desired outputs @${bᵢ …} as type
+ arguments.}
+ @item{Lenses. Can be in a way compared to explicit coercions, where
+ the coercion is reversible and the accessible parts can be altered.}
+ @item{Structural polymorphism (also sometimes called static duck-typing): Scala,
+ TypeScript. It is also possible in @typedracket, using the algebraic
+ datatypes library which we implemented. Possible to mimic in Java
+ and @csharp with interfaces ``selecting'' the desired fields, but
+ the interface has to be explicitly implemented by the class (i.e. at
+ the definition site, not at the use-site).
+
+ Palmer et al. present TinyBang@~cite{types-for-flexible-objects}, a
+ typed language in which flexible manipulation of objects is possible,
+ including adding and removing fields, as well as changing the type of
+ a field. They implement in this way a sound, decidable form of static
+ duck typing, with functional updates which can add new fields and
+ replace the value of existing fields. Their approach is based on two
+ main aspects:
+ @itemlist[
+ @item{@emph{Type-indexed records supporting asymmetric concatenation}:
+ by concatenating two records @${r₁ \& r₂}, a new record is obtained
+ containing all the fields from @${r₁} (associated to their value in
+ @${r₁}), as well as the fields from @${r₂} which do not appear in @${r₁}
+ (associated to their value in @${r₂}). Primitive types are eliminated
+ by allowing the use of type names as keys in the records: integers
+ then become simply records with a @${int} key, for example.}
+ @item{@emph{Dependently-typed first-class cases}: pattern-matching
+ functions are expressed as
+ @${pattern \mathbin{\texttt{->}} expression}, and can be concatenated
+ with the @${\&} operator, to obtain functions matching against
+ different cases, possibly with a different result type for each
+ case. The leftmost cases can shadow existing cases (i.e. the case
+ which is used is the leftmost case for which the pattern matches
+ successfully).}]
+
+ TinyBang uses an approach which is very different from the one we
+ followed in our Algebraic Data Types library, but contains the
+ adequate primitives to build algebraic data types which would
+ fulfill our requirements (aside from the ability to bound the set of
+ extra ``row'' fields). We note that our flexible structs, which are
+ used within the body of node-to-node functions in passes, do support
+ an extension operation, which is similar to TinyBang's @${\&}, with
+ the left-hand side containing a constant and fixed set of
+ fields.@htodo{we probably can have / will have the ability to merge
+ non-constant left-hand side values too.}}
+ @item{Row polymorphism: Apparently, quoting a post on
+ Quora@note{@hyperlink["https://www.quora.com/Object-Oriented-Programming-What-is-a-concise-definition-of-polymorphism"]{https://www.quora.com/Object-Oriented-Programming-What-is-a-concise-definition@|?-|-of-polymorphism}\label{quora-url-footnote}}:
+ @aquote{
+ Mostly only concatenative and functional languages (like Elm and PureScript) support this.
+ }
+
+ Classes in @typedracket can have a row type argument (but classes in
+ @typedracket cannot have immutable fields (yet), and therefore
+ occurrence typing does not work on class fields. Occurrence typing
+ is an important idiom in @typedracket, used to achieve safe but
+ concise pattern-matching, which is a feature frequently used when
+ writing compilers).
+
+ Our Algebraic Data Types library implements a bounded form of row
+ polymorphism, and a separate implementation (used within the
+ body of node-to-node functions in passes) allows unbounded row
+ polymorphism.}
+ @item{@todo{Virtual types}}
+ @item{So-called ``untyped'' or ``uni-typed'' languages: naturally
+ support most of the above, but without static checks.
+
+ @htodo{
+ @; phc/reading/CITE/Object-Oriented Programming_ What is a concise definition of polymorphism_ - Quora.html
+ @; TODO: fix the footnote here!
+ See also post on Quora@superscript{\ref{quora-url-footnote}},
+ which links to @~cite{cardelli1985understanding}, and to a blog post by Sam
+ Tobin-Hochstadt@note{@url|{https://medium.com/@samth/on-typed-untyped-and-uni-typed-languages-8a3b4bedf68c}|}
+ The blog post by Sam Tobin-Hochstadt explains how @typedracket tries to
+ explore and understand how programmers think about programs written in
+ so-called ``untyped'' languages (namely that the programmers still
+ conceptually understand the arguments, variables etc as having a type (or a
+ union of several types)). @todo{Try to find a better citation for that.}}
+
+ Operator overloading can be present in ``untyped'' languages, but is
+ really an incarnation of single or multiple dispatch, based on the
+ run-time, dynamic type (as there is no static type based on which the
+ operation could be chosen). However it is not possible in ``untyped''
+ languages and languages compiled with type erasure to dispatch on
+ ``types'' with a non-empty intersection: it is impossible to
+ distinguish the values, and they are not annotated statically with a
+ type.
+
+ As mentioned above, @typedracket does not have operator overloading,
+ and since the inferred types cannot be accessed reflectively at
+ compile-time, it is not really possible to construct it as a
+ compile-time feature via macros. @typedracket also uses type erasure,
+ so the same limitation as for untyped languages applies when
+ implementing some form of single or multiple dispatch at run-time ---
+ namely the intersection of the types must be empty. @todo{Here,
+ mention (and explain in more detail later) our compile-time
+ ``empty-intersection check'' feature (does not work with polymorphic
+ variables).}}]
+
+ @todo{Overview of the existing ``solutions'' to the expression problems, make
+ a summary table of their tradeoffs (verbosity, weaknesses, strengths).}
+
+ @todo{Compare the various sorts of subtyping and polymorphism in that light
+ (possibly in the same table), even those which do not directly pose as a
+ solution to the expression problem.}
+
+
+ ``Nominal types'': our tagged structures and node types are not nominal types.
+
+ The ``trivial'' Racket library tracks static information about the types in
+ simple cases. The ``turnstile'' Racket language @todo{is a follow-up} work,
+ and allows to define new typed Racket languages. It tracks the types of
+ values, as they are assigned to variables or passed as arguments to functions
+ or macros. These libraries could be used to implement operator overloads which
+ are based on the static type of the arguments. It could also be used to
+ implement unbounded row polymorphism in a way that does not cause a
+ combinatorial explosion of the size of the expanded code.@todo{Have a look at
+ the implementation of row polymorphism in @typedracket classes, cite their
+ work if there is something already published about it.}
+
+ From the literate program (tagged-structure-low-level):
+
+ @quotation{
+ Row polymorphism, also known as "static duck typing" is a type system
+ feature which allows a single type variable to be used as a place
+ holder for several omitted fields, along with their types. The
+ @tt{phc-adt} library supports a limited form of row polymorphism:
+ for most operations, a set of tuples of omitted field names must be
+ specified, thereby indicating a bound on the row type variable.
+
+ This is both a limitation of our implementation (to reduce the
+ combinatorial explosion of possible input and output types), as well as a
+ desirable feature. Indeed, this library is intended to be used to write
+ compilers, and a compiler pass should have precise knowledge of the
+ intermediate representation it manipulates. It is possible that a compiler
+ pass may operate on several similar intermediate representations (for
+ example a full-blown representation for actual compilation and a minimal
+ representation for testing purposes), which makes row polymorphism
+ desirable. It is however risky to allow as an input to a compiler pass any
+ data structure containing at least the minimum set of required fields:
+ changes in the intermediate representation may add new fields which should,
+ semantically, be handled by the compiler pass. A catch-all row type variable
+ would simply ignore the extra fields, without raising an error. Thanks to
+ the bound which specifies the possible tuples of omitted field names,
+ changes to the the input type will raise a type error, bringing the
+ programmer's attention to the issue. If the new type is legit, and does not
+ warrant a modification of the pass, the fix is easy to implement: simply
+ adding a new tuple of possibly omitted fields to the bound (or replacing an
+ existing tuple) will allow the pass to work with the new type. If, on the
+ other hand, the pass needs to be modified, the type system will have
+ successfully caught a potential issue.
+ }
+ }
+ }@;{Algrbraic datatypes for compilers (phc-adt)}
diff --git a/scribblings/thesis.scrbl b/scribblings/thesis.scrbl
@@ -0,0 +1,11 @@
+#lang scribble/manual @;or classicthesis
+@require[@for-label[typed/racket/base]
+ "util.rkt"]
+@(use-mathjax)
+
+@title[#:style (with-html5 manual-doc-style)]{Thesis}
+@author[@author+email["Georges Dupéron" "georges.duperon@gmail.com"]]
+
+@include-section{state-of-the-art.scrbl}
+
+@(generate-bibliography-section)
+\ No newline at end of file
diff --git a/scribblings/util.rkt b/scribblings/util.rkt
@@ -0,0 +1,102 @@
+#lang racket
+
+(provide (rename-out [my-title title])
+ asection
+ atitle
+ aquote
+ quotation
+ htodo
+ todo
+ (rename-out [~cite* ~cite])
+ citet
+ generate-bibliography-section
+ (rename-out [note* note])
+ define-footnote ;; TODO: does not use the (superscript …)
+ (all-from-out "abbreviations.rkt")
+ (all-from-out scribble-math))
+
+(require racket/stxparam
+ racket/splicing
+ scribble/base
+ scribble/core
+ scriblib/bibtex
+ scriblib/footnote
+ scriblib/render-cond
+ racket/runtime-path
+ scribble-enhanced/math
+ scribble-math
+ "abbreviations.rkt")
+
+(use-mathjax)
+
+;; TODO: merge the handling of unicode chars into scribble-math.
+(define m setup-math)
+(define my-title
+ ;; TODO: use this for the other wrapped procs in this file
+ (make-keyword-procedure
+ (λ (kws kw-args . rest)
+ (list m
+ (keyword-apply title kws kw-args rest)))))
+
+(define counter 0)
+(define (counter!)
+ (set! counter (add1 counter))
+ counter)
+
+(define (note* . content)
+ (cond-element
+ [html (let ([c (number->string (counter!))])
+ (list (superscript c)
+ (apply note
+ (list (superscript c) ~ content))))]
+ [latex (apply note content)]
+ [else (apply note content)]))
+
+(define-runtime-path bib-path "bibliography.bib")
+(define-bibtex-cite bib-path
+ ~cite
+ citet
+ generate-bibliography-section)
+
+(define-syntax-parameter asection-current-level 0)
+(define-syntax-rule (asection . body)
+ (splicing-syntax-parameterize ([asection-current-level
+ (add1 (syntax-parameter-value
+ #'asection-current-level))])
+ . body))
+
+(define-syntax (atitle stx)
+ (syntax-case stx ()
+ [(_ . args)
+ (case (syntax-parameter-value #'asection-current-level)
+ [(0) #'(my-title . args)]
+ [(1) #'(section . args)]
+ [(2) #'(subsection . args)]
+ [(3) #'(subsubsection . args)]
+ [else
+ ;; TODO: log a warning here maybe?
+ #'(subsubsub*section . args)])]))
+
+;; hidden todo:
+(define (htodo . args) (list))
+
+;; todo:
+(define (coloured-elem colour . content)
+ (elem #:style (style #f (list (color-property colour))) content))
+(define (todo . args)
+ (list (coloured-elem "gray" "[")
+ args
+ (coloured-elem "gray" "]" (superscript "Todo"))))
+
+(define (aquote . content)
+ (nested-flow (style #f '())
+ (list (paragraph (style #f '()) content))))
+
+(define (quotation . content)
+ (nested-flow (style #f '())
+ (list (paragraph (style #f '()) content))))
+
+(define (~cite* #:precision [precision #f] . rest)
+ (if precision
+ (list (apply ~cite rest) ", " precision)
+ (apply ~cite rest)))
+\ No newline at end of file
diff --git a/travis-deploy-key-id_rsa.enc b/travis-deploy-key-id_rsa.enc
Binary files differ.
