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.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
