[Ur] A few questions about Ur/Web

[Artyom Shalkhakov]

Hello Andy,

Sorry for the late reply. Your message got into my spam folder for
some reason...

2014-07-21 22:15 GMT+06:00 Andy <angelflow at yahoo.com>:
> Hi,
>
> New to Ur/Web. This looks like a very interesting project. Would love to try
> it out. Have a few questions:
>
> 1) The FAQ states "From the world of dependent types, Ur/Web takes
> type-level computation." Does that mean Ur/Web have full support for
> dependent type? If not, what is missing? Anything that the type system of
> ATS or Agda can do that the type system of Ur/Web can't, or vice versa?
>

ATS doesn't support type level computation in the same way that Ur/Web
does. ATS doesn't support row polymorphism, it's kind-level language
is simply-typed, in contrast to Ur/Web's.

For instance, in Ur/Web one might implement a function that takes any
record (where every field is typed differently) and produces another
record such that:

1. the resulting record has all the same fields as the source record
2. where type of a field L in source record is T, the type of a field
in resulting record would be option(T), i.e. optional value

So for instance, such a function would turn a record of type {A:int,
B:string} into a record of type  {A:option(int), B:option(string)}.

This is certainly not possible to do in ATS2 currently. Even if you
encoded the necessary predicates using ATS type system, it would be
quite burdensome to handle record disjointness proofs manually. ATS
certainly isn't designed with row polymorphism in mind.

I don't know about Agda enough to say for sure, but it seems that
programming style employed in Ur/Web would be impractical in Agda too.

In Ur/Web it isn't quite possible to guarantee e.g. safe array
subscription: by this I mean an array subscription operation A[i],
such that the type system guarantees at compile-time that i >= 0 and i
< length(A), where A is an array. This is something that ATS is better
suited to handle. Well, I think it might be possible to do in Ur/Web
(probably by emulating singleton types in some way?), the point being
that Ur/Web isn't designed with this in mind.

Hopefully you'll find the above useful. :-)

> 2) Looking at the Techempower benchmark, for the "Multiple Queries" and
> "Fortune" tests, the performances of Ur/Web-Postgresql are several times
> higher than that of Ur/Web-MySQL. This is really strange because for almost
> all other frameworks the exact opposite is true: MySQL results tend to be
> much higher than postgresql results. Is this due to some problems with the
> urweb mysql driver? Any workaround? All my data is on MySQL so the poor
> performance on Mysql is a concern.
>
> 3) For the "Data Updates" benchmark Ur/Web has poor performances with high
> latencies. The FAQ attributes this to "optimistic SQL concurrency thrashing
> to provide the transactional semantics that most benchmark entrants don't
> bother to shoot for." Can you get into more details about this concurrency
> thrashing and why does it cause poor update performance? Is there anyway to
> turn this off and just use the "normal" semantics that other frameworks use?
> My application is write-heavy and latencies measured in seconds are just too
> high.
>
> 4) How big is the size of the javascript code generated by Ur/Web compared
> to hand written JS code? For example Dart-generated js tend to be several
> times bigger than the comparable hand written one. Is Ur/Web similar to
> that?
>
> Thank you.
> Andy
>
>
> _______________________________________________
> Ur mailing list
> Ur at impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>



-- 
Cheers,
Artyom Shalkhakov