[Ur] typechecker rejects form handler

[Sergey]

On 05.01.2014 22:37, Adam Chlipala wrote:
> On 01/05/2014 11:00 AM, Sergey Mironov wrote:
>> If I understand correctly, it is the two specialized versions of
>> `validator' which cause problems in my example. But does this mean
>> that specializations are not usable in practice at the moment?
>
> More precisely, you'll run into trouble if you cause multiple 
> specializations of a function that defines local functions that need 
> to have URIs assigned to them!
But I've experimented with moving function `validator' to a global 
scope, like this:

fun validator (fview : int -> url) (ferr : string -> url) (i:int) 
(s:{Text:string}) : transaction page =  (* the same code *)

fun form (fview : int -> url) (ferr : string -> url) (i:int) : 
transaction xbody =
   return
     <xml>
       <form>
         <textarea{#Text}/>
         <br/>
         <submit action={validator fview ferr i}/>
       </form>
     </xml>

The error remains the same.

>> Do you plan to introduce some kind of automatic names generator for 
>> cases
>> like this one?
>
> No, I advise folks to use functors for such cases.
Functors have a weak point: looks like they don't support recursive 
declarations. Imagine the following use-case: An application has several 
different views, each view has a small login/password form in it's 
upper-right corner. Developer wants to improve the usability of this 
application by redirecting users back to the view they were at the 
moment they filled up the form. I am sure that most of the people would 
try to use a basic functional trick here:

(* Version 1 *)
fun validate_and_apply f = return {}
fun handler u f = validate_and_apply f ; redirect u
fun form (u:url) : transaction xbody = reutrn <xml><form>...<submit 
action={handler u}/></form></xml>
fun viewA (idx:int) = template ( f<- form (url (viewA idx)); return 
<xml>{f}</xml>)
fun viewB (idx:int) = template ( f<- form (url (viewB idx)); return 
<xml>{f}</xml>)
...
The "Input to exported function 'FormBug3/handler' involves one or more 
types that are disallowed for page handler inputs: Basis.url" will 
appear. This error is legitimate so people would probably try to hide 
the `u' parameter of `handler' by hiding `handler' inside `form'. I've 
moved one step further and tried to employ specializations directly:

(* Version 2 *)
fun validate_and_apply f = return {}
fun handler fu f = validate_and_apply f ; redirect (fu {})
fun form (fu:unit->url) : transaction xbody = reutrn 
<xml><form>...<submit action={handler fu}/></form></xml>
fun viewA (idx:int) = template ( f<- form (fn {} => url (viewA idx)); 
return <xml>{f}</xml>)
fun viewB (idx:int) = template ( f<- form (fn {} => url (viewB idx)); 
return <xml>{f}</xml>)
...

So the "duplicate HTTP tag" errors appeared.

Unfortunately, if I try to rewrite this code using functors, I will end 
up defining a `Form' functor taking an url to redirect users to. Now, 
this url is defined by a function that should already know how to use 
the Form functor since it calls `Form.form'! So, if only I am not 
missing something, we have a module-level recursion and thus, an 
uncovered use-case.

I have an idea of a compromise solution. I assume that every url has 
'Module/function/arg1/arg2/..' format. In order to prevent users from 
running in such a bad specializations, you may want to:

1) Forbid passing function arguments to public functions. This way 
modules will export only correct nice-looking urls. But.
AFAIK it is safe to allow binding urls to a non-public specializations 
because the compiler knows the exact number of specializations. So
2) Generate url names for private specializations

Of cause, urweb still has to make sure that there are no duplicate 
names. But this time it has all information so it is easy to this thing 
by examining the contents of a current module.
What do you think?

Regards,
Sergey