From 291bf17c0e9290e9dbe8f47ab8026230bb445e74 Mon Sep 17 00:00:00 2001 From: ben Date: Mon, 14 Mar 2016 05:02:57 -0400 Subject: [PATCH] [icfp] stc checkpoint --- icfp-2016/README.md | 13 +++++ icfp-2016/benchmark/vector-map.rkt | 68 ---------------------- icfp-2016/conclusion.scrbl | 38 +++++++++++-- icfp-2016/experience.scrbl | 4 +- icfp-2016/implementation.scrbl | 4 +- icfp-2016/intro.scrbl | 2 +- icfp-2016/related-work.md | 91 +++++++++++++++++++++++++++++- icfp-2016/usage.scrbl | 1 + 8 files changed, 144 insertions(+), 77 deletions(-) delete mode 100644 icfp-2016/benchmark/vector-map.rkt diff --git a/icfp-2016/README.md b/icfp-2016/README.md index f9d4e8c..e2070ac 100644 --- a/icfp-2016/README.md +++ b/icfp-2016/README.md @@ -104,4 +104,17 @@ generates the type constraint curry : ((A B -> A) -> (A -> B -> A)) ] +--- +Readers with a phd in type theory may think: "these are just wannabe dependent types". +That is correct. +Readers with a phd in macrology may think: "these are just macros". +Also correct. +We think we have found a sweet spot, combining the basic features of macros + to get the basic utility of dependent types. + +Let the programmers judge. + +--- + +also useful for untyped (goes wihtout saying?) diff --git a/icfp-2016/benchmark/vector-map.rkt b/icfp-2016/benchmark/vector-map.rkt deleted file mode 100644 index 2887cf3..0000000 --- a/icfp-2016/benchmark/vector-map.rkt +++ /dev/null @@ -1,68 +0,0 @@ -#lang typed/racket/base -(require - trivial/vector - trivial/math - racket/vector - plot/typed/no-gui - math/statistics) - -(define NUM-TRIALS 8) - -(define-vector: v1 (make-vector (expt: 10 1))) -(define-vector: v2 (make-vector (expt: 10 2))) -(define-vector: v3 (make-vector (expt: 10 3))) -(define-vector: v4 (make-vector (expt: 10 4))) -(define-vector: v5 (make-vector (expt: 10 5))) -(define-vector: v6 (make-vector (expt: 10 6))) -(define-vector: v7 (make-vector (expt: 10 7))) -;(define-vector: v8 (make-vector (expt: 10 8))) -;(define-vector: v9 (make-vector (expt: 10 9))) - -(define-syntax-rule (tt e) - (let ([proc (lambda () e)]) - (mean (for/list : (Listof Integer) - ([i (in-range NUM-TRIALS)]) - (let-values (((res cpu real gc) (time-apply proc '()))) - cpu))))) - -(define before* - (list - (tt (vector-map (lambda (x) x) v1)) - (tt (vector-map (lambda (x) x) v2)) - (tt (vector-map (lambda (x) x) v3)) - (tt (vector-map (lambda (x) x) v4)) - (tt (vector-map (lambda (x) x) v5)) - (tt (vector-map (lambda (x) x) v6)) - (tt (vector-map (lambda (x) x) v7)) - #;(tt (vector-map (lambda (x) x) v8)) - #;(tt (vector-map (lambda (x) x) v9)))) - -(define after* - (list - (tt (vector-map: (lambda (x) x) v1)) - (tt (vector-map: (lambda (x) x) v2)) - (tt (vector-map: (lambda (x) x) v3)) - (tt (vector-map: (lambda (x) x) v4)) - (tt (vector-map: (lambda (x) x) v5)) - (tt (vector-map: (lambda (x) x) v6)) - (tt (vector-map: (lambda (x) x) v7)) - #;(tt (vector-map: (lambda (x) x) v8)) - #;(tt (vector-map: (lambda (x) x) v9)))) - -;; TODO plot-pict -(plot-file - (list - (lines (for/list : (Listof (List Integer Real)) - ([i (in-naturals 1)] - [t (in-list before*)]) - (list i t)) - #:color 1 - #:label "before") - (lines (for/list : (Listof (List Integer Real)) - ([i (in-naturals 1)] - [t (in-list after*)]) - (list i t)) - #:color 2 - #:label "after")) - "map-microbench.png" - 'png) diff --git a/icfp-2016/conclusion.scrbl b/icfp-2016/conclusion.scrbl index afb2491..3579b1d 100644 --- a/icfp-2016/conclusion.scrbl +++ b/icfp-2016/conclusion.scrbl @@ -1,4 +1,5 @@ #lang scribble/sigplan +@require["common.rkt"] @title[#:tag "sec:conclusion"]{Closing the Books} @@ -8,6 +9,7 @@ This pearl described an approach to using a macro system to enhance Whereas types support reasoning independent of data representations, we hope to have shown that reflecting a little value information into the compile-time environment can pay off for common programming tasks. +@; Moreover, can do without programmer annotations Indeed, a tempting subtitle for this pearl would be @emph{compile-time constant propagation}, because that is precisely what we do. @@ -18,12 +20,38 @@ A key thesis behind this work is that the analysis can be implemented in a variety of languages using their existing type and syntax extension systems. Indeed: -@parag{Typed Clojure} has +@parag{Typed Clojure} has a flexible macro system derived from Common Lisp. +Built-in functions @tt{macroexpand} and @tt{with-meta} correspond to Racket's + @racket[local-expand] and @racket[syntax-property]; with help from a library + implementing identifier macros,@note{@url["https://github.com/clojure/tools.macro"]} + we were able to implement a basic prototype in untyped Clojure. + +@todo{does TC have macros? can I use macros from untyped code if I type them?} + + +@parag{Haskell} Template Haskell + + +@parag{OCaml} ppx + + +@parag{Rust} has a stable, pattern-based macro system which unfortunately + seems too weak to reimplement our analysis. +As of Rust 1.7,@note{@url["https://doc.rust-lang.org/reference.html"]} + the basic macros can only specify input/output pairs. +There is no way to do complex branching within a condition, + such as throwing an exception if a format string is given too many arguments. +Just parsing the format string would be challenging. + +However Rust also has an interface for writing arbitrarily powerful compiler + plugins. +It would be interesting to reproduce our results as a plugin. + + +@parag{Scala} users have a few macro systems to choose from. +@; We investigated Scala Macros and TODO. +@; https://doc.rust-lang.org/book/compiler-plugins.html -@parag{Haskell} -@parag{OCaml} -@parag{Rust} -@parag{Scala} With out last words, we look to the future. Although we gave criteria for correct predicates and translations diff --git a/icfp-2016/experience.scrbl b/icfp-2016/experience.scrbl index a96fbe1..658540d 100644 --- a/icfp-2016/experience.scrbl +++ b/icfp-2016/experience.scrbl @@ -1,10 +1,12 @@ #lang scribble/sigplan +@require["common.rkt"] @title[#:tag "sec:experience"]{Experience} - @; compile times, running times, binary size @; LOC reduction, bugs caught +Coarse measure of usefulness, applied to xxx lines of code. + We used the library to simplify @todo{lines} of database code and @todo{lines} of vector code. Performance of the vector code improved by @todo{xxx}, a nice bonus. diff --git a/icfp-2016/implementation.scrbl b/icfp-2016/implementation.scrbl index 522cf89..9596b76 100644 --- a/icfp-2016/implementation.scrbl +++ b/icfp-2016/implementation.scrbl @@ -496,12 +496,14 @@ Code used to generate a syntax-parse pattern may be run at phase level 2, and Phases are explicitly separated. By design, it is difficult to share state between two phases. Also by design, it is very easy to import bindings from any module at a specific - phase + phase. The upshot of this is that one can write and test ordinary, phase-0 Racket code but then use it at a higher phase level. @; + non-meta programming @; + not getting stuck in ascending ladder @; + modular development +@; + don't need to worry about Singletons Haskell duplication +@; There is no need to duplicate code for use at different phases. @subsection{Lexical Scope, Source Locations} diff --git a/icfp-2016/intro.scrbl b/icfp-2016/intro.scrbl index d24896f..dafad5f 100644 --- a/icfp-2016/intro.scrbl +++ b/icfp-2016/intro.scrbl @@ -5,6 +5,7 @@ @; : can you give more example? @; : too generous to other languages -- why didn't you do the entire paper in hs? @; - a note on macro-land? where truthy & boolean monads are king? +@; - also, the untyped style of reasoning, the needing to unfold code @; - transf vs. macro @@ -116,4 +117,3 @@ We also give a modern description of Racket's macro system and handle definition 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/???/???"]. -Suggestions for a new package name are welcome. diff --git a/icfp-2016/related-work.md b/icfp-2016/related-work.md index 5185bc3..6f24804 100644 --- a/icfp-2016/related-work.md +++ b/icfp-2016/related-work.md @@ -3,6 +3,7 @@ related-work All papers in `src/` directory. +Many workarounds = polydots, pi-types, printf-types, ... Herman Meunier, 2004 --- @@ -15,8 +16,39 @@ Herman Meunier, 2004 [Politz, Q-D, Krishnamurthi](http://cs.brown.edu/research/plt/dl/progressive-types/progressive-types.pdf) --- +- turning up the class of type errors +- progressively say what more should go wrong -yolo + +[neelk](/Users/ben/code/racket/my-pkgs/trivial/icfp-2016/src/k-obt-2016.pdf ) +--- +- breakup into more steps +- elaborte from sexp to binding trees #nuprl, then to lambda terms +0 if this niggas just doing stlc that will be very sad + + + +[oleg](http://okmij.org/ftp/Computation/lightweight-dependent-typing.html) +--- +- ADTs can enforce propositions. + If you functor apply to get an abstract set, you have a property about the integers: + \forall n,m . n /= m -> mem? n (singleton m) == False +- singletons are for types with unique inhabitants +- Dont understand hongwei example + - http://okmij.org/ftp/Haskell/eliminating-array-bound-check.lhs + + +[Lightweight Static Capabilites] +[Lightweight Static Resources] + + + +[Singletons] +--- +- Eisenberg, Weirich +- Kicking my ass a little, do printf + nary zip in parentheses; db as main thing +- library does the boilerplate of writing types/functions a second time +- [Hasochism] @@ -28,3 +60,60 @@ yolo Especially Ernst, Dietl and the regular-expression types for Java. Maybe just regexp types but at least that, ya know? + + +QDSL / LINQ +--- + +- http://homepages.inf.ed.ac.uk/slindley/papers/qdsl-draft-february2015.pdf + - host(C) + target(SQL) language (can we apply elsewhere) + - + + +- http://homepages.inf.ed.ac.uk/slindley/papers/practical-theory-of-linq.pdf + - + +- https://homes.cs.washington.edu/~akcheung/papers/cidr13.pdf + - java Hibernate? this paper just compiles java to sql + + +- http://infoscience.epfl.ch/record/180642/files/EPFL_TH5456.pdf + - generate SQL with embedded compiler + - wow, Tiarks thesis is looking very familiar (to me) + +- http://hackage.haskell.org/package/opaleye +- (dead?) https://wiki.haskell.org/MetaHDBC + - https://lindstroem.files.wordpress.com/2008/09/metahdbc.pdf + +;; TODO related work? +;; - OCaml https://github.com/mmottl/postgresql-ocaml/ +;; seems to return strings +;; - Haskell http://book.realworldhaskell.org/read/using-databases.html +;; get 'SqlString', etc + + +[Futamuru](http://blog.sigfpe.com/2009/05/three-projections-of-doctor-futamura.html) +--- + +Partial evaluation +- specialize interpreter for source code; given fixed input, specialize + - can use the specializing machine as a compiler + - (compile programs to machines) +- specialize specializer to interpreter, make compiler for class of interpreters + - (make specific interpreter->compiler machine) +- specliaze specializer to specializer = interpreter->compiler machine + - (make interpreter->compiler machine) + + +@; Tuples in Haskell http://hackage.haskell.org/package/tuple +@; Regexp +@; - ocaml http://caml.inria.fr/pub/docs/manual-ocaml/libref/Str.html +@; - haskell https://hackage.haskell.org/package/regex-compat/docs/Text-Regex.html + + + +SoundX -- cannot reporduce this because + +[anti-TH](http://stackoverflow.com/questions/10857030/whats-so-bad-about-template-haskell) +--- +Not great news for me / metaprogramming diff --git a/icfp-2016/usage.scrbl b/icfp-2016/usage.scrbl index 36acd44..91d8e7d 100644 --- a/icfp-2016/usage.scrbl +++ b/icfp-2016/usage.scrbl @@ -360,6 +360,7 @@ Each operation match the length of its arguments at compile-time and expand @section{Database Queries} @; db @; TODO Ocaml, Haskell story +@; TODO connect to ew-haskell-2012 os-icfp-2008 Racket's @racket[db] library provides a string-based API for executing SQL queries.