[icfp] stc checkpoint

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?)

icfp-2016/benchmark/vector-map.rkt

@@ -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)

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

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.

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}

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.

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

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.