[Ur] No-code use cases?

[Adam Chlipala]

Folks, I apologize for being behind responding to Ur/Web GitHub issues 
and so forth, but I've been distracted trying to kick off an 
Ur/Web-based startup company.  I figured that, nonetheless, I'd try my 
luck here and see if anyone has any advice for us finding early 
customers or in a few other dimensions.


I imagine, for this audience, I don't have to work too hard to make the 
case that Ur/Web raises the abstraction level of web-app programming 
significantly.  As I developed UPO  and 
applied it for a few medium-sized apps, I realized that the abstraction 
level had gotten high enough that we should even be able to build a GUI 
that lets laypeople design their own apps without thinking like 
programmers.  So we built that platform, called Nectry.  The way I'm 
thinking of it now is that it should be the perfect way to help 
non-developer, business-oriented folks within companies take advantage 
of all the local services, from standard ones like Salesforce to the 
company's custom REST APIs. Building blocks for all that can be 
provisioned, such that types etc. guarantee that apps others build with 
them are secure.  The game is really helping nonprogrammers build full 
web apps with dependently typed combinator libraries!


I would much appreciate hearing from members of the Ur/Web community 
about any of the following aspects of our quest:


 * Do you know anyone who might appreciate being an early adopter of
   tooling to harness the business know-how of nonprogrammers safely in
   do-it-yourself web-app development?
 * Would you or someone you know potentially be interested in getting
   involved with our effort?  We're open to remote work, though we
   can't pay anyone yet.  The most pressing roles would be in
   engineering, applying expertise in advanced functional programming
   and compilers; or a business-y role driving discovery of early
   customers and fine-tuning of our model for who we should be
   marketing to and how.
 * Do you know any investors who might resonate with the technology and
   consider seed funding for an early-stage venture just signing its
   first paying customers now?

Thank you in advance for any leads!

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] build errors in travis

[Adam Chlipala]

Good catch!  Now I'm curious why the CI system didn't tip me off about 
this problem earlier, but it should be fixed now.


On 3/30/21 3:03 AM, Fabrice Leal wrote:
Decided to check again on urweb, and noticed the build error mark on 
the readme; after some light investigation it seems the error comes 
from building the demo application, which has a bunch of


allow url #*

is this new syntax or obsolete syntax? :)


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur/Web first impressions

[Adam Chlipala]

On 3/18/21 2:20 PM, Joachim Breitner wrote:

Obviously, I need to connect the above function to a source/signal with
the game state. I found that this works, although I wonder if this is
an idiomatic way to do so:

   
   
 }/>

  The idiomatic way would be to use the features of the FFI for adding
change listeners on signals.  You may have been thrown off by the
fact that the library you took as inspiration does no such thing!
You'll find JavaScript function "listen" documented briefly on page
59 of the currently posted reference manual.

Yes, I remembered that mention, but given that both the source and the
code I want to invoke upon changes already lives in “Ur world” it felt
wrong to reach for the FFI. And it was expressible with just non-FFI-
features, as shown above… I guess either way is just a way to deal with
the fact that I am doing something uncommon (running possibly effectful
code upon changes to the signal).
I should have been more specific in my suggestion.  Instead of exposing 
a mutable datatype of canvases, I would prefer a pure datatype of 
functional drawing descriptions.  Then you can give your canvas a type 
like `signal picture_description -> xbody`.  I don't see a place where 
we'd want an operation to listen for changes to trigger mutation.

However, I also think of the type `source xbody` as a bad code
smell.  It is usually better to put your fundamental data model in
sources and then derive HTML from them using  tags.

That’s what I ended up doing in the end, and it’s probably cleaner.
(Although a part of me, when it sees a data type T that is only
deconstructed by a single function T -> A, wonders why not create
values of type A directly. At least in a pure language.)
The payoff from introducing an explicit data model is that you might 
find later that parts of the data you used previously should also 
influence other parts of the page, and you don't need to go back and 
change anything else -- you avoid "callback hell" of finding all the 
places a source was changed and adding new logic to modify some other 
part of the page.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur/Web first impressions

[Adam Chlipala]

Thanks for all the thoughts on the language!  My responses:

On 3/17/21 6:36 PM, Joachim Breitner wrote:

I got “Some constructor unification variables are undetermined in
declaration” for unification variables in unused code (e.g. when I
stopped using some temporary recursive helper function). Made me wonder
if undetermined variables could be maybe be allowed in unused code, so
that I don’t have to comment out that code?
Maybe, but that's not as simple of an idea as it would be in classic 
Hindley-Milner type inference.  The reason is that, in general, not all 
values of remaining unification variables are legal.  There are other 
lingering constraints, including disjointness of rows, so it really 
would involve adding a somewhat-interesting solver.

In terms of developer usability, I was kinda expecting a “urweb watch”
mode that, upon changes to the sources, recompiles, restarts the
server, and maybe reloads the client. But not a big deal, I am just
spoiled.
I sometimes use my own simple external scripting to that end (watching 
the file system for changes), for interactive demos. However, for better 
or worse, large projects will take long enough to compile that I would 
think an unpleasant user experience could follow from automatic 
recompilation.

On the server side, the old app didn’t need any persistent state (it
only associated state with open connections), but in Ur/Web I had to
use the database to communicate between the open connections.
Yeah, it makes sense that that use case would require a bit of 
arbitrary-feeling setup, to use the SQL database for cross-HTTP-request 
state.  It's not at all the kind of scenario I had in mind in designing 
the language.  However, it would be easy enough to wrap all use of SQL 
in a functor exporting a pretty natural interface.

The “serialized” type
constructor was a bit odd; I wonder why can’t I just use the type
directly and instead have to serialize/deserialize, but I kinda see the
point.
I'm trying to remember why I introduced that type family years ago! Part 
of it is that I wanted to use type classes to control which types are 
allowed in SQL code values, so that functors may declare their 
expectations appropriately.  Serialization fails at compile time when 
used on inappropriate types, and that failure logic uses arbitrary 
compiler code, not a nice set of type-class instances.  So it can be 
seen as kind of a trick to get arbitrary type-level approval code into a 
type-class instance.

Ur/Web doesn’t support canvas drawing out of the box, but I found
https://github.com/fabriceleal/urweb-canvas/. Using a library like that
was simple enough. Unfortunately, it didn’t cover the full Canvas API
yet, and it seemed that adding the missing functions would require more
boiler plate than I wanted to write right now.


I can see how that makes sense for a quick pilot to evaluate the 
language, though I expect it's pretty cost-effective to extend that 
library with general Canvas features, for any kind of production app 
(and then everyone else gets to benefit from the improvements!).


In my experience, wrapping JavaScript libraries isn't a significant 
effort bottleneck for real projects, but you've raised a number of good 
ideas for improving the FFI experience, which I would at least be glad 
to see come in as pull requests, after some discussion on this mailing list.



But maybe the need to import JS libraries is just rare enough.
Speaking only for myself, there have been precious few JavaScript 
libraries that I've ever wanted to connect to from Ur/Web.  I think the 
tally stands at about five since 2006.  I find that most libraries used 
in web programming are making up for design mistakes in other libraries, 
Ponzi-scheme style.

Obviously, I need to connect the above function to a source/signal with
the game state. I found that this works, although I wonder if this is
an idiomatic way to do so:

   
   
 }/>
The idiomatic way would be to use the features of the FFI for adding 
change listeners on signals.  You may have been thrown off by the fact 
that the library you took as inspiration does no such thing! You'll find 
JavaScript function "listen" documented briefly on page 59 of the 
currently posted reference manual.

I found it odd that I cannot have mutually recursive values of type
transaction (which is a function of sorts), and have to add unit
arguments. Probably a ML programmer finds that restriction natural,
with my Haskell background it was odd.
Right: Ur/Web has eager evaluation, so it is not coherent to allow 
recursive definition of just anything!  And it's an interesting question 
how such a language can allow introduction of new classes of recursive 
things in libraries, rather than as built-in language features.  Nothing 
about transactions is built into the Ur/Web core language.

Similarly, at one point I tried to use `s : source xbody <- source …`
for the main views (because why introduce a data type 

Re: [Ur] Better date & time support in Ur/Web + PostgreSQL

[Adam Chlipala]

Thanks for sharing the description of your new functionality, at my 
request in a GitHub issue ! 
It looks like there are no related strong opinions lurking on this 
mailing list.


I would definitely be up to seeing appropriate types built into the 
standard library (and compiler). Are there natural implementations for 
the other major open-source SQL engines, not just Postgres?


On 8/16/20 9:56 AM, Simon Van Casteren wrote:


I've been building www.classy.school  for 
some time with Ur/Web now. It's an application for music schools and a 
lot of it revolves around schedules: Who has lessons at what time, 
which teacher, which room, etc etc.


In Ur/Web's "standard library" there are 2 types to represent dates / 
times:


  * Basis.time (Corresponds to unix epoch milliseconds IIRC). Contains
both date and time
  * Datetime.t (Corresponds to a C struct IIRC). A bit more structure
than Basis.time

I don't work with these two types at all. I defined two other types:

  * calendardate. This is actually a type synonym for Basis.time, but
only because it makes it possible to serialize this to sql values.
All operations on this type only change the date part, so year -
month - day. It contains no timezone info.
  * clocktime: { Hour: int, Minute: int}. (I don't need seconds, but
it wouldn't hurt to add it as well). I have to serialize /
deserialize this whenever it goes into the DB, very annoying.

I've found this to be a much easier representation to work with for my 
domain. Example: When you enroll with a teacher for some private 
lessons, you often do it for x (eg: 10) lessons on a certain weekday 
on a certain time. This time I have in my datamodel as a clocktime. 
The actual "timestamps" of every lesson are seperate. Another benefit: 
Comparing calendardates is much easier than comparing Basis.time / 
Datetime.t.


Anyway, I've been thinking for some time to propose to upstream all of 
this / some of this into the standard library, if there is any 
interest for it. With that I'd also serialize them into the correct 
PostgreSQL types (calendardate -> date, clocktime -> time without 
timezone). Afterwards, I want to look into adding support for some SQL 
operators on these, especially adding a clocktime to a date (which 
then becomes a PostgreSQL timestamp without timezone, not sure yet how 
to model this in the type system). Being able to do this in SQL would 
be huge for my application.


So long story short, I'd mainly like to know if adding this stuff to 
the standard library would be welcomed. If not, I'll keep all this in 
my personal repo and put the SQL stuff in my urweb fork, but I thought 
I'd ask :).


Simon



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Change grammar to swap precedence of "&&" and "||"?

[Adam Chlipala]

OK, it is now changed!

On 5/15/20 2:47 PM, Adam Chlipala wrote:


Way back when, in Ur/Web's grammar, I apparently gave these two 
quintessential Boolean operators different relative precedences, 
compared to other widely used languages, as has been pointed out 
<https://github.com/urweb/urweb/issues/202>. Would anyone object to 
swapping them?  It's entirely possible that there has not yet been 
written an Ur/Web program that would parse differently depending on 
this choice, but it seems worth checking for strong opinions.  A week 
from posting this message, I'll consider it safe to take the proposed 
action, if no one has complained.




___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Change grammar to swap precedence of "&&" and "||"?

[Adam Chlipala]

Way back when, in Ur/Web's grammar, I apparently gave these two 
quintessential Boolean operators different relative precedences, 
compared to other widely used languages, as has been pointed out 
. Would anyone object to 
swapping them?  It's entirely possible that there has not yet been 
written an Ur/Web program that would parse differently depending on this 
choice, but it seems worth checking for strong opinions.  A week from 
posting this message, I'll consider it safe to take the proposed action, 
if no one has complained.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Blogpost

[Adam Chlipala]

Thanks so much for sharing this link, which I've added to the Ur web site.

One bit of Ur/Web style advice: I recommend List.app over List.mapM for 
cases where you just want to perform a side effect on each list element, 
rather than constructing a new list.  That change in your examples would 
make them a bit shorter and epsilon more time-and-memory-efficient.


You also have an example of queryL1 followed by List.mapM.  I would just 
use queryI1 there.


On 4/27/20 2:28 AM, Simon Van Casteren wrote:

Hi everybody,

In case anyone is interested, I wrote a blog post some time ago about 
my experiences with Ur/Web.


http://frigoeu.github.io/urweb1.html

Simon


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Any interest in bringing up a platform for virtual conferences?

[Adam Chlipala]

On 3/30/20 2:23 AM, Urs Wegmann wrote:

I tried to install the demo and failed so far. Is there any advice on how to 
install libraries? Do I need to build them first or can I just download and 
copy to a certain directory?


I was inspired to add build instructions including all unusual 
dependencies, /and///I've moved the repo to the urweb organization, so 
see info here:


    https://github.com/urweb/upo

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Any interest in bringing up a platform for virtual conferences?

[Adam Chlipala]

I'm glad to see the interest from Daniel and Simon!  Here's my latest 
demo application 
<https://github.com/achlipala/upo/blob/master/examples/onlineconf.ur>, 
which also uses the Ur/Web World library 
<https://github.com/urweb/world> for Google and Zoom integration, plus 
the Mail library <https://github.com/urweb/email>.  On the near-term 
to-do list is also showing off some Slack integration.


I'm curious if anyone else can figure out how to build and run that 
demo. >:)


I encourage folks who like the general idea to give it a try and then 
contact me privately about how it goes.


On 3/21/20 3:29 AM, Daniel Tornabene wrote:
I'm interested.  I haven't used Urweb but I love standard ML, so my 
contributions would be perhaps less immediate as others more familiar 
with the codebase


On Fri, Mar 20, 2020 at 5:47 PM Adam Chlipala <mailto:ad...@csail.mit.edu>> wrote:


Some of you may remember the Ur/Web People Organizer (UPO) library
<http://upo.csail.mit.edu/> that I've mentioned a few times.  It's
an Ur/Web component library for rapid creation of applications to
organize people -- a pretty broad remit. It uses a lot of
metaprogramming to write your application for you based on your
database schema.

Suddenly an important variant of coordinating people is running a
virtual event.  For instance, many planned conferences have moved
to online substitutes, on short notice.  Events often have subtle
differences from each other while sharing many logistical elements.

I wonder what interest there is out there in developing enough new
UPO components to support virtual events.  For instance, I think
it needs good ways to interact with video-conferencing software to
livestream talks with Q, and to make the recorded videos
available easily afterward in perpetuity, integrated within sites
that take advantage of rich, per-event data schemas.

Would anyone like to join me in trying to plan out the required
functionality and divvy up the coding work?

Full disclosure: I'm still developing a startup-company concept
that could take advantage of that support.  The company is about,
basically, a very simplified IDE for snapping UPO components
together, so that people without programming experience can do
it.  My idea is that the underlying, programmer-focused library
remains open forever, though.

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Any interest in bringing up a platform for virtual conferences?

[Adam Chlipala]

Some of you may remember the Ur/Web People Organizer (UPO) library 
 that I've mentioned a few times.  It's an 
Ur/Web component library for rapid creation of applications to organize 
people -- a pretty broad remit.  It uses a lot of metaprogramming to 
write your application for you based on your database schema.


Suddenly an important variant of coordinating people is running a 
virtual event.  For instance, many planned conferences have moved to 
online substitutes, on short notice.  Events often have subtle 
differences from each other while sharing many logistical elements.


I wonder what interest there is out there in developing enough new UPO 
components to support virtual events.  For instance, I think it needs 
good ways to interact with video-conferencing software to livestream 
talks with Q, and to make the recorded videos available easily 
afterward in perpetuity, integrated within sites that take advantage of 
rich, per-event data schemas.


Would anyone like to join me in trying to plan out the required 
functionality and divvy up the coding work?


Full disclosure: I'm still developing a startup-company concept that 
could take advantage of that support.  The company is about, basically, 
a very simplified IDE for snapping UPO components together, so that 
people without programming experience can do it.  My idea is that the 
underlying, programmer-focused library remains open forever, though.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] New release

[Adam Chlipala]

A new release is available at:
  https://github.com/urweb/urweb/releases/tag/20200209

CHANGELOG for this release:

- New invocation mode 'urweb daemon restart'
- Disallow wildcards in signatures
- At compile time, start allowing "#" as a URL
- New option '-u' for generated HTTP servers, to use UNIX sockets
- New HTML tag attribute: 'step' (for )
- New SQL function: 'similar' (via pg_trgm)
- New List function: foldli
- New Json functions: json_record_withOptional, json_time, rfc3339_in, 
rfc3339_out

- New Datetime member: ord_month
- New JavaScript FFI function 'listen'
- Experimental support for the Language Server Protocol (helpful for IDEs)
- Bug fixes and improvements to documentation, error messages, 
performance, and compatibility



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Result monad

[Adam Chlipala]

In this case, I think the straightforward answer is that result is 
clearly not a monad, just on the basis of its kind!  However, for any 
fixed x, fn a => result a x can be a monad.  I suggest reformulating 
your last definition to be polymorphic in that way.  Probably everything 
resolves most nicely if you swap the order of arguments to result.


On 2/6/20 1:34 PM, Urs Wegmann wrote:


I try to create a monad:

datatype result a x =

  Ok of a

| Err of x

fun mreturn [a] [x] (r : a) : result a x = Ok r

fun mbind [a] [b] [x] (r : result a x) (f : a -> result b x) : result 
b x =


  case r of

    Ok r => f r

  | Err x => Err x

val result_monad = mkMonad

  {

    Return = @@mreturn,

    Bind = @@mbind

  }

I think the error message tries to tell me that x is not defined 
enough. Is there a way to fix this? When I remove x from result, it 
compiles.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Planning a new Ur/Web release soon

[Adam Chlipala]

I like the idea of making a final Ur/Web release of 2019.  Please let me 
know this week if there are any lingering issues that have not been 
addressed yet in the main repo  that 
seem straightforward enough to address before a release.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Utility objectifyUr function in JavaScript

[Adam Chlipala]

On 10/28/19 3:35 PM, Mark Clements wrote:

I found that the following function is very useful for converting Ur/Web
data structures within JavaScript. This may be useful to others --
although has it been implemented elsewhere?


Thanks for sharing this code.  It's not obvious to me that this code 
belongs in a general library, since it seems to be based on some 
nontrivial assumptions about which Ur/Web types to handle. For instance, 
I think the code mishandles pairs (records with field names 1 and 2), 
incorrectly identifying them as lists.  It also seems to assume that all 
algebraic datatypes are option-style, which isn't true in general.  For 
instance, a term like A (B (C 7))) will apparently be flatted into 7, 
even if the constructors that were peeled away are conveying important 
information.


If one wants to support the full range of types, then I think it becomes 
clear that the original format is actually a pretty good choice!  At 
least, every one of the features that you flatten away was included 
explicitly to avoid ambiguity.  One possible exception is avoiding 
underscores at the beginnings of some record field names, but in that 
case I was motivated by uniformity (simple map to field names in 
JavaScript just by prepending underscores).


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Default settings using a generic record update

[Adam Chlipala]

On 10/28/19 3:27 PM, Mark Clements wrote:

fun defaultSetting args =
  update {A=1, B=1} args

val _ = defaultSetting {A=2} (* {A=2, B=1} *)
val _ = defaultSetting {B=2} (* {A=1, B=2} *)
The problem is that polymorphism in Ur/Web is always declared 
explicitly, not inferred as OCaml or Haskell.  You must add binders for 
type variables for defaultSettings just as you did for update.  (This 
statement applies to definitions of functions, not uses, so the two 
example calls above should work once you get defaultSettings defined 
properly.)


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] software architectures in Ur/web?

[Adam Chlipala]

I only recognize "microservices" from your list of architectures, and I 
can say that one has been well-supported for a while.  It's easy to 
expose URL handlers that take in and produce formats like JSON.


On 10/18/19 12:01 PM, Marko Schuetz-Schmuck wrote:

I am aware of the paper "Ur/Web: A Simple Model for Programming the Web"
which does talk a bit about software architecture of Ur/web
applications. Has anyone considered architectures like layered
architecture, smart UI, microservices, Elm MVU, ... and how well they
lend themselves to use in Ur/web? Or what alternative architectures
arise naturally in Ur/web?


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur/Web -> JavaScript objects

[Adam Chlipala]

On 10/16/19 4:17 AM, Artyom Shalkhakov wrote:

I think this is what you are looking for:

https://github.com/vizziv/UrLib/blob/master/UrLib/record.urs#L36
https://github.com/vizziv/UrLib/blob/master/UrLib/record.ur#L23

It would be very nice if we as a community were to come up with a 
"batteries included" library for Ur/Web.
The equivalent code I maintain is in UPO 
, though I 
didn't bother to define this particular operator, since, as Mark showed 
us, it is so directly expressed with built-in operators.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur/Web -> JavaScript objects

[Adam Chlipala]

On 10/6/19 5:45 PM, Mark Clements wrote:
In defining an FFI to a JavaScript library such as Chart.js, config 
options may be defined in terms of (nested) JavaScript objects with a 
range of potential keys/fields. Analogous to the xml tags, is there 
any way to define a record type in Ur/Web that potentially includes a 
subset of fields?


In my own FFI wrapping so far, I have just given fields [option] types 
when they are optional, dealing with writing in [None] values for unused 
fields manually.  I don't think it's so bad!


Since I never miss an opportunity to show off metaprogramming in Ur/Web, 
here's a function you can use to cast a record to a wider type where all 
the new fields have [option] types.


fun expand [original ::: {Type}] [additional ::: {Type}] [original ~ 
additional]

   (fl : folder additional) (r : $original)
    : $(original ++ map option additional) =
    r ++ @map0 [option] (fn [t ::_] => None) fl

fun foo (x : {A : int, B : option string, C : float, D : option bool, E 
: string}) =

    42

val example = foo (expand {A = 3, C = 1.234, D = Some True, E = "hi"})


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Understanding Ur Inference Failure

[Adam Chlipala]

On 9/24/19 4:54 PM, Mario Alvarez wrote:
Finally, a quick follow-up question: is there any way to convince the 
Ur inference engine as it currently stands to solve this kind of 
problem? (For instance, would it be possible to write a type-level 
function to compute the overlap between the records in my example, or 
would this just lead to a different version of the same unification 
problem that the inference engine can't solve?)


I don't know a way to write it in today's Ur/Web, and let me try to 
explain why it is a big departure from existing features, to contemplate 
an extended unification approach.


Faced with a unification like [[A = int] = U1 ++ U2], it is ambiguous 
how to split the record literal among the two unification variables [U1] 
and [U2].  We could try both possibilities, but that would require 
backtracking to undo unification decisions.  As in classic ML type 
inference, Ur/Web's engine never backtracks past variable assignments.  
So we seem to need some unification approach that looks at multiple 
unsolved constraints at once, to make better choices.  Again, it is a 
fundamental design decision in both ML type inference and Ur/Web's to 
consider one unification constraint at a time, communicating between 
them only through side effects to assign values to unification variables.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Understanding Ur Inference Failure

[Adam Chlipala]

On 9/24/19 3:38 PM, Mario Alvarez wrote:
The idea behind the function is the following: I want to construct a 
record by combining together a record representing a set of 
customization options with a record representing a set of defaults.

[...]
fun recDif' [ts1 ::: {Type}] [ts2 ::: {Type}] [ts3 ::: {Type}] [ts1 ~ 
ts2] [ts2 ~ ts3] [ts1 ~ ts3]
           (fl : folder (ts2)) (r1 : $(ts1 ++ ts2)) (r2 : $(ts2 ++ 
ts3)) : $(ts1) =
    @fold [fn ts2 => ts1 ::: {Type} -> [ts1 ~ ts2] => $(ts1 ++ ts2) -> 
$(ts1)]

     (fn [nm ::_] [v ::_] [r ::_] [[nm] ~ r]
                  (f : ts1 ::: {Type} -> [ts1 ~ r] => $(ts1 ++ r) -> 
$(ts1))

[ts1] [ts1 ~ [nm = v] ++ r] (z : $(ts1 ++ ([nm = v]) ++ r)) =>
            f (z -- nm))
     (fn [ts1] [ts1 ~ []] (r : $(ts1 ++ [])) => r) fl ! r1

fun mergeDfl [more ::: {Type}] [overlap :: {Type}] [rest ::: {Type}]
    [more ~ overlap] [overlap ~ rest] [more ~ rest] (fl : folder overlap)
    (i1 : $(more ++ overlap)) (i2 : $(overlap ++ rest)) : $(more ++ 
overlap ++ rest) =

    (i1 ++ (@recDif' ! ! ! fl i2 i1))


Have you seen the triple-minus operator [---]?  I think it does your 
[recDif'], without the seemingly superfluous parameters.  You could 
replace the last line above with [i1 ++ (i2 --- overlap)].


Writing [recDif'] does seem to have been a useful exercise in Ur/Web 
metaprogramming!  Congrats on entering the elite club of people who have 
written new folds from scratch. >:)



I then attempt to run both of these functions on some simple examples:
[...]
val fails = mergeDflInfer {A = 1, B = 1} {B = 2, C = 3}
[...]
/mnt/c/Users/yorix/Code/Lunes/lunes.ur:191:35: (to 191:51) Error in 
final record unification

Can't unify record constructors
Have:  [A = int, B = int]
Need:   ++ 


In general, Ur inference isn't meant to solve equalities with just 
multiple unification variables concatenated together on one side.  You 
should always set things up so that there is at most one unification 
variable left when we get to unifying record types.  The underlying 
type-inference problem is undecidable, so we're fundamentally limited to 
using heuristics, and your case here didn't come up before to motivate a 
heuristic to support it.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Ban wildcards from signature files?

[Adam Chlipala]

An under-development compiler feature would behave more predictably if 
we could be sure that signatures never contain wildcards (underscores, 
standing for unknown types).  I don't think I've ever used a wildcard in 
a signature.


Would anyone object to making wildcards in signatures a compile-time error?


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Drop of several orders of magnitude in Techempower benchmarks

[Adam Chlipala]

On 8/5/19 5:17 PM, Oisín Mac Fhearaí wrote:

Update! The good news:
I was able to update the Dockerfile to build Ur/web from the latest 
release tarball (basically, using the old round 16 Dockerfile with a 
couple of small fixes like installing libicu-dev) and compare the 
benchmarks with the version installed with apt from the Ubuntu repo. 
The version built from the latest release was over ten times faster, 
even running on my old laptop.
Very interesting finding!  I've asked the Debian packager if he can 
think of some build-process change there that would have introduced a 
slowdown.

The bad news:
The latest version of Ur appears to fail the "fortunes" test with the 
following diff (there is more, but this seems to explain it):


fortune: -6Emacs is a nice operating system, but I 
prefer UNIX. — Tom Christaensen
fortune: +6Emacs is a nice operating system, but I 
prefer UNIX.  Tom Christaensen

fortune: @@ -17 +17 @@
fortune: -12フレームワークのベンチマーク
fortune: +12

It would seem that Unicode characters are being stripped from the 
output, causing the test to fail. I'm not familiar with exactly what 
the test is trying to do, and I don't know much about how Ur handles 
UTF-8.
That's odd.  I see the Unicode characters when I run that benchmark 
locally with a recent Git checkout of Ur/Web.  Are you sure you ran the 
database-setup scripts properly?  What happens when you query the 
database manually?  Are the right characters there?


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Drop of several orders of magnitude in Techempower benchmarks

[Adam Chlipala]

I'm glad you brought this up, Oisín.  I was already thinking of 
appealing to this mailing list, in hopes of finding an eager detective 
to hunt down what is going on!  I can say that I can achieve much better 
performance with the latest code on my own workstation (similar profile 
to /one/ of the several machines used by TechEmpower), which leads me to 
think something basic is getting in the way of proper performance in the 
benchmarking environment.


On 7/31/19 8:06 PM, Oisín Mac Fhearaí wrote:
I've noticed that Ur/web's performance benchmarks on Techempower have 
changed significantly between round 16 and 17.


For example, in round 16, Urweb measured 323,430 responses per second 
to the "Fortunes" benchmark.
In round 17 (and beyond), it achieved 4,024 RPS with MySQL and 2,544 
RPS with Postgres.


What could explain such a drastic drop in performance? The blog entry 
for round 17 mentioned query pipelining as an explanation for some of 
the frameworks getting much faster, but I don't see why Urweb's RPS 
would drop by a factor of 100x, unless perhaps previous rounds had 
query caching enabled and then round 17 disabled them.


Can anyone here shed light on this? I built a simplified version of 
the "sql" demo with the 2016 tarball version of Ur (used by the round 
16 benchmarks) and a recent snapshot, and they both perform at similar 
speeds on my laptop.


Oddly, the load testing tool I used (a Go program called "hey") seems 
to have one request that takes 5 seconds if I set it to use more 
concurrent threads than the number of threads available to the Ur/web 
program. Otherwise, the longest request takes about 0.02 seconds. This 
seems unrelated to the performance drop on the Techempower benchmarks, 
since the max latency is quite low there.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Pre-compressing static assets

[Adam Chlipala]

I can't think of a good way to do it with Ur/Web as it stands. It should 
be a pretty simple tweak to the compiler to specify an external program 
to run to transform this JavaScript code.


On 5/21/19 9:05 AM, Simon Van Casteren wrote:

Hey everybody,

I've been breaking my head today on how to do pre-compression of 
static assets, mainly the app.*.js bundle. Currently I'm having Nginx 
do on-the-fly compression using brotli at lvl 4. This causes my 
app.*.js bundle to shrink from 1.8 MB to 145 kB. This is really good 
already, but running it at lvl 11 gets me a 90 kB bundle, still 50% 
less than what I have now! Running it at lvl 11 takes around 5 seconds 
(on my underpowered server) though, which is really quite long.


In a normal situation I'd run the brotli compressor at build or 
deployment time, but the app.*.js bundle is never on the filesystem, 
so I haven't found a way to do this pre-compression in an Ur/Web context.


Anybody has any ideas?

Simon


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Mandatory nginx conf: merge_slashes off

[Adam Chlipala]

Done 
<https://github.com/urweb/urweb/commit/c4aba7a0befd9988ae032c5532790e5fabb321b9> 
now!  Thanks for the suggestion.


On 1/26/19 2:00 PM, Simon Van Casteren wrote:
If it's not much work, I'd say yes. What I mentioned won't happen 
often, but it was an extremely annoying thing to track down.


Simon

Op za 26 jan. 2019 om 19:33 schreef Adam Chlipala <mailto:ad...@csail.mit.edu>>:


Reviewing a PR just now, I'm reminded that the logic I
half-recalled to avoid empty serializations is only for strings. 
Would it be worth changing [unit] serialization to avoid empty
serializations there, too?

On 1/25/19 8:21 AM, Simon Van Casteren wrote:

It doesn't happen often of course, since you rarely use unit in a
page or RPC function. How I ran into it was actually via the now
fixed bug
https://github.com/urweb/urweb/issues/117, I made some ADT's that
got around that bug by declaring all constructors to have at
least one parameter, unit if nothing else. That came back to bite
me now...

A page with this signature:

val page: unit -> string -> transaction page

Would be affected by the issue I described. This obviously won't
happen much outside of you making a mistake (for example because
first the function took just a unit, then you added the string
parameter), but because it doesn't happen often and it's actually
nginx making the "mistake", I still thought it could help someone
out in the future!

Simon

    On Fri, 25 Jan 2019 at 13:57, Adam Chlipala mailto:ad...@csail.mit.edu>> wrote:

Thanks for sharing that wisdom!  Somehow I remember making a
special effort to encode empty strings with underscores,
precisely to avoid this problem (though it was appearing in
Apache, if I recall correctly).  Can you point us to an
example where it arises, in a URL that an Ur/Web app
generates itself?

On 1/25/19 5:13 AM, Simon Van Casteren wrote:

Hi,

I just ran into an awful problem combining urweb with nginx.
By default, nginx by default merges double slashes in urls,
eg: http://www.bla.com//users becomes
http//www.bla.com/users <http://www.bla.com/users>. This can
be a problem for UrWeb applications since a double slash is
actually how urweb encodes the unit or () value.

The solution is to use the option: "merge_slashes off".

It's not a bug in either application so I didnt want me make
an issue for it, but this could be useful info for other
people running Ur/Web programs behind nginx...

Simon



___
Ur mailing list
Ur@impredicative.com <mailto:Ur@impredicative.com>
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] New release

[Adam Chlipala]

A new release is available at:
 https://github.com/urweb/urweb/releases/tag/20190217

CHANGELOG for this release:

- Update of standard-library string functions to handle non-ASCII UTF-8 
properly

- New command-line options: -endpoints
- New .urp directive: safeGetDefault
- New Basis functions: textOfBlob, unsafeSerialized[To|From]String
- New Top functions: mapX4, foldR4
- New List functions: allM, assocAddSorted, mapConcat, mapConcatM, 
mapMi, searchM

- New ListPair functions: mapM, unzip
- New Option function: mapM
- Flycheck integration
- Bug fixes and improvements to type inference, documentation, error 
messages, and compatibility



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Explicitly asking for a sql rollback

[Adam Chlipala]

On 2/3/19 7:54 AM, Simon Van Casteren wrote:

About your first comment,

Yes I have the same code habit of first running validations and then 
doing the actual work. As long as stuff stays kind of simple that is 
manageable. But a place where this has caused some serious bugs was in 
my import page. So I have a function that runs validations and then 
makes the resource in the database. Now, my import page makes many of 
these at once, based on a CSV file format (see one of my previous 
questions). However when one fails, I'd like the whole import to fail. 
A complete rollback operation would make this much easier and less 
error-prone since I now have to delete all the previous saved resource 
when one resource fails to save. It was more of a question on how to 
do it though, since providing an explicit rollback is probably more 
dangerous than it's worth.


Right.  This part sounds doable by splitting your import functionality 
into separate validation and database insertion.  It sounds like a small 
drag, but at least it only locally affects your use case.


One example of a pain arising from general database rollback is: imagine 
a nicely encapsulated function that allocates a message-passing channel, 
stashes it in an appropriate database table, and returns it to the 
caller (perhaps declared as an abstract type, so the caller doesn't even 
know a channel is involved).  The caller uses the rollback function you 
asked for, but the caller also hangs onto and uses the channel.  Now we 
have a scary ability to break application-wide invariants: rollback is, 
in effect, a way to mess with "private fields" of library modules!



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Explicitly asking for a sql rollback

[Adam Chlipala]

On 2/3/19 5:24 AM, Simon Van Casteren wrote:
I'm wondering if there is a way to explicitly ask for a sql rollback. 
I think the only way you can now trigger a rollback would be by 
calling the "error" function and providing an xbody.


I have two use cases for which I think an explicit rollback mechanism 
(not sure how that would look like) would be handy. My main use case 
is rolling back everything when a validation is not ok. I don't use 
the "error" function because I can't return structured error messages. 
When I save some form with 5 fields, I mostly return an error object 
with the same 5 fields, so I can provide precise feedback to the user. 
Having to clean up all my sql work is huge drag and a source of subtle 
bugs.
Let me check that I understand: you want a transaction to return a 
structured value that will actually be processed further by legit code, 
say the client-side code that has called your server-side RPC?  However, 
you will undo all database effects, so that the transaction that leaked 
a result back to legit code that is now "apocryphal" in terms of 
database effects?  Wouldn't it be nicer to maintain a data structure in 
your RPC handler that batches all database updates until you are sure 
you really want to run them?  I wouldn't expect to see it complicate the 
code much.  In fact, I would naturally write database updates /after/ 
all validation, so that no special code complication is needed.
My second use case is testing with the database. I know some people 
frown upon incorporating the database into your tests, but I think 
that's silly so I'll ignore that. If have quite some tests that load 
stuff into the database as a setup step, then run some tricky query 
procedure, check the results, and then clear the DB again. This last 
step is again a big annoyance and a source of incorrectly failing tests.


I actually never use automated tests myself, but, if you do, they 
probably want to start each test with a predictable, pristine database 
state, and likely very small states suffice, right?  So then why not 
make your testing harness manage all this business outside of Ur/Web?


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Mandatory nginx conf: merge_slashes off

[Adam Chlipala]

Reviewing a PR just now, I'm reminded that the logic I half-recalled to 
avoid empty serializations is only for strings.  Would it be worth 
changing [unit] serialization to avoid empty serializations there, too?


On 1/25/19 8:21 AM, Simon Van Casteren wrote:
It doesn't happen often of course, since you rarely use unit in a page 
or RPC function. How I ran into it was actually via the now fixed bug
https://github.com/urweb/urweb/issues/117, I made some ADT's that got 
around that bug by declaring all constructors to have at least one 
parameter, unit if nothing else. That came back to bite me now...


A page with this signature:

val page: unit -> string -> transaction page

Would be affected by the issue I described. This obviously won't 
happen much outside of you making a mistake (for example because first 
the function took just a unit, then you added the string parameter), 
but because it doesn't happen often and it's actually nginx making the 
"mistake", I still thought it could help someone out in the future!


Simon

On Fri, 25 Jan 2019 at 13:57, Adam Chlipala <mailto:ad...@csail.mit.edu>> wrote:


Thanks for sharing that wisdom!  Somehow I remember making a
special effort to encode empty strings with underscores, precisely
to avoid this problem (though it was appearing in Apache, if I
recall correctly).  Can you point us to an example where it
arises, in a URL that an Ur/Web app generates itself?

On 1/25/19 5:13 AM, Simon Van Casteren wrote:

Hi,

I just ran into an awful problem combining urweb with nginx. By
default, nginx by default merges double slashes in urls, eg:
http://www.bla.com//users becomes http//www.bla.com/users
<http://www.bla.com/users>. This can be a problem for UrWeb
applications since a double slash is actually how urweb encodes
the unit or () value.

The solution is to use the option: "merge_slashes off".

It's not a bug in either application so I didnt want me make an
issue for it, but this could be useful info for other people
running Ur/Web programs behind nginx...

Simon


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Mandatory nginx conf: merge_slashes off

[Adam Chlipala]

Thanks for sharing that wisdom! Somehow I remember making a special 
effort to encode empty strings with underscores, precisely to avoid this 
problem (though it was appearing in Apache, if I recall correctly).  Can 
you point us to an example where it arises, in a URL that an Ur/Web app 
generates itself?


On 1/25/19 5:13 AM, Simon Van Casteren wrote:

Hi,

I just ran into an awful problem combining urweb with nginx. By 
default, nginx by default merges double slashes in urls, eg: 
http://www.bla.com//users becomes http//www.bla.com/users 
. This can be a problem for UrWeb 
applications since a double slash is actually how urweb encodes the 
unit or () value.


The solution is to use the option: "merge_slashes off".

It's not a bug in either application so I didnt want me make an issue 
for it, but this could be useful info for other people running Ur/Web 
programs behind nginx...


Simon
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Securing sessions in Ur/Web

[Adam Chlipala]

On 1/18/19 10:14 AM, Simon Van Casteren wrote:
When a person logs in, username-password style, I make a cookie with 
this form:


{ Role: 
, Email: string
, CreatedOn: time}

I'm saving the role in the cookie, so subsequent security checks in 
the page generators and rpc functions don't need to hit the database.
Actually, that's an insecure method.  The Ur/Web implementation is not 
meant to prevent cookie forgery!  Rather, it just tries to make sure any 
side-effecting operation that reads a cookie was triggered by an 
explicit form submission within your application (that's XSRF protection).
1. Is this safe? Is this a good solution? Or am I better off 
abandoning the whole thing and going back to putting just a SessionId 
inside a cookie and going to the database with that SessionId to check 
for authorization? Or another solution that I'm not thinking of at the 
moment?


Creating a unique and effectively unguessable session identifier to 
store in the database is a pretty good solution.  Actually, however, I 
recommend avoiding implementing your own authentication whenever 
possible!  You could consider using the Ur/Web World library 
, which is growing in a lazy manner, as 
different usage modes are requested.  Specifically, it's only been used 
for authentication via GitHub, as far as I know.


Passwords are just a sordid business, so best to avoid or at least push 
off onto some other web service, IMO.


2. A problem I'm having is storing the key that is needed to run the 
digest. My plan was to pass it via an environment variable to my 
program, but getenv inside a page generator causes the compiler to 
complain, saying that it could cause side-effects... Anybody have any 
ideas how to handle this? I feel like putting my key in plain text 
inside my source code is not very good, but maybe I'm wrong about that?


I don't see a fundamental security advantage of a sensitive value in a 
source file (and therefore compiled into the application) vs. in an 
environment variable (and therefore presumably appearing as plaintext in 
a script somewhere to set the variable).  I would even think there is a 
teeny bit of extra security in compiling the key into a binary on a 
build machine and then uploading the binary to a server that will only 
have the key appearing in the binary instead of a more-easily-viewed 
text file.  (Of course, even a modestly sophisticated adversary can grab 
a password out of a binary.)


However... it was an oversight that the compiler didn't recognize getenv 
as having only benign effects!  I believe I have fixed that issue now in 
the compiler, so please let me know if that method hasn't switched to 
working.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Producing XML (tags clash with built-in ones)

[Adam Chlipala]

The truth is, there has been minimal use so far of the built-in XML 
types to build other kinds of XML than HTML, as far as I know.  And, at 
the moment, I can't think of any workaround for tag names that clash 
with HTML tag names, without changing the compiler.  Suggestions are 
welcome!


It wouldn't be too big of a deal to build a separate FFI-based solution 
for your particular XML domain, I bet, not reusing the built-in XML support.


On 1/10/19 2:56 PM, Artyom Shalkhakov wrote:

Hello list,

I am working on this library [1] for producing Atom feeds.

The idea is to produce XML similarly to the way HTML is produced with 
Ur/Web. It is mostly going very nicely.


However, in the case of [entry] and [email] there exists a clash 
between the new tags and the existing tags defined in Basis and built 
into the compiler.


Questions:

1. Is it a good idea to produce XML like this? (So far I like it.)
2. If this approach is okay, then how to overcome this issue? I would 
except shadowing of tags to work the same way as shadowing of bindings. 



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] SQL table.field IN list

[Adam Chlipala]

Yes, "IN" isn't supported by Ur/Web at the moment, and I would be glad 
to see a PR adding support!  It could probably be as simple as modeling 
the second argument of "IN" as a regular Ur/Web list, processed 
internally with a fold similar to what Simon wrote externally (but 
generating "IN" syntax instead of a compound Boolean condition).


On 1/12/19 10:50 AM, Artyom Shalkhakov wrote:

Hi Simon,

сб, 12 янв. 2019 г. в 16:15, Simon Van Casteren :

Hi,

Am I correct in thinking that the standard library/compiler doesn't support SQL 
"IN" statements? It's something that I use a lot in my programs, and in psql 
for example you can just do:

SELECT *
FROM uw_lesson_lessons
WHERE uw_id in (1, 2, 3)


Yes, it doesn't seem to be supported at the moment.


I made my own function to handle this, using a bunch of sql_or statements:

fun inlist
   [a ::: Type]
   [otherfields ::: {Type}]
   [tablename :: Name]
   [columnname :: Name]
   [otherfields ~ [columnname = a]]
   (_ : sql_injectable a)
   (ids: list a)
 : sql_exp ([tablename = [columnname = a] ++ otherfields]) ([]) ([]) bool
   =
   List.foldl
 (fn id acc => (SQL {acc} OR {{tablename}}.{columnname} = {[id]}))
 (WHERE {[False]})
 ids

I'm not sure about the performance characteristics of this though. Anyway, just 
wondering if it is already supported but I can't find it, or it's not supported 
at all?


Well I think you should really file an issue for this on GitHub. I'd
like to work on it but it seems that it would require extending
Ur/Web's grammar, then adding some way to handle the right-hand side
of the operator -- which is an SQL tuple (right?), and we don't have
those in the syntax elsewhere except the INSERT clause handling. This
is a bit too much for my ability right now.

Other than that, I'm really in favor of adding it.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] I'm planning a new release in the first days of 2019.

[Adam Chlipala]

A bunch of good stuff has been merged into Ur/Web over the last few 
months, so I'd like to put out a new release shortly after I finish my 
current vacation.  Please let us all know if you think any further 
changes are worth making first.  The best way to give said notice is by 
submitting a PR on GitHub!



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Clarifying public API

[Adam Chlipala]

On 12/21/18 11:01 AM, Benjamin Barenblat wrote:

I’d like to change the way the liburweb API appears to consumers.
[...] As I see it, there ought to be
four categories of functions:

   1. functions that are public for FFI purposes,
   2. functions that are used in compiled code but should never be called
  by FFI libraries,
   3. functions that are internal to the runtime but need to be called
  across translation units, and
   4. static functions.
That sounds like a reasonable categorization.  I hadn't mentally 
distinguished too much between categories 2 and 3, but otherwise this 
system matches my thinking.

I think only public functions (category 1) should be listed in urweb.h.
Functions needed by compiled code but not available for the FFI
(category 2) should go in their own header file, and to emphasize their
internal nature, we shouldn’t install that header in /usr/include but
rather in /usr/share/urweb. Internal functions needed across translation
units (category 3) should be declared in headers that are only used
while compiling the runtime and not installed at all.
I could go along with that.  My current model is that the manual lists 
all category-1 functions, though I may have missed some that belong 
there.  As for physically separating categories across header files, I 
see the benefit of more detail/encapsulation conveyed by 
machine-processed documentation (headers).  I also see the downside of 
added complexity in compilation and use of the file system.

The major challenge here is figuring out exactly what the public API
should be. What functions and types should we expose to FFI consumers?
See last paragraph of my answer.  I have always thought the manual 
already answers this question, and it's a documentation bug if not.

But do FFI libraries really need to call, say,
uw_Basis_strlen, when there’s a perfectly reasonable strlen in libc that
does the same thing?
No, they shouldn't, and that's why I didn't list any 'uw_Basis_*' 
functions in the manual.  However, you picked a funny example, since 
things have recently been getting interesting there, with support 
(mostly by Fabrice Leal) for internationalization in the runtime 
system!  As a person unfamiliar with how all that business works, I 
might indeed be tempted to call uw_Basis_strlen from C FFI code!


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] about the -static compiler flag

[Adam Chlipala]

On 11/23/18 5:04 AM, Chris Double wrote:

It's possible to get a complete static executable from urweb by using
musl-libc [1] and a workaround. I tried with a simple "hello world"
type project, with musl installed:

$ urweb -protocol http -output test -ccompiler musl-gcc -static hello1


Neat!  So just running the 'configure' script with the right arguments 
can enable the right command line.



Would you be interested in a PR for replacing timelocal usage?
I'm always interested in PRs that substitute behavior-equivalent code 
that relies less on functions from outside appropriate standards like 
POSIX (assuming said PRs don't bring in tons of hard-to-maintain code).  
Is timelocal such a case?


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] about the -static compiler flag

[Adam Chlipala]

I don't know if this GitHub issue 
 is related, but in general I 
made a token effort (about 10 years ago) to support static linking by 
adding one flag to the GCC/Clang command line, and it has been clear for 
years that more modifications are needed somehow.  I don't intend to 
research them myself since I literally always use dynamic linking for 
Ur/Web apps, but I would be very glad to see related PRs.


On 10/27/18 7:32 PM, Fabrice Leal wrote:
So as I was trying to make a release for deployment on a cloud vm, I 
tried to compile a fastcgi executable using the -static option but I 
get some warnings and some errors from what it seems to be undefined 
references to SSL_ function calls - to successfully deploy i had to 
copy a bunch of .so files which is not ideal, but I got it working. 
Wonder what everyone's experience is or if im missing something.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] calling javascript code in

[Adam Chlipala]

Good.  I think that's been true all along.  Thanks for confirming!

On 10/24/18 5:35 PM, Fabrice Leal wrote:

@adamChlipala

I can confirm in my end (urweb master) I get a type error when i try 
to use onload on a 


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Tooling: type of an expression

[Adam Chlipala]

It doesn't sound too hard, and I'd be glad to see a patch for it; and 
feel free to open a GitHub issue.


On 10/24/18 4:11 AM, Simon Van Casteren wrote:

Is there a possibility for -dumpTypes to also dump values in let bindings?

Op do 11 okt. 2018 om 16:33 schreef Adam Chlipala <mailto:ad...@csail.mit.edu>>:


Well, you could take advantage of the type-inference daemon and
run a new compilation job with your extra expression added to the
build.

On 10/11/2018 02:56 AM, Simon Van Casteren wrote:

I think that would get me to the first level: getting types of
identifiers. Do you see any way to evaluate expressions and
getting the types of those?

This is something that would definitely be worth it for me, so
I'll be implementing it unless I can't figure it out :).

Simon

On Thu, Oct 11, 2018, 5:20 AM Adam Chlipala mailto:ad...@csail.mit.edu>> wrote:

I'm sure it's more than just remotely possible and is just a
question of
someone getting hands dirty and writing the code!  The
baseline of a
whole-program compiler could make it trickier than for many
other
toolsets, but it could work to periodically run "compiles"
through type
inference, saving the results to hidden files.

On 10/10/2018 08:22 PM, Simon Van Casteren wrote:
> Urweb tooling is pretty limited compared to other
languages. I knew
> that when I started with it and so far I'm OK with it.
Honestly, most
> of the "modern" tooling I see in other ecosystems is a
waste of time.
>
> However, the one thing that would really cut dev time in
half for me
> in Ur/web (slightly exaggerated for effect) would be being
able to
> have the compiler tell me the type of an expression. You
can go
> multiple levels deep here:
>
> - type of an identifier
> - type of an expression at top level
> - type of an expression in function definition,
let-binding, etc
>
> I'm sending this email to the mailing list to ask if
something like
> this is remotely possible, what kind of approach we can
take and how
> we could go about implementing it.
>
> Any help much appreciated


___
Ur mailing list
Ur@impredicative.com <mailto:Ur@impredicative.com>
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] calling javascript code in

[Adam Chlipala]

Sorry, just to be clear: to the best of my knowledge, type errors are 
already generated when trying to use 'onload' with tags other than 
!  Is that not the case?


On 10/24/18 12:05 AM, Aistis Raulinaitis wrote:

Adam,

Yes, I've noticed ignored `onload` on tags other than `body`.

It would be good to have a type error or allowing it more broadly.

Aistis

On Mon, Oct 22, 2018 at 11:41 AM Adam Chlipala <mailto:ad...@csail.mit.edu>> wrote:


Belated follow-up on this remark: now that I look at the types
from the standard library, I see that 'onload' is statically
disallowed for  and indeed most other tags.  Is that what you
meant?  It could be reasonable to add 'onload' more widely, but
currently including it for most tags should not have 'no effect'.
Instead, it should trigger type error messages!

On 7/5/18 2:05 PM, Adam Chlipala wrote:

On 07/05/2018 01:43 PM, Fabrice Leal wrote:

I found out too late for my own good that onload only works for
, placing it in a  as no effect


Oh, I didn't realize that some event attribute was systematically
ignored.  That might qualify as a bug!




___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] calling javascript code in

[Adam Chlipala]

Here's a hypothesis: if you return a  at the top level 
of a generated page (after adding the attribute by changing basis.urs), 
it will actually do what you expect.  However, if you embed such a  
within dynamically generated content, even the /initial value/ of such a 
dynamic region, the 'onload' handler is not called.  The reason is that 
the dynamically generated  actually isn't there at the moment when 
the page loads; it is only created by JavaScript code running thereafter.


Does that hypothesis seem to match your prior situation?

On 10/22/18 6:50 PM, Fabrice Leal wrote:

@AdamChlipala

At the time I implemented an onload attribute for  on basis.ur 
and only later found out if was for no good on html/js land: the only 
onload that gets triggered is the one defined on , setting 
onload for any other child tag has no "side effects"; so I scrapped that.


Sorry for the vagueness :)

I did end up using  and that worked for me


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] calling javascript code in

[Adam Chlipala]

Belated follow-up on this remark: now that I look at the types from the 
standard library, I see that 'onload' is statically disallowed for  
and indeed most other tags.  Is that what you meant?  It could be 
reasonable to add 'onload' more widely, but currently including it for 
most tags should not have 'no effect'.  Instead, it should trigger type 
error messages!


On 7/5/18 2:05 PM, Adam Chlipala wrote:

On 07/05/2018 01:43 PM, Fabrice Leal wrote:
I found out too late for my own good that onload only works for 
, placing it in a  as no effect


Oh, I didn't realize that some event attribute was systematically 
ignored.  That might qualify as a bug!
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Should we have contributor guidelines for the Ur/Web project?

[Adam Chlipala]

An old-ish GitHub issue  asks 
for posting of clear guidelines for new contributors.  What does 
everyone think about whether that makes sense?  I feel like there have 
been quite a few successful contributors already without such 
guidelines, but who knows which others are being turned away.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Tooling: type of an expression

[Adam Chlipala]

Well, you could take advantage of the type-inference daemon and run a 
new compilation job with your extra expression added to the build.


On 10/11/2018 02:56 AM, Simon Van Casteren wrote:
I think that would get me to the first level: getting types of 
identifiers. Do you see any way to evaluate expressions and getting 
the types of those?


This is something that would definitely be worth it for me, so I'll be 
implementing it unless I can't figure it out :).


Simon

On Thu, Oct 11, 2018, 5:20 AM Adam Chlipala <mailto:ad...@csail.mit.edu>> wrote:


I'm sure it's more than just remotely possible and is just a
question of
someone getting hands dirty and writing the code!  The baseline of a
whole-program compiler could make it trickier than for many other
toolsets, but it could work to periodically run "compiles" through
type
inference, saving the results to hidden files.

On 10/10/2018 08:22 PM, Simon Van Casteren wrote:
> Urweb tooling is pretty limited compared to other languages. I knew
> that when I started with it and so far I'm OK with it. Honestly,
most
> of the "modern" tooling I see in other ecosystems is a waste of
time.
>
> However, the one thing that would really cut dev time in half
for me
> in Ur/web (slightly exaggerated for effect) would be being able to
> have the compiler tell me the type of an expression. You can go
> multiple levels deep here:
>
> - type of an identifier
> - type of an expression at top level
> - type of an expression in function definition, let-binding, etc
>
> I'm sending this email to the mailing list to ask if something like
> this is remotely possible, what kind of approach we can take and
how
> we could go about implementing it.
>
> Any help much appreciated

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Error compiling "Anonymous function remains at code generation"

[Adam Chlipala]

Short answer before I can investigate in more detail: it is expected 
that the Ur/Web compiler give that kind of terrible error message in 
many cases that don't nest server-side and client-side code properly.  
Some day it should be enforced with a type system, yielding better error 
messages, but that day is not yet upon us!


On 09/19/2018 04:05 PM, Fabrice Leal wrote:
ok so this was itching me so I decided to try to isolate whatever is 
at fault. and I think I created the simplest sample to reproduce the 
problem:


https://github.com/fabriceleal/urweb-test

so I'm assuming the problem is not at my end and will try to do the 
parsing on my own until the urweb-regex lib gets updated


On Tue, Sep 18, 2018 at 11:01 PM Fabrice Leal 
mailto:fabrice.leal...@gmail.com>> wrote:


I'm having this weird error while trying to compile urweb using
urweb-regex; if I isolate that page in a separate module, it
compiles fine (even though I seem unable to access that page from
the browser), so I assume I'm doing something wrong in my
helloworld.ur file.

Would appreciate some pointers; Source file is this one

(https://github.com/fabriceleal/urweb-experiments/blob/doesnt_compile/helloworld.ur#L869)
and I also included the result of -dumpVerboseSource

(https://github.com/fabriceleal/urweb-experiments/blob/doesnt_compile/dumpVerboseSource.txt#L7705)

That FFI maybe_onload is particularly suspicious ... is the call
to parsePgn being "lifted" to javascript code? Some time ago I had
some errors while trying to use the rpc function in the loadPost
page because i was mixing it with code that uses my canvas library
which has a bunch of clientOnly FFI calls; I reorganized my code
and eventually made it work nicely

(https://github.com/fabriceleal/urweb-experiments/commit/503da7e28f1a05be6e69e9f60c9cd321bfa252ce
IIRC). I tried to isolate the testParse function but seems to not
lead anywhere.

Sorry for the wall of text and thanks in advance :)

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Parsing text files

[Adam Chlipala]

On 09/17/2018 04:11 PM, Fabrice Leal wrote:
I wanted to parse a text file with a non trivial syntax 
(https://en.wikipedia.org/wiki/Portable_Game_Notation) and was 
wondering what would be the best way to achieve this. The best option 
seems to be maybe FFI with C or haskell ... would it be too crazy to 
do this with plain urweb?


I don't see what would be wrong with parsing in Ur/Web directly. That's 
how I've always done parsing in Ur/Web apps.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] about the UrFlow Demos

[Adam Chlipala]

Right, that's the paper I was referencing.  It has a fine vintage by now.

On 09/11/2018 04:24 AM, Fabrice Leal wrote:

oh that's a pity, i was looking forward to play with this feature :\
you mean your "Static Checking of Dynamically-Varying Security 
Policies in Database-Backed Applications" i assume?


On Mon, Sep 10, 2018 at 9:44 PM Fabrice Leal 
mailto:fabrice.leal...@gmail.com>> wrote:


Hi, I downloaded the scdv.tgz and tried to compile the demos but
had to fix a "wrap" function used throughout the poll, calendar,
gradebook and forum demos:
it seems that just replacing the arguments title and body with
"titl" and "bod" gets rid of the compilation errors, and then I
seem to be able to run the demos normally.

However when i run urweb with the -iflow switch, I get a few
"Information flow checker can't parse SQL query" notices, so I'm
not sure if I'm missing something or if there's anything needing
fixing.

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] about the UrFlow Demos

[Adam Chlipala]

It seems I stopped bothering to update those demos over the last few 
years.  Sorry!  If it makes you feel any better, that feature was never 
really production-quality, so you'd might as well learn about it by 
reading a paper instead of running a real compiler. ;)


On 09/10/2018 04:44 PM, Fabrice Leal wrote:
Hi, I downloaded the scdv.tgz and tried to compile the demos but had 
to fix a "wrap" function used throughout the poll, calendar, gradebook 
and forum demos:
it seems that just replacing the arguments title and body with "titl" 
and "bod" gets rid of the compilation errors, and then I seem to be 
able to run the demos normally.


However when i run urweb with the -iflow switch, I get a few 
"Information flow checker can't parse SQL query" notices, so I'm not 
sure if I'm missing something or if there's anything needing fixing.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Interested in getting involved with a startup company?

[Adam Chlipala]

This message is going to be a bit of deja vu, with regards to a similar 
one I sent to this list about 10 years ago.


I'm trying to spin up a startup company building on Ur/Web and UPO 
 to provide a platform where people with no 
programming training can create web applications quickly.  So many 
aspects of the plan are indeterminate at the moment, but I will need 
collaborators who are effective at Ur/Web programming.  In the initial 
phases, these folks need to have relatively high tolerance for risk, 
what with likely iterating to make a few initial customers happy with 
the product, with no financial compensation yet, before raising venture 
capital.  (Afterward, I'd expect everyone to have both stock and salary.)


If you're interested in discussing more, please get in touch with me, 
with any relevant information on your background relevant to Ur/Web 
programming or any other subject that seems apropos to running a company 
selling a product for authoring and automatic cloud hosting of web 
applications.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Project binary milestone of the year

[Adam Chlipala]

I wasn't paying close enough attention and missed when the Ur/Web 
repository on GitHub passed 512 stars, but that doesn't mean I can't 
still propose a brief celebration now!  Thanks, everyone, for your 
interest in the project and help hunting down bugs and dreaming up 
feature ideas.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Struggling to figure out mapping of record

[Adam Chlipala]

On 08/18/2018 08:43 AM, Simon Van Casteren wrote:

{Age: option float, FirstName: string}

[...]

{Age: option float -> either string int, FirstName: string -> either 
string string}


[...] Output should be of the type:

{Age: either string int, FirstName: either string string}

I feel Ur should be able to do it but I can't figure it out. I keep 
going back to Top.map2, but there the "to" and "from" types should be 
type level functions from a certain K to a and b, but my records are 
monomorphic and don't really have any relation between them except for 
the record of mapping functions.


Actually, your records look like each field has a particular fundamental 
type pair, e.g. [option float] and [int] for [Age] and [string] and 
[string] for [FirstName].  So you can build a type-level record of pairs 
of types, that is, with kind [{(Type * Type)}], and use [map2] very 
naturally!


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Reading files uploaded by a user

[Adam Chlipala]

On 08/11/2018 04:34 PM, Simon Van Casteren wrote:
I want to provide import functionality of this data and I feel CSV 
files are probably the best way to go with this. Microsoft Excel 
exports these, database programs can export these they're 
human-readable, etc.


I know Ur/Web supports file upload with the file and blob types, but I 
don't know where to go from there.


I just use textboxes for CSV upload, in a few different production 
deployments based on UPO .  I have to admit, 
it isn't obvious that there shouldn't be a [blob -> string] function in 
the standard library, so I'd be open to adding that, too, if it sounds 
like the demand is there.



BTW: Thanks for Ur/Web, it's been a godsend for me.


Glad to hear you're getting some mileage out of it!  I'm sure the crowd 
here will be interested to hear more details of your applications, when 
they're far enough along (and I like to add links from the Ur project site).
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] calling javascript code in

[Adam Chlipala]

On 07/05/2018 01:43 PM, Fabrice Leal wrote:
I found out too late for my own good that onload only works for 
, placing it in a  as no effect


Oh, I didn't realize that some event attribute was systematically 
ignored.  That might qualify as a bug!
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] calling javascript code in

[Adam Chlipala]

Oh, right.  The  tag should do just as well, in that case.  
You'd need to return an empty XML document explicitly, but that's not hard.


On 07/05/2018 09:43 AM, Simon Van Casteren wrote:
Side note: the 

Re: [Ur] calling javascript code in

[Adam Chlipala]

Let me try to disentangle the potential parts of your question.

I hope you are not asking about literally writing code in JavaScript.  I 
will proceed as though you are actually asking about /client-side code/, 
but let me know if I misunderstood.  (It is a rather nice feature of 
Ur/Web that writing Ur/Web programs need not involve JavaScript at all, 
anymore than we talk about "transistors" when reading JavaScript code!)


So, then, I conclude that your question is how to add a listener on a 
[source], to run arbitrary client-side code whenever the source 
changes.  You seem to be on a good track there, with the mention of a 
dummy node.  I would create a  node that generates only a 

Re: [Ur] about

[Adam Chlipala]

I remember that someone put a proof-of-concept canvas interface on 
GitHub at some point, but now I forget the details.  Certainly there is 
nothing within the urweb GitHub organization.


On 06/21/2018 11:11 AM, Benjamin Barenblat wrote:

On Thursday, June 21, 2018, at  5:11 AM EDT, Fabrice Leal wrote:

are there any plans to support the  tag?

I'm not aware of anybody working on it right now. An FFI library that
presented an FRP interface to canvas would be pretty cool, though.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] New release

[Adam Chlipala]

I'm trying out a new release method, based on the GitHub feature of the 
same name.  You can find this release at:

    https://github.com/urweb/urweb/releases/tag/20180616

CHANGELOG for this release:

- New feature to cache files stored in the database as blobs, via the
  'filecache' .urp directive
- New .urp directives: 'mimeTypes' and 'file' (new long form)
- New HTML pseudo-tag: 
- New HTML tag attributes: 'oninput', 'onscroll', 'title', 'size'
- New standard-library functions: 'List.findM' and 'List.existsM'
- New '-help' command-line option for compiler
- Remove insecure function 'Basis.crypt' (which didn't seem to have any 
users)

- Selenium-based automatic testing
- Bug fixes and improvements to documentation and error messages

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Thoughts on cryptographic hashing for Ur/Web standard library?

[Adam Chlipala]

That sounds like a pretty credible plan!  If no one objects by, say, the 
end this coming Monday, I will feel free to remove 'crypt' from the 
standard library, counting on others to figure out the right way to 
materialize a more comprehensive freestanding library.


On 05/23/2018 12:22 PM, Benjamin Barenblat wrote:

On Saturday, May 19, 2018, at 3:52 pm -0400, Adam Chlipala wrote:

It has been pointed out <https://github.com/urweb/urweb/pull/114> that
Ur/Web's Basis.crypt uses DES, a weak hashing approach by today's
standards.  I can think of a few potential courses of action:

[...]

  2. Switch to a different cryptosystem available in OpenSSL's libcrypto,
 which is already linked with all Ur/Web apps.
  3. Realize that literally no one is using this function and just delete
 it from the standard library.  (A less severe version is to ask a
 small but nonzero-size user community to switch to using separate
 libraries for this functionality.)

I think we should pursue both of these: Remove crypt from the standard
library, and replace its functionality with external libraries that
depend on OpenSSL.

I wrote bindings for the OpenSSL MD5, SHA-1, and SHA-2 APIs a while
back [1]. They're Apache-licensed. I'd love to see them get wider
use, and I'd welcome patches to add additional hash functions. I've also
written a bcrypt wrapper [2], so you've got two options if you want to
use bcrypt (the other being [3]). I AGPL-licensed my bcrypt wrapper, but
I'd be happy to relicense to Apache.

There may also be room for a general-purpose OpenSSL library for
Ur/Web. Such a library would bring the useful parts of the OpenSSL API
(data hashing, HMACs, password hashing, AES, ChaCha20/Poly1305, etc.) to
all Ur/Web applications and would effectively supersede [1]. I've been
working on something similar for Haskell [4], which could be a useful
model.


[1] https://benjamin.barenblat.name/git/urweb-crypto-hash-openssl.git
 https://github.com/bbarenblat/urweb-crypto-hash-openssl

[2] https://benjamin.barenblat.name/git/urweb_bcrypt.git
 https://github.com/bbarenblat/urweb_bcrypt

[3] https://github.com/steinuil/urweb-bcrypt

[4] https://github.com/google/btls

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Thoughts on cryptographic hashing for Ur/Web standard library?

[Adam Chlipala]

After a busy semester, I am going through the backlog of Ur/Web issue 
reports.  I'm hoping to make a new Ur/Web release soon, and here is the 
first in what may be a series of community queries, to decide whether 
certain changes are appropriate.


It has been pointed out  that 
Ur/Web's Basis.crypt uses DES, a weak hashing approach by today's 
standards.  I can think of a few potential courses of action:


1. As in the linked PR, just add a comment essentially saying "hey,
   this crypto isn't so great."
2. Switch to a different cryptosystem available in OpenSSL's libcrypto,
   which is already linked with all Ur/Web apps.
3. Realize that literally no one is using this function and just delete
   it from the standard library.  (A less severe version is to ask a
   small but nonzero-size user community to switch to using separate
   libraries for this functionality.)

Any thoughts?

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Multitenancy

[Adam Chlipala]

Right, that all makes sense.  It should be easy to set up a shell script 
from first principles, with no particular support from Ur/Web.  Then 
calling that shell script from an Ur/Web app with the C FFI should also 
be straightforward -- just be sure to register the execution of the 
script as a transactional with no rollback handler.


On 05/13/2018 02:19 PM, Simon Van Casteren wrote:
In general, not really. And at the moment I don't have time to 
implement the automation so I for sure will do it manually. But I plan 
to add a "Demo" button where people can check out the whole 
application with some demo data and can do whatever they want. I 
wanted to implement that also as a seperate tenant, and after a few 
days of inactivity delete those "demo tenants".


Secondly, as a client I would appreciate it if I could buy this 
product and immediately get my environment up and running, so not 
having to wait minutes-hours until I can start using what I bought. 
This is not that important right now, but I would like to have the 
possibility.


2018-05-13 20:11 GMT+02:00 Adam Chlipala <ad...@csail.mit.edu 
<mailto:ad...@csail.mit.edu>>:


I'm confused about something: do you really expect to add new
tenants frequently enough that it would be a problem for you to
have to log into the server and run a shell script each time? 
Would it even be a problem if you had to edit configuration files
manually on the server each time?

On 05/13/2018 02:02 PM, Simon Van Casteren wrote:

As I see it now, I'll probably have an API endpoint
"new_tenant" that will run the following:

* Run a shell script to set up a new DB and load default data.
* Write the necessary config for a new fastCGI server with the
new connection string into my nginx config and reload nginx,
as I've read this should not impact the other servers. I'll
probably add some notification to myself whenever I do this so
I don't silently start thousands of servers when something
goes wrong.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Multitenancy

[Adam Chlipala]

I'm not sure which aspect of deployment you're worried about.  With 
Apache, you can configure as many FastCGI applications as you'd like, 
and they will all be started automatically on each reboot.  It only 
takes a few lines of configuration per application.  Similarly, creating 
a new database is a few lines of shell script, using the .sql file that 
the Ur/Web compiler produces for an application.  All of the details are 
independent of application specifics.


I am not aware of any existing tools for doing these simple steps 
automatically, but it should be easy to roll an all-inclusive shell script.


On 05/13/2018 09:48 AM, Simon Van Casteren wrote:
I considered it briefly as I was doing some research on the topic. 
It's the first time I'll be running and deploying a SaaS app myself 
(I've so far always been on the programming side only) so it felt more 
natural to me to keep everything inside a single application. Running 
the application right now consists of me ssh'ing into a Linode and 
running the exe by hand. If I want to split this into one application 
per database (which does guarantee data security better, that's really 
nice) then deployment seems to become much more complicated.


But let's say I do go that route. Is using one of the new deployment 
tools a good idea for a just-started scenario? I appreciate how ur/web 
uses very basic and simple tools, eg: Using curl in the Worldffi 
project to do HTTP requests, not having editor tooling but having the 
compiler use standard error formatting so emacs picks it up 
automatically. This is in strong contrast to the javascript community 
where I normally reside, which likes to re-implement things a lot. So 
I'd like to know what advice the community has on the right tools for 
setting up a new application and database automatically (probably via 
the C FFI?) and then running and updating them together. I would like 
to note that adding and running new clients without any manual work is 
strongly preferred.


Because I don't have any idea of how I would handle this adding and 
deploying of clients, I can't weigh the two alternatives: Complicating 
the app with tenantIds, or complicating the deployment with seperate 
apps.


2018-05-13 15:31 GMT+02:00 Adam Chlipala <ad...@csail.mit.edu 
<mailto:ad...@csail.mit.edu>>:


Can you explain why you don't want to run separate applications
with separate databases?


On 05/13/2018 05:50 AM, Simon Van Casteren wrote:

Hi,

I'm in the process of making a new application for music schools,
using ur/web for front and backend. I'm at the point where I have
two customers and am starting to implement support for multiple
clients/tenants in one DB (postgres). I've been planning to
implement multitenancy from the start, but haven't had the time yet.

Has anyone implemented a form of multitenancy in ur/web before?

I see two areas that need consideration.

1. Deciding which user belongs to which tenant. Ideally I'd have
a seperate url for each tenant that I can give out to my clients
(=the schools), do some dns magic to send them all to the same
exe, extract the tenantname from the url and save the tenantId in
a cookie. Also ideally, the user's url would not change, ie. All
urls should go to myschool.coolschools.be
<http://myschool.coolschools.be> during a session, not getting
redirected at all. This is all in an ideal situation of course.

2. Database access: I'll have tenantId columns in all tables +
foreign keys and indexes on these columns. I'm a bit afraid I'll
forget adding tenantId = cookie.tenantid somewhere, so I was
thinking I could make a function that takes a sql_exp and a
tenantId and adds these clauses to all tables involved. Not 100%
sure that will work but I think it's possible, I haven't had to
dive into the internals of sql_exp yet. Secondly, I wonder if I
can somehow declare my endpoints to be tenantdepandent (all but
the most general will be) maybe via newtyping the transaction
datatype and then allowing the execute only sql queries that have
the above function applied. Just dreaming out loud here.

I'd be very interested in any ideas or examples!

Simon




___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Multitenancy

[Adam Chlipala]

Can you explain why you don't want to run separate applications with 
separate databases?


On 05/13/2018 05:50 AM, Simon Van Casteren wrote:

Hi,

I'm in the process of making a new application for music schools, 
using ur/web for front and backend. I'm at the point where I have two 
customers and am starting to implement support for multiple 
clients/tenants in one DB (postgres). I've been planning to implement 
multitenancy from the start, but haven't had the time yet.


Has anyone implemented a form of multitenancy in ur/web before?

I see two areas that need consideration.

1. Deciding which user belongs to which tenant. Ideally I'd have a 
seperate url for each tenant that I can give out to my clients (=the 
schools), do some dns magic to send them all to the same exe, extract 
the tenantname from the url and save the tenantId in a cookie. Also 
ideally, the user's url would not change, ie. All urls should go to 
myschool.coolschools.be  during a 
session, not getting redirected at all. This is all in an ideal 
situation of course.


2. Database access: I'll have tenantId columns in all tables + foreign 
keys and indexes on these columns. I'm a bit afraid I'll forget adding 
tenantId = cookie.tenantid somewhere, so I was thinking I could make a 
function that takes a sql_exp and a tenantId and adds these clauses to 
all tables involved. Not 100% sure that will work but I think it's 
possible, I haven't had to dive into the internals of sql_exp yet. 
Secondly, I wonder if I can somehow declare my endpoints to be 
tenantdepandent (all but the most general will be) maybe via newtyping 
the transaction datatype and then allowing the execute only sql 
queries that have the above function applied. Just dreaming out loud here.


I'd be very interested in any ideas or examples!

Simon


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] SVG Test based on ListEdit.ur

[Adam Chlipala]

Yes, I'm sorry, but the  tag is only for HTML and the DOM.  It 
would take extra implementation effort to make it compatible with SVG, 
and that effort has not yet been made... so it's good that the compiler 
is raising a static error!


On 05/01/2018 06:04 PM, Jonas Mellin wrote:


Dear all, I have tried to adapt ListEdit.ur in the tutorial to a small 
SVG application that adds circles to the screen as you double click 
(the code is at the end). The SVG.urs is found at 
https://github.com/karsar/urweb-examples/blob/master/SVGTest/SVG.urs


I get a problem at row 57 “” and also at 
line 22 “show' (pl : plist) : signal xsvg   =” where the compiler gets 
stuck on “Error in final record unification


Can't unify record constructors”. My hypothesis is that there is some 
problem between html and SVG.


An excerpt of the error messages sis:

/home/a/SVGTest5/SVGTest.ur:57:3: (to 58:8) Error in final record 
unification


Can't unify record constructors

Have:  ++ [Dyn = ()]

Need:  [Svg = ()]

= CODE =

[...]

    stroke="red" fill="blue"/>


[...]

and show' (pl : plist) : signal xsvg   =

    case pl of

Nil => return 

| Cons {Point = p, Tail = t } => return 

    





___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] UR/Web SVG (ffi) question

[Adam Chlipala]

I think it should all "just work," with your new tag added in an FFI 
.urs file like that!


On 04/17/2018 08:00 AM, Jonas Mellin wrote:


My bad, sorry. It took me a short while to see the misspelling. Got it 
working. I will be more careful about that in the future.


I move on to trying multiple objects and then adding “foreignObject” tag:

val foreignObject : svgTag([X = string, Y = string, Width = string, 
Height = string] ++ typicalAttrs)


an addition to the SVG.urs (cf. original at 
https://github.com/karsar/urweb-examples/blob/master/SVGTest/SVG.urs) 
, this require somehow to mix xsvg with xbody. Anything in particular 
that has to be taken into account when mixing this?


/Jonas Mellin

*From:*Ur [mailto:ur-boun...@impredicative.com] *On Behalf Of *Adam 
Chlipala

*Sent:* den 17 april 2018 13:20
*To:* ur@impredicative.com
*Subject:* Re: [Ur] UR/Web SVG (ffi) question

For future questions, I think it would be good for you to explain what 
you understand from error messages, highlighting what additional 
understanding you need to diagnose the error. Here again the problem 
is a simple one that would be recognized as a bug in any programming 
language.


Notice the difference in spellings of field names, between the "Have" 
and "Need" parts of the error message.


On 04/17/2018 05:53 AM, Jonas Mellin wrote:

...

   set x (ev.ScreenX,ev.SceenY)}>

...

*But I get:*

Can't unify record constructors

Have:

[ScreenX = int, ScreenY = int, ClientX = int, ClientY = int,

  CtrlKey = bool, ShiftKey = bool, AltKey = bool, MetaKey = bool,

  Button = mouseButton]

Need: <UNIF:U140::{Type}> ++ [ScreenX = int, SceenY = int]



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] UR/Web SVG (ffi) question

[Adam Chlipala]

For future questions, I think it would be good for you to explain what 
you understand from error messages, highlighting what additional 
understanding you need to diagnose the error.  Here again the problem is 
a simple one that would be recognized as a bug in any programming language.


Notice the difference in spellings of field names, between the "Have" 
and "Need" parts of the error message.


On 04/17/2018 05:53 AM, Jonas Mellin wrote:

...

   set x (ev.ScreenX,ev.SceenY)}>

...

*But I get:***

Can't unify record constructors

Have:

[ScreenX = int, ScreenY = int, ClientX = int, ClientY = int,

  CtrlKey = bool, ShiftKey = bool, AltKey = bool, MetaKey = bool,

  Button = mouseButton]

Need:  ++ [ScreenX = int, SceenY = int]



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] UR/Web SVG (ffi) question

[Adam Chlipala]

I have not read all of your code, but I did spot the problem behind the 
first compiler error message, which I think all web developers would 
agree is problematic. (I.e., it isn't just a question of a fussy Ur/Web 
type system.)


On 04/16/2018 04:58 AM, Jonas Mellin wrote:


fun proc (x: intPair) =

x <- source x;

return

 

    set x 
(ev.ScreenX,ev.SceenY)}>




   

fun main(): transaction page =

xml <- proc (0,0);

return

 

   

 Banzai

   

   

 {xml}

   

 

[...]


/home/a/SVGTest2/SVGTest.ur:33:4: (to 44:2) Error in final record 
unification


Can't unify record constructors

Have:  [Dyn = (), MakeForm = (), Body = ()]

Need:  [Html = ()]



Notice that your [proc] code includes a  tag, but then you nest it 
within another  tag!
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Forms that call rpc instead of redirect

[Adam Chlipala]

Maybe just stop worrying about it, so that you might find that problems 
don't arise in practice? >:)


On 02/11/2018 07:13 PM, Aistis Raulinaitis wrote:
Any pointers to get me started on the right path when it comes to a 
more effective usage of source based forms?


On Feb 11, 2018 16:09, "Adam Chlipala" <ad...@csail.mit.edu 
<mailto:ad...@csail.mit.edu>> wrote:


I'm not sure what to suggest.  No, there is no existing feature
like what you suggest.  I have found it quite pleasant to work
with sources and widgets connected to them.

On 02/11/2018 05:03 PM, Aistis Raulinaitis wrote:

The way that a form will pack all of its contents into a stuct is
a clear advantage over the source based route. It requires
defining possibly many sources and wiring them all into the right
slots, having to call "get" on each one of them in the onclick
handler and then wire all the gotten values into the handler.




___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Forms that call rpc instead of redirect

[Adam Chlipala]

I'm not sure what to suggest.  No, there is no existing feature like 
what you suggest.  I have found it quite pleasant to work with sources 
and widgets connected to them.  And it is even better to use 
higher-level abstractions like in UPO <http://upo.csail.mit.edu/> 
(itself likely not applicable to your card game).


On 02/11/2018 05:03 PM, Aistis Raulinaitis wrote:
Yes I did get a little demo working with ctextbox, cchecbox, and the 
like. However the result is much more verbose and more likely to have 
runtime errors over a regular form.


The way that a form will pack all of its contents into a stuct is a 
clear advantage over the source based route. It requires defining 
possibly many sources and wiring them all into the right slots, having 
to call "get" on each one of them in the onclick handler and then wire 
all the gotten values into the handler.


Losing the form submit struct typing mechanism and the added verbosity 
of all the sources would be very painful if you are expecting the 
majority of your forms to be of this style. Which I am.


On Feb 11, 2018 13:20, "Adam Chlipala" <ad...@csail.mit.edu 
<mailto:ad...@csail.mit.edu>> wrote:


I think that kind of form has gone out of style, and I personally
almost always use the Ur/Web tags like  to collect data
and then choose RPCs programmatically.

On 02/11/2018 04:10 PM, Aistis Raulinaitis wrote:

The form mechanism is excellent, with the built in type
checking, but the submit action function returns a page: state
-> transaction page.

Is there such a thing such as a version of forms that has a
submit action function with a type of: state -> transaction unit.

This is so I can call rpc functions there in the submit action
and then the current page is updated using responses over a
channel from the server.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Forms that call rpc instead of redirect

[Adam Chlipala]

I think that kind of form has gone out of style, and I personally almost 
always use the Ur/Web tags like  to collect data and then 
choose RPCs programmatically.


On 02/11/2018 04:10 PM, Aistis Raulinaitis wrote:
The form mechanism is excellent, with the built in type checking, but 
the submit action function returns a page: state -> transaction page.


Is there such a thing such as a version of forms that has a submit 
action function with a type of: state -> transaction unit.


This is so I can call rpc functions there in the submit action and 
then the current page is updated using responses over a channel from 
the server.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Key-value store extension

[Adam Chlipala]

That's an interesting idea.  It is not a feature that has ever occurred 
to me to suggest.  I prefer to settle configuration at compile time, so 
that the compiler can specialize code to chosen settings.  Have you 
considered that path, too?


On 01/29/2018 10:43 AM, Athene Noctua wrote:

Hi all,

I find it useful to have a module for storing global configuration
settings and the likes in my applications, using a single table with
key and value fields and a simple get/set interface. Unfortunately
this approach breaks the nice encapsulation properties you get with
Ur/Web tables, as there's no way to control which module can access
which key, and trying to generate the keys to avoid collisions would
likely be cumbersome and break through multiple versions of the same
application.

I was wondering if this was a useful enough feature to be added into
the language, and if I should bother trying to hack it into the
compiler, or if I should just stick with writing a functor and make a
key-val table for each module that needs it instead.

For example:

 key test : string

 fun set_test { Test = t } =
   storeSet test t

 val main =
   t <- storeGet test;
   return 
 The value of test is {[Option.get "test" t]}.
 
   

"key" is probably not a very good name, as adding it as a keyword it
would likely break a lot of existing code, but that's easy to change.

What do you think?

- Francesco


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Set / Update values within a structure

[Adam Chlipala]

You can register a callback that, when called, reads another callback 
out of a [source] and calls it.  Is that sufficient?


On 11/10/2017 04:19 PM, Nitin Surana wrote:

Hi Adam

Thanks for responding. Is there any alternative to change the callback 
? I want to trigger a urweb function defined within `let` block upon a 
javascript event.
Since, the function is within `let` block (because it needs access to 
certain variables within the parent function), I'm unable to use 
execF(...) from javascript.


Also, is `ref` not supported in urweb ?

Thanks

On Fri, Nov 10, 2017 at 4:48 AM, Adam Chlipala <ad...@csail.mit.edu 
<mailto:ad...@csail.mit.edu>> wrote:


On 11/09/2017 10:42 PM, Harshita Kasera wrote:

What I ultimately want to achieve is to be able to change the
callback function /debugMe/ at a later point of time. Is it
possible to set or update values within a structure at a later
point of time?


No, module (structure) fields can't be modified at runtime in
Ur/Web or ML.  Therefore, the module system is not the right tool
for runtime rewriting of callbacks.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Research topic one semester Ur/Wev or dependent typer

[Adam Chlipala]

Actually, one other idea that just came up on GitHub is adding a 
WebAssembly backend to the Ur/Web compiler.  This task requires SML 
expertise but is probably small enough for someone starting with that 
expertise.


On 11/10/2017 07:50 AM, Adam Chlipala wrote:
Glad to hear you're interested in these topics!  And presumably some 
other people following the mailing list might be interested in similar 
suggestions, though I suggest you take any further replies private, 
sending to me alone.


The only semester-sized idea I have at the moment is to learn about 
UPO <http://upo.csail.mit.edu/> and implement a new module or two.  I 
consider Ur/Web almost done as a research project, as it is almost 
fully transitioned into a production toolset.


On 11/10/2017 03:13 AM, Daniel Agota wrote:

Dear Adam,

Could you propose me a small scale research project either related to 
Ur/Web or the topics covered in the cpdt book?


I am doing a one semester masters level course focusing primarily on 
research methodol‎ogy, but I personally  would like to work on a 
meaningful project.


I am a Senior Developer with 9 years industrial experience currently 
working with micro services.


I have read the ‎Types and Programming Languages book from Benjamin 
Pierce and the Software Foundations book about two years ago.


Kind Regards, Daniel Agota
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Research topic one semester Ur/Wev or dependent typer

[Adam Chlipala]

Glad to hear you're interested in these topics!  And presumably some 
other people following the mailing list might be interested in similar 
suggestions, though I suggest you take any further replies private, 
sending to me alone.


The only semester-sized idea I have at the moment is to learn about UPO 
 and implement a new module or two.  I 
consider Ur/Web almost done as a research project, as it is almost fully 
transitioned into a production toolset.


On 11/10/2017 03:13 AM, Daniel Agota wrote:

Dear Adam,

Could you propose me a small scale research project either related to 
Ur/Web or the topics covered in the cpdt book?


I am doing a one semester masters level course focusing primarily on 
research methodol‎ogy, but I personally  would like to work on a 
meaningful project.


I am a Senior Developer with 9 years industrial experience currently 
working with micro services.


I have read the ‎Types and Programming Languages book from Benjamin 
Pierce and the Software Foundations book about two years ago.


Kind Regards, Daniel Agota


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Set / Update values within a structure

[Adam Chlipala]

On 11/09/2017 10:42 PM, Harshita Kasera wrote:
What I ultimately want to achieve is to be able to change the callback 
function /debugMe/ at a later point of time. Is it possible to set or 
update values within a structure at a later point of time?


No, module (structure) fields can't be modified at runtime in Ur/Web or 
ML.  Therefore, the module system is not the right tool for runtime 
rewriting of callbacks.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] No sql_injectable(_prim) xbody (or xml in general).

[Adam Chlipala]

Actually, not all types are serializable, but you're right that XML 
currently is!  This might call for more checking in the compiler for bad 
type parameters of [serialize]/[deserialize]. Thanks for pointing it out.


On 11/03/2017 08:58 AM, Peter Brottveit Bock wrote:

I don't really see the injection problem in the case of ur/web,  since there is 
a strict separation between strings and xml. (I also just checked: it seems  
one can't send xml from the client to the server—which is good in case of 
malicious clients.)

I do see the problem with the javascript, though. Related to this, I was 
surprised to learn yesterday that all types are serializeable. Given the 
problem you just highlighted, this seems problematic!

Example code:

fun get_text () : transaction string =
 return "hello world"

fun generate_page () : transaction xbody =
 text <- source "";
 return
 
 
  {[x]} 
 }/>
  s <- rpc (get_text ()); set text s }
 />
 

table t : { Elem : serialized xbody }

fun add_page () : transaction unit =
 page <- generate_page ();
 dml(INSERT INTO t(Elem) VALUES ({[serialize page]}))

fun main () : transaction page =
 current_pages <-
 queryX (SELECT * FROM t) (fn row => deserialize row.T.Elem);
 return 
 
  rpc (add_page ())}/>
 
 {current_pages}
 
 


Running this page, clicking on "add page", and then refreshing gives an error 
in Firefox's developer console.

— Peter

On Fri, 3 Nov 2017, at 13:00, Adam Chlipala wrote:

On 11/02/2017 11:19 PM, Artyom Shalkhakov wrote:

2017-11-03 1:59 GMT+06:00 Peter Brottveit Bock <p...@peterbb.net
<mailto:p...@peterbb.net>>:

 It seems to me that it's not possible to store xml in a database.
 Is there any reason for this?


Storing it in a database is prone to XML/HTML injection (therefore the
general case is disallowed).

Right, that's true.  However, it shouldn't be a concern when only your
Ur/Web app accesses that database.

Still, overnight I thought of another issue: legitimate JavaScript code
within HTML fragments can become illegitimate across versions of your
Ur/Web app!  A global identifier may no longer exist, causing an
unbound-identifier exception when using HTML retrieved from the
database.  To me, this is the kiss of death, reminding me why this
feature deserves to be left out.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur record types as sets of fields

[Adam Chlipala]

On 11/03/2017 08:22 AM, Anthony Clayden wrote:

On 4/11/2017, at 12:57 AM, Adam Chlipala <ad...@csail.mit.edu> wrote:


On 11/02/2017 09:51 PM, Anthony Clayden wrote:
I'm curious what the full signature would look like. Here's my guess:

 fun natJoin [ t1' :: {Type} ] [ t1_2 :: {Type} ] [ t2' :: {Type} ]
 [ t1' ~ t1_2 ] [ t1' ~ t2' ] [ t1_2 ~ t2' ]
 ( t1 : $( t1' ++ t1_2 ) )  ( t2 : $( t1_2 ++ t2' ) )
 = ??

One possibility is:
 t1 ++ (t2 --- t1_2)

IIUC that's merely projecting away the t1_2 attributes from t2; then 
cross-multiplying with t1(?) What it needs is matching records type t1 with 
records type t2 that have the same values in the fields in common -- i.e. in 
their t1_2 fields. That's typically implemented as a record-by-record fold over 
one argument.


It's not clear to me what result type you expect, though.


Oh, that was in the earlier message: [ t1' ++ t1_2 ++ t2' ]


Oh, you meant the brackets to signify a list, Haskell-style?  But then 
the argument types don't make sense, as they only give single records, 
not lists or sets of records.


In real Ur/Web code, such a function would be a bad smell, since SQL 
queries do all this natively.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] No sql_injectable(_prim) xbody (or xml in general).

[Adam Chlipala]

On 11/02/2017 11:19 PM, Artyom Shalkhakov wrote:
2017-11-03 1:59 GMT+06:00 Peter Brottveit Bock >:


It seems to me that it's not possible to store xml in a database.
Is there any reason for this?


Storing it in a database is prone to XML/HTML injection (therefore the 
general case is disallowed).


Right, that's true.  However, it shouldn't be a concern when only your 
Ur/Web app accesses that database.


Still, overnight I thought of another issue: legitimate JavaScript code 
within HTML fragments can become illegitimate across versions of your 
Ur/Web app!  A global identifier may no longer exist, causing an 
unbound-identifier exception when using HTML retrieved from the 
database.  To me, this is the kiss of death, reminding me why this 
feature deserves to be left out.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur record types as sets of fields

[Adam Chlipala]

On 11/02/2017 09:51 PM, Anthony Clayden wrote:

I'm curious what the full signature would look like. Here's my guess:

 fun natJoin [ t1' :: {Type} ] [ t1_2 :: {Type} ] [ t2' :: {Type} ]
 [ t1' ~ t1_2 ] [ t1' ~ t2' ] [ t1_2 ~ t2' ]
 ( t1 : $( t1' ++ t1_2 ) )  ( t2 : $( t1_2 ++ t2' ) )
 = ??


One possibility is:
    t1 ++ (t2 --- t1_2)
It's not clear to me what result type you expect, though.


And how would I invoke it? With those three `~` constraints, does that need

 natJoin ! ! ! r1 r2

And can Ur figure out the rest?


Disjointness proofs are implicit by default, so just
    natJoin r1 r2


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] No sql_injectable(_prim) xbody (or xml in general).

[Adam Chlipala]

You're right that there are currently no type-class instances for 
storing XML in the SQL database.  At the moment, I can't remember any 
good reasons for not adding an instance for all [xml] types. I'll plan 
to do it, if no one adds a counterargument here in the next few days!


On 11/02/2017 03:59 PM, Peter Brottveit Bock wrote:

Hi,

It seems to me that it's not possible to store xml in a database. Is there any 
reason for this?

My understanding of ur/web is that the xml data type is—under the hood—simply a 
string. I therefore would have thought it would be trivial to store it in a 
database.

As a minimal example:

--
table db : { Elem : xbody }

fun display_db () =
 queryX (SELECT * FROM db)
(fn row => row.Db.Elem)

fun add_to_db (x : xbody) : transaction unit =
 dml (INSERT INTO db(Elem) VALUES ({[x]}))

fun main () =
 add_to_db  Hello ;
 display_db ()
--

fails with
--
example.ur:5:38: (to 5:43) Can't resolve type class instance
Class constraint:
sql_injectable (xml ([Dyn = (), MakeForm = (), Body = ()]) ([]) ([]))
Reduced to unresolvable:
sql_injectable_prim
  (xml ([Dyn = (), MakeForm = (), Body = ()]) ([]) ([]))
--

— Peter


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur record types as sets of fields

[Adam Chlipala]

On 11/01/2017 08:26 PM, Anthony Clayden wrote:
I'm wondering whether Ur's disjointness constraint might be used to 
build a record merge operator -- as needed for Relational Algebra 
Natural Join.


Given two records of type t1, t2 with (some) fields in common, some 
private; let's chop their fields into projections:

t1' -- fields private to t1
t1_2 -- fields in common
t2' -- fields private to t2

Then we can say (treating `++` as union of fields):
t1 is [ t1' ++ t1_2 ];
t2 is [ t1_2 ++ t2' ];
the result of Natural Join is [ t1' ++ t1_2 ++ t2' ].

We also require those projections to be disjoint:
[ t1' ~ t1_2 ], [ t1' ~ t2' ], [ t1_2 ~ t2' ]

Those constraints uniquely 'fix' all those record types modulo 
ordering of names/fields in the records. Is that going to work?


Short answer: yes, it works!  And I don't think a long answer is needed.

It also feels weird using `++` for record union: again it strongly 
suggests Haskell's list concatenation, which is non-commutative. 
Perhaps Ur's `++` is non-commutative(?) It's the inbuilt semantics for 
`$( )`, `!` that make `++` commutative in effect(?)


Yes, Ur/Web [++] is commutative.  I'm not sure what constitutes an 
"explanation of why," but yours seems reasonable.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] RPC call line throwing error

[Adam Chlipala]

I like Benjamin's solution.  To me, it clearly leads to better code, 
even independently of this issue.  I always try to avoid querying SQL 
row data that won't be used.


The problem has to do with embedding of server-side values in 
client-side code.  The type [client] should only appear in server-side 
code, so it's proper for the compiler to signal an error when 
[client]-containing variable [row] is mentioned in a GUI event handler.  
The error message arises because this faulty embedding prevents the 
compiler from translating code to JavaScript, and therefore the code to 
get the mouse-event info remains in server-side code, which isn't 
allowed, because only client code can call that function.


Clearly not a nice error message, but I don't plan to fix it, per se.  I 
have longer-term plans to reimplement Ur/Web or a similar system in a 
nicer way that avoids the problem with static typing.


On 10/25/2017 10:33 PM, Benjamin Barenblat wrote:

On Tue, Oct 24, 2017 at 7:56 PM, Nitin Surana  wrote:

I'll really appreciate if someone can help us. It shouldn't take more
than a few minutes - https://github.com/urweb/urweb/issues/94

This took a bit more than a few minutes, and I'm still not entirely sure
what's going on, but I eventually figured out how to fix your particular
problem. I ran the compiler with the `-explainEmbed` flag, which gives
more information about errors like this, and got

 Can't embed
 loc:  peers.ur:20:20-21:3
   e:  UNBOUND_1.Peers.A
   t:  FFI(Basis.client)
 peers.ur:20:20: (to 21:3) Server-side code uses client-side-only identifier 
"Basis.mouseEvent"

So I tried changing your `onclick` handler to avoid capturing
`row.Peers.A` - i.e., I changed your `SELECT` statement to

 SELECT Peers.C FROM peers WHERE peers.A > {[me]} OR peers.A < {[me]}

and it compiled.

This is definitely a case of a bad error message, but there may be more
in play here. It sounds like the compiler is trying to evaluate the body
of the `onclick` handler on the server instead of on the client, which
seems wrong to me. This may also be related to Ur/Web's apparent
inability to handle client IDs on the client side [1]. In any case,
though, if anybody else has experienced issues like this, please speak
up.

As an unrelated aside, you can simplify your `SELECT` statement further
- Ur uses `<>` as the inequality operator, so you can say

 SELECT Peers.C FROM peers WHERE peers.A <> {[me]}

with the same semantics.

Best,
Benjamin


[1] https://github.com/urweb/urweb/issues/96

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Arrays and maps?

[Adam Chlipala]

On 07/25/2017 11:48 AM, Artyom Shalkhakov wrote:
Well, arrays may be overused and such, but here in this particular 
instance:

https://github.com/ashalkhakov/urweb-projects/blob/master/sam/app.ur#L238

The update requires rebuilding the whole list, seems quite wasteful
for this particular usage.

Is this algorithmic inefficiency not something to be concerned about?


I don't know.  Do you notice any performance issues with your 
application under realistic workloads?


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Improving JS VM (was: Re: Arrays and maps?)

[Adam Chlipala]

On 07/24/2017 11:08 PM, Artyom Shalkhakov wrote:

2017-07-25 1:46 GMT+06:00 Aistis Raulinaitis :

I agree, I think arrays are much overused in programming for the most part.
My thoughts on are that these libs should facilitate easier interop with the
existing JS libs rather than as a bedrock for a data structure on the
frontend. On the other hand, I like the idea of a finger tree
implementation. My only question is, since we have the choice, would it be
more appropriate to implement it using modules or type classes? My Haskell
background makes me lean in one direction, but I think it would be
interesting to have both. That being said, I should have the js array
library out in the next day or two. Mind you both of these libs in their
forEach functions call execF twice. So you are invoking the Ur/Web runtime
twice for each element. This shouldn't be too bad depending on the
calculation, but it's something to keep in mind.


Speaking of which, how is the VM implemented and are there any
low-hanging fruits to improve it?


That is a tough question to give a short answer to!  However, you can 
find the whole implementation within urweb/lib/js/urweb.js.  The whole 
runtime system is there, but the file is an upper bound on VM 
complexity.  It's under 2000 lines of code.


I haven't heard anyone complain about performance of client-side Ur/Web 
code in years, as far as I can remember, so it's not clear there are any 
high-priority issues on that front.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Arrays and maps?

[Adam Chlipala]

Yes, it's possible in principle to add such things to the standard 
library.  However, the rarity with which such a feature is requested 
provides evidence that it's not important enough to build in!  Benjamin 
Barenblat's suggestions of functional data structures seem good; most 
applications will be fine using those.


Do you have a particular application in mind?

In general, I think arrays are dramatically overused in programming.  
They're really a rather poor fit for almost all problems, in terms of 
programming elegance.  Finite maps are more justifiable, but I would 
claim SQL subsumes them, for computations happening on the server.


On 07/22/2017 11:59 AM, Artyom Shalkhakov wrote:

Hello all,

Is it possible to extend Ur/Web with arrays and maps? It would be
really useful, I guess.

For the time being, Aistis put together a JS-only solution:

https://github.com/sheganinans/js_map

The downside is that this solution exploits some implementation
details of the Ur/Web JS virtual machine (e.g. the fact that all Ur
functions are in a curried form).




___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Anything to squeeze in before a new Ur/Web release?

[Adam Chlipala]

On 07/13/2017 02:55 AM, Artyom Shalkhakov wrote:
Here's a list of stuff I'd like to see, in no particular order: 


Thanks for the suggestions.  They mostly sound like enhancement ideas, 
which I probably won't tackle soon, though I'd be glad to consider 
patches for any of them.



* query string parsing support (there isn't even an example on how to do it...
   would come in handy if one were to use Ur/Web to implement a "microservice")


I believe there is already documentation on how to obtain query strings, 
at which point string parsing is just like usual (and pretty 
straightforward), with no special library support.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

[Ur] Anything to squeeze in before a new Ur/Web release?

[Adam Chlipala]

I'd like to make a new release early next week.  I just cleared the 
backlog of bug reports and merge-ready PRs, I think.  Are there any 
other changes appropriate to make before a release?


P.S.: Ur/Web is now included in Debian stable!  Thanks to Benjamin 
Barenblat for maintaining the package.



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] About clientOnly

[Adam Chlipala]

Yes, JavaScript functions are not valid as functions within Ur/Web's 
runtime representations.  The details are intentionally undocumented, 
but perhaps I should add more of a disclaimer not to rely on the 
details.  (I hope I've understood your issue report well enough to 
isolate the problem.)


On 05/22/2017 01:53 PM, Aistis Raulinaitis wrote:
Ah, so is this now why I'm getting this error?: TypeError: fr.f is not 
a function


Here's some screenshots of the code in the inspector: 
http://imgur.com/a/FBm3R


The code in question looks like this:

function new_map_with (init) {
var acc = new Map ();
var curr = init;
while (curr._2 != null) {
acc.set (curr._1._1, curr._1._2);
curr = curr._2;}
//curr._1._1 contains the last elem when curr._1._2 === null.
acc.set (curr._1._1, curr._1._2);
return acc;}

I am attempting to pass back the Map from JS back to Ur, and it seems 
that fr.f at runtime will hold new_map_with at first, then after it 
executes it then holds the Map I generates. At that point line 1991 
gets called e = {c: "c", v: fr.f(v)}; and I get that error, since fr.f 
now holds Map {...} and Map isn't a function..


On Mon, May 22, 2017 at 4:42 AM, Adam Chlipala <ad...@csail.mit.edu 
<mailto:ad...@csail.mit.edu>> wrote:


I can confirm that non-primitive/abstract types are not meant to
cross the FFI boundary.


On 05/21/2017 11:31 PM, Aistis Raulinaitis wrote:

Thanks!

On Sun, May 21, 2017 at 8:27 PM, Artyom Shalkhakov
<artyom.shalkha...@gmail.com
<mailto:artyom.shalkha...@gmail.com>> wrote:

2017-05-22 9:19 GMT+06:00 Aistis Raulinaitis
<sheganin...@gmail.com <mailto:sheganin...@gmail.com>>:
> Hmm, that makes sense. Do you have an example of FFI with
an abstract type?
> I tried to encapsulate the map type with a con, but
obviously that does not
> work..
>

Sure, here are two examples:

https://github.com/bbarenblat/urweb-regex
<https://github.com/bbarenblat/urweb-regex> (in particular,
take a look
at regex__FFI.urs and the two types [substring_t] and
[substring_list_t])
https://github.com/ashalkhakov/urweb-storage
<https://github.com/ashalkhakov/urweb-storage> (shameless
plug; in
particular, take a look at storage__FFI.urs and the type
[storage])

> On Sun, May 21, 2017 at 8:10 PM, Artyom Shalkhakov
> <artyom.shalkha...@gmail.com
<mailto:artyom.shalkha...@gmail.com>> wrote:
>>
>> 2017-05-22 6:22 GMT+06:00 Aistis Raulinaitis
<sheganin...@gmail.com <mailto:sheganin...@gmail.com>>:
>> > So I am working with the JS FFI, however it seems that
the clientOnly
>> > directive is being ignored.
>> >
>> > Here is the example code:
>> >
>> > ~~~
>> > main.urp:
>> > ~~~
>> >
>> > ffi js_map
>> > jsFunc Js_map.new_map=new_map
>> > jsFunc Js_map.new_map_with=new_map_with
>> > clientOnly Js_map.new_map
>> > clientOnly Js_map.new_map_with
>> > benignEffectful Js_map.new_map
>> > benignEffectful Js_map.new_map_with
>> > jsFile js_map.js
>> >
>> > main
>> >
>> >
>> > ~~~
>> > main.urs:
>> > ~~~
>> >
>> > val main : unit -> transaction page
>> >
>> >
>> > ~~~
>> > main.ur:
>> > ~~~
>> >
>> > fun main () =
>> > c <- Js_map.new_map_with ((1, 2)::[]);
>> > return 
>> >
>> >
>> > ~~~
>> > js_map.urs:
>> > ~~~
>> >
>> > con js_map :: Type -> Type -> Type
>> >
>> > val new_map  : k ::: Type -> v ::: Type -> unit ->
transaction
>> > (js_map k
>> > v)
>> > val new_map_with : k ::: Type -> v ::: Type -> list (k *
v) ->
>> > transaction
>> > (js_map k v)
>> >
>> >
>> > ~~~
>> > js_map.js:
>> > ~~~
>> >
>> > function new_map () {return new Map ();}
>> >
>> > function new_map_with (arg) {return new Map (arg); }
&g

Re: [Ur] Generating fresh name (gensym :: {Unit} -> Name).

[Adam Chlipala]

On 07/09/2017 05:11 PM, Peter Brottveit Bock wrote:

Is it possible to generate a fresh name relative to some collection of names? I.e. something 
of kind "gensym :: {Unit} -> Name".


Short answer: I can't think of any way to implement that feature, with 
Ur as it stands today.



  Does it break some nice meta-properties of Ur/Web?


It seems consistent with the model of Ur in Coq, though the 
representation of rows might need to be extended to allow iteration even 
without a folder (to find a fresh name).



I have two possible types which can be used to represent this:

val lolli_right :
 t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} ->
 (n :: Name -> [[n] ~ gamma] => lin (gamma ++ [n = t0]) t1) ->
 lin gamma (lolli t0 t1)

and

val lolli_right' :
 n ::: Name -> t0 ::: Type -> t1 ::: Type -> gamma ::: {Type} ->
 [[n] ~ gamma] =>
 lin (gamma ++ [n = t0]) t1 ->
 lin gamma (lolli t0 t1)

The first type is arguably nicer, since when used as a proof term, it actually binds the 
name "n" locally. The second
version works, but it's not a binder proper, so it "pushes" the problem of 
finding a suitable name further out. Said another way, the first version is modular while 
the second is not.

While it is straight forward to implement the second version, I can not 
immediately see a way to implement the first one, without a way to generate a 
fresh name.


Well, you could combine the two: take in a polymorphic premise, but also 
ask for a concrete disjoint name to be passed at the top level. The 
implementation can instantiate the premise with the concrete name.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] need help with unification and field name disjointness proof failures

[Adam Chlipala]

On 04/08/2017 04:05 PM, Adam Chlipala wrote:

On 04/06/2017 06:22 PM, Benjamin Barenblat wrote:

The fact that `rand` returns -1 on failure, however, is a bit scary.
That sounds like a CVE waiting to happen – people aren’t going to
check the result code from `rand`. Adam, how would you feel about it
returning an `option` or throwing an application error if it fails?


Raising an error seems like a reasonable idea.  It could signal to 
snooping parties that we ran out of entropy, but I hope that isn't 
such a serious leak.  Any other strong opinions from people watching 
the list? 


OK, absent other opinions, I implemented raising an error.

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] expressing non-emptiness?

[Adam Chlipala]

No such more refined type of strings is built into Ur/Web, any more than 
it's built into OCaml or Haskell.


On 05/10/2017 06:25 PM, Marko Schuetz-Schmuck wrote:

I'm puzzled over expressing non-emptiness.

Say, I want to write a function that has a non-empty string
parameter. How would one express this additional property as some form
of constraint? Just to be clear, I'm not looking at implementing a new
type of non-empty strings in parallel to the already existing strings.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] race condition in urweb-email

[Adam Chlipala]

Oh, I see why that is happening.  It's definitely a bug.  Thanks for the 
report, and consider it pushed onto my to-do list.


On 05/02/2017 02:01 PM, Marko Schütz Schmuck wrote:

I'm seeing a race condition using urweb-email.

An example is attached below.

On the console I see the three TO: addresses reported by Mail.to and
then the three mails are sent with the last of the three addresses.

Should Mail.from, Mail.subject and friends yield transaction header?

Best regards,

Marko


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] EUnurlify in code to be compiled to JavaScript[2]?

[Adam Chlipala]

On 05/01/2017 09:42 AM, Benjamin Barenblat wrote:

On Sun, Apr 30, 2017 at 1:19 PM, Adam Chlipala <ad...@csail.mit.edu> wrote:

Ur/Web doesn't support any interaction with cookies in client-side
code.

Is this because Ur/Web signs all its cookies and doing the signing and
verification on the client side is a security problem?


No, it's because said feature didn't seem necessary to implement so far 
(you can always hoist the cookie reads into the server-side code, 
referring to their variables in client code), /and/ the implementation 
strategy for deserializing cookie values so far happens to use 
server-side-specific code (direct generation of rather imperative C in 
the Ur/Web compiler), so it's not a quick job to extend to client code.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] EUnurlify in code to be compiled to JavaScript[2]?

[Adam Chlipala]

Ah, that one's easy for me to spot.  Ur/Web doesn't support any 
interaction with cookies in client-side code.


On 04/21/2017 07:38 PM, Marko Schütz Schmuck wrote:


cookie auth : string
fun startSession (email : string) : transaction unit
   = setCookie auth {Value = email,
 Expires = None,
 Secure = False}

fun main () : transaction page
   = loggedIn <- source (None : option string);
 scUser <- source "";
 return 
   
   
 vu <- get scUser;
 rpc (startSession vu);
 c <- getCookie auth;
 case c of
 None => set loggedIn None
   | Some _ => set loggedIn (Some vu)}/>
   



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] fastCGI backend and POST /.msgs HTTP/1.1 requests

[Adam Chlipala]

I don't think I'm going to be able to look into this problem any time 
soon, but I'll be happy to accept a patch, if someone finds one.


On 04/14/2017 06:46 PM, Sergey Mironov wrote:

Yes, I am able to reproduce the error with the latest Ur/Web. I've
checked the related code and didn't find any obvious errors. But, if I
replace the following assignment
   o->r.requestIdB0 = current_request_id & 0x00ff;
with the assignment to 1, the error disappears.

Very strange.

Regards,
Sergey


2017-04-14 18:28 GMT+03:00 Benjamin Barenblat :

On Thu, Apr 13, 2017 at 6:35 PM, Sergey Mironov  wrote:

I am facing a problem running the application compiled in FastCGI mode
with nginx. The error on server says

2017/04/14 01:19:13 [error] 11847#0: *2 upstream sent unexpected
FastCGI request id low byte: 0 while reading response header from
upstream, client: 127.0.0.1, server: , request: "POST /.msgs
HTTP/1.1", upstream: "fastcgi://127.0.0.1:9000", host:
"127.0.0.1:8081", referrer: "http://127.0.0.1:8081/App/convertFile/48;

That sounds suspiciously like
. Are you running the latest
version of Ur/Web?


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] [Ur/Web Ffi: JavaScript]

[Adam Chlipala]

On 04/24/2017 11:54 PM, Jeevjyot Chhabda wrote:

I am developing an application in Ur/Web which requires good amount of 
javascript code. I would like to warn/ throw an error during the compile time 
when the user doesn’t set the right configuration in javascript? Is it possible 
to throw compile time error through javascript code?
I would like to take the benefit of the compilation of the web app.


Short answer: no, it is not possible to do any kind of compile-time 
analysis of JavaScript code.  That is, Ur/Web provides no tools for 
static analysis of JavaScript.


I also encourage you to reconsider using "a good amount of JavaScript 
code" in any Ur/Web application, especially when you're writing that 
code instead of importing a popular library.  It usually isn't the best 
way to accomplish the overall goal of a project.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur on gitlab pages

[Adam Chlipala]

On 04/16/2017 11:10 PM, Artyom Shalkhakov wrote:

* [wget] is used to scrape the pages and save them to a file (using
-static protocol, I could not get the dynamic JS file output)


I hadn't thought of that case, so it sounds like a good new feature to 
request: outputting JavaScript code in '-static' mode.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur/Web people organizer: editable table with fixed (hidden) field?

[Adam Chlipala]

If the "user" field is not editable, how do you choose which user to 
associate with a new row?


On 04/11/2017 12:10 PM, Marko Schütz Schmuck wrote:

On Tue, 11 Apr 2017 10:58:31 -0400,
Adam Chlipala wrote:

OK, so you don't want to support adding or deleting rows, just editing the ones 
that
already exist?  I'm not sure UPO has something like that right now, but I'd 
need to look
through the code again to be sure.

No, no: adding and deleting are required too. It's just that I want to
have the User field not editable. A "sink widget" that does not
display but can be assigned as the widget of a field might work? The
field would still be in the records and be stored in the table.

Best regards,

Marko


On 04/10/2017 04:14 PM, Marko Schütz Schmuck wrote:

I was wondering whether the tools available in UPO are already
sufficient to cover the following:

I have a table where each user can register several tuples. For now,
I'd like to present it as an editable table where the field User is
not editable (not even visible) and will be constants for all tuples
entered by that user.

Best regards,

Marko

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] need help with unification and field name disjointness proof failures

[Adam Chlipala]

On 04/06/2017 06:22 PM, Benjamin Barenblat wrote:

The fact that `rand` returns -1 on failure, however, is a bit scary.
That sounds like a CVE waiting to happen – people aren’t going to
check the result code from `rand`. Adam, how would you feel about it
returning an `option` or throwing an application error if it fails?


Raising an error seems like a reasonable idea.  It could signal to 
snooping parties that we ran out of entropy, but I hope that isn't such 
a serious leak.  Any other strong opinions from people watching the list?


BTW, Ur/Web is also already using cryptographic hashing internally, for 
CSRF cookie signatures, so perhaps it also makes sense to expose 
functionality of your other library by default.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Big drop in Ur performance in latest web framework benchmark

[Adam Chlipala]

On 04/01/2017 05:22 PM, Andy wrote:
Prelim results for the latest web framework benchmark is out 
(https://www.techempower.com/benchmarks/previews/round14/) and the 
performances of Ur suffer pretty some big drops in a few tests 
(Fortune Single Query, Multiple Query - but improved significantly in 
Data Updates). Any idea what causes that?


The number of cores per machine has changed, and my best guess is that 
the Ur/Web benchmark's solution hasn't been tweaked properly to set its 
number of threads as a function of the number of cores. (Now there are 
quite different core counts across the three machines in the study, 
while the counts used to match.)
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur