[Ur] Draft of a paper on the Ur/Web optimizer

[mozert1 mozert1]

Some comments mixed with some questions mixed with my own personal notes (◡‿◡✿)

1. *** p3 * " Sets of textual source files. " ______to______
It may be profitable to clarify that ur/web use non-extensible LR
bottom-up parsing by mlyacc. And there is no extensible parsing
although ur/web is marketed as some DSL.

For Gross: how difficult would it be to do extensible parsing for fun
? can coq parsing parses be ocaml-extracted and used here :D By the
way, in the parsing parses paper sec 7.3 p10, why change the
definition of the minimal parse tree instead of restricting the
definition of the productions so to exclude productions with cycles;
... even harper sml book chooses to restrict the definition of regular
expression instead of to change the implementation/trace/tree to make
the bug go away. By the way harper sml book p228 sec 27.2 contains
errors/notclear in the transformation to "regular expression in
standard form".

More serious question: can the inria dedukti modulo grammar be encoded
profitably using ur ?  and also can the dedukti runtime which is
programmed in ocaml be also programmed in ur (.. dedukti makes uses of
mutual recursive datatypes which ur lacks .. and also doesnt ur put
some restrictions on too-much first-class functions somewhere down the
compilation phases ?)

2. *** p3 * " type-level finite maps (having kinds like {κ}, for
finite maps from names to types of kind κ, inspired by row types
[28]), " _____to_____ maybe for the lazy people, explain more how ur
[5] differs from "row types [28]", and MORE IMPORTANTLY HOW DID THE
CREATOR OF UR KNEW IN ADVANCE that hes flavor of contructor-level
computation (and not .. any other flavor-or-full dependent types)
would suffice to encode some XML and the very complex SQL (in sec 3.3
monoize phase, something is said about reynolds parametricity but more
comment is lacked)

3. *** p4 * " Core also supports mutually recursive definitions of
algebraic datatypes,  ______to______ really? mutually recursive
datatypes ? CLARIFICATION pls.. does ur/web source code somehow
support multually recursive datatypes? .. speciallly when this comment
comes before saying that "Not shown in the figure, but included in the
implementation, are poly-morphic variants" which really are'nt used
much anywhere other than in basis.urs ...  by the way, the mlyacc
parser has problems with the quotes ['] and wont accept this [
datatype dt' ty = DtNil' | DtCons' of ty * dt' ty ]

4. *** p10 sec 4 * " It does not seem that any of the publicly
deployed appli-cations are pushing the limits of Ur/Web server
performance yet, " _____to______  maybe add also some comment for the
productivity or programming point of view in contrast to server
performance point of view:  the only thing programmingly difficult in
ur/web is to achieve full genericity with SQL as shown in the UPO
library. As long as the user is programming one fixed particular
application for hes particular database table schemas then everything
is easy, but as soon as full genericity is wished things get
ridiculuous as shown in the UPO library and only the ur creator would
bother with such fancy stuff.

5. *** p11 sec 4.2 * " The application-specific code amounts to about
600 lines of Ur/Web, relying on a library we are developing for custom
event-organizer applications. "  ______to______ comment: surprisingly
although upo includes many very generic sql ui functionaity, there is
one thing missing from upo: how do you edit list of list generically ?
in other words some table with some columm of sql_injectable type
[serialized (list t)]  or some table with some column which is
referenced by foreign key (from same table) (parent/childs rows) ? For
the serialized alternative, is some new [Widget.t (serialized (list
t)) listbox] class witness in /upo/widget.ur possible and enough ?

6. *** p11 sec 4.2 * .. maybe comment somewhere that doing   wc -l *
c/* elisp/* coq/*    in /urweb/src/ gives 100000 lines total and how
many years did it take?

7. *** p11 sec 4.2 * .. Comment: may be some few words on the topic of
the other non-performance particularities of ur/web: auditability of
the source code and database policy (.. Capsules, Caja ..) . Question:
for some "freelance developer" how does hemself in practice sells
auditability of the source code that hemself write for the
customer/bigcorp ?  The ur/web ref manual lacks details on
auditability and database policy but this is where ur/web can
distinguish itself from php n00bs who can't be shared secrecy by
bigcorps   ( ͡ಠ ͜ʖ ͡ಠ)

8. *** RE: the chat.ur example in the popl paper or in the demo: there
is still something which feels wrong with the given code, no matter
how the reactive javascript implementation detects the changes to the
data [source]s or incrementally/optimally recompute/update the [dyn]
elements .. ok here is one proposed middle solution, which simply fix
the formating, instead of :

fun append t text =
s <− source Nil;
oldTail <− get t.Tail;
set oldTail (Cons (text, s));
set t.Tail s;

log <− get t.Head;
case log of
Nil => set t.Head (Cons (text, s))
| _ => return ()


pretty print:
fun append t text =
s <− source Nil;

oldTail <− get t.Tail;
set oldTail (Cons (text, s));

log <− get t.Head;
case log of
Nil => set t.Head (Cons (text, s))
| _ => return ()

set t.Tail s;

or pretty print:
fun append t text =
s <− source Nil;

oldTail <− get t.Tail;
set oldTail (Cons (text, s));

set t.Tail s;

log <− get t.Head;
case log of
Nil => set t.Head (Cons (text, s))
| _ => return ()

9. MISC:
*** p1 * " supporting objects with arbitrary lifetimes, accessed via
pointers or references that may be aliased. " ______to______ accessed
via pointers or names that may be aliased.

*** p12 * " [5] A. Chlipala. Ur: Statically-typed metaprogramming with
type-level record computation. " ______to______ Ur: the programming
for static computation of constructor-level (type-level) records

*** p3 * " MLton partially evaluates programs to remove uses of
abstraction and modularity mech-anisms like parametric polymorphism or
functors, in the sense of ML module systems " ______to______
parametric polymorphism or functors ("parametric scoped contexts" ...
parametric signatures)

*** p3 * " Core. Here we remove the module system from the language,
so " _______to_______ maybe propose some alt name as MonoScope instead
of Core ...

========================

10. MISC ERRATA FOR THE URWEB REF MAN 20150520
*** sec 7 p30 * fold.  r :: {K} → folder r → tf r   ____to____ r :::
{K} → folder r → tf r

*** sec 8 p31 * redirect doesnt interup as transaction unit, only
redirect as transaction page

*** sec 8.3 p32 * [file] datatype implementation not perfect
/tmp/fileoWA5ki/webapp.c: In function ‘uw_handle’:
/tmp/fileoWA5ki/webapp.c:654:7: error: implicit declaration of
function ‘uw_Basis_unurlifyFile’
[-Werror=implicit-function-declaration]
       uw_Basis_file uwr_File = uw_Basis_unurlifyFile(ctx, &request);
       ^
/tmp/fileoWA5ki/webapp.c:654:7: error: invalid initializer
/tmp/fileoWA5ki/webapp.c:654:7: error: (near initialization for ‘arg0’)
cc1: all warnings being treated as errors

*** sec 9.1.2 p48 * T ::= x
x AS X
x AS {c}
{{e}} AS t   ____to______ {{e}} AS X ___and___ what use for antiquoted
table expressions anyway?

*** sec 8.4.3 p41 * " The parsing extension for UPDATE will elaborate
all table-free field references to use table variable T. "
_____to_____ constant table name T

*** sec 8.4.2 p37 * " The other aggregate functions are placed into a
general type family, using constructor classes to restrict usage to
properly typed arguments. "  _____to_____  The other aggregate
functions are classified into a general type family, using constructor
classes to restrict usage to proper type arguments.

*** sec 8.4.2 p38 * val sql subquery : tables ::: {{Type}} → agg :::
{{Type}} → exps ::: {Type} → nm ::: Name → t ::: Type → nt ::: Type
→ nullify t nt → sql query tables agg [nm = t] →  ______to______ sql
query tables agg [] [nm = t]

*** p48 * F ::= T | {{e}} | F J JOIN F ON E
| F CROSS JOIN F
| (Q) AS t | ({{e}}) AS t ______to_____   in practice ({{e}}) AS t is
not recognized by parser, and what does it mean anyway?

*** p48 * T ::= x
x AS X
x AS {c}
{{e}} AS t _____________to _________ {{e}} AS X   (equivalently AS f ,
but t is not ok for AS)

*** p48 * F ::= T | {{e}} | F J JOIN F ON E
| F CROSS JOIN F
| (Q) AS t _________to__________  (Q) AS X | (Q) AS {c}  (equivalently
AS f , but t is not ok for AS), also clarify that Q only return
expression columns, no table columns

*** s5.6 p21 * pattern: combines checking with multiclassification by
equivalent types ___to___ contrast with expression

*** s4.2 p14  s5.6 p21 * {(x = p, ) ∗ } rigid record pattern
{(x = p, ) + , . . .} flexible record pattern _____to_____ change x to
X everywhere including in section pattern typing, because constant
constructor - field name is lacked

*** sec5.7 p22 * in declaration typing, [open M] or [open constraint
M] it is not at all clear what [O(M,s)] does to constraint signature
items.. guessing that it is comparable to making one theorem into some
axiom, so to speed up constraint inference ?
Also the two [structure X : S = M] declarations bindings, it is not
clear how they are exclusive ?
Also the [constraint c1 ~ c2] declaration "binding", maybe clarify
that it is some check not some binding ?
Also clarify how to view [c1 ~ c2] as some dependent kind which
depends on constructors, and the resulting special lambda fn-forall
abstraction-quantification syntax?