[Ur] new user having some questions such as a:::Type twice? and more

[Adam Chlipala]

Marc Weber wrote:
>    Which is the correct type for my_length2
>    The line below "TYPE 1" show how to it for my_length
>
>    my_length2 takes two lists and sums both length. (There is no use case
>    but learning ur for this function)
>
>
>    val rec my_length
>      (* TYPE 1 *)
>      : a:::Type ->  list a ->  int
>      = fn [a:::Type] (li: list a) =>
>                      case li of
>                          [] =>  0
>                          | _ :: ls =>  1 + my_length ls
>
>    val my_length2
>      (* TYPE 2 *)
>      (*: What is the type of this function *)
>      = fn [a:::Type] [b:::Type] (li: list a, lj: list b) =>
>                        ( my_length li + my_length lj )
>    

You can trick the compiler into answering this kind of question for 
you.  Just add an obviously-wrong type annotation on the [val] 
declaration.  For instance:
     val my_length2 : int = (* code you have *)
Then the error message will tell you what type Ur/Web thinks the 
function has:

   Have con:
a ::: Type ->
  b ::: Type -> ({1 : Basis.list a, 2 : Basis.list b} -> Basis.int)
   Need con:  Basis.int

Writing this a little more nicely, using the usual shorthands:
a ::: Type -> b ::: Type -> list a * list b -> int

> 2)
>    comparing my_length above with the one by lib/ur/list.ur I think
>    my_length is much simpler. So why is lib/ur/list.ur using acc?
>    

This is an instance of a common principle for all functional languages.  
The version in the Ur/Web standard library is tail-recursive and 
requires constant auxiliary space, while your version requires auxiliary 
(stack) space linear in the list length.  You should be able to find 
some explanation online of tail recursion and its benefits.

> 3) Is there a way to comment lines in .urp files?
>    

Not at the moment.  That sounds like a reasonable feature, so feel free 
to file a Mantis feature request if you care enough.  (And feel free to 
do that in the future without asking first, too.)

> 4)
>    How would you feel about adding //, #  or-- like comments which always
>    comment everything until end of line?
>    

At the moment, it sounds like it would make the syntax more complicated 
without enough justifying benefit, but maybe others disagree.

> 5) Has anyone already thought about adding pdf support in some way -
>     probably by interfacing with C?
>    

I haven't.  It should be easy to wrap standard C libraries with the FFI, 
as you suggest.

> 6) speed:
>
>     [..snip..]
>
>      Having about 640 functions means 40sec compilation time. That's
>      close to being a coffee break.
>
>      Now I worked on a booking system (PHP) which has about 1200 PHP
>      functions which would have meant 1min 20sec. That's a very rough
>      approximation.
>    

The Ur/Web compiler does a lot more than the PHP interpreter.  The 
Ur/Web compiler also isn't specialized to type-checking Web 
applications, despite the language name.  Generality has a price, and if 
you don't use it, you'll probably see performance costs.

I'll be very surprised if your application would need anywhere close to 
1200 functions in Ur/Web.  You should be able to do much better, using 
generic functions that can take over for many of your hand-coded PHP 
functions.

I'd be interested to see what you find when you run your benchmark 
compilations with the '-timing' command-line flag.  I'm guessing the 
'elaborate' phase uses almost all the time, but, if not, that would be 
useful information.

>      Do you think splitting a larger project into pieces is enough to
>      keep compilation time short?
>    

That's not possible without extensive reimplementation of the compiler, 
which doesn't support separate compilation right now.  (The benefit you 
get from this is serious whole-program optimization.)

> 7) XHTML: does it make sense to think about encoding it differently -
>      maybe something close to WASH style?
>
>      html
>        body onclick=".."
>          script type="javascript" url="myscript.js"
>        head
>          h2 {["title"]}
>    

The XML syntax is just a convenience; it has no fundamental connection 
to the underlying XML datatypes from the Ur/Web basis library.  You can 
write your own wrappers for combinators like [cdata] and [tag], which 
you'll find in lib/ur/basis.urs.  It's unlikely that you'll be able to 
understand the types of these combinators if you don't have prior 
experience with Coq or Agda.  The Ur/Web manual defines all the 
constructs, but only in notation that most programmers aren't familiar 
with (but that are completely standard for people familiar with formal 
language semantics).

>      Even if ur will never support this - would it be possible to use
>      create a function taking a block of code (string) returning an ast
>      which would be processed by ur instead?
>    

Yes, but I'll be very impressed if anyone else but me can figure out how 
to write it. :)

This will only work with very basic HTML.  The type system isn't strong 
enough for encoding of a function whose "precondition" depends on the 
value of a string argument.

> 8) does ur have a repository you I could clone ?
>    

Thanks to Karn Kallio for answering this before.  I just want to point 
out that the earlier answer didn't draw on any privileged information; 
the front page of the Ur web site links to the Mercurial repository.