[Ur] typechecker rejects form handler

[Adam Chlipala]

On 01/07/2014 12:54 PM, Sergey wrote:
> On 05.01.2014 22:37, Adam Chlipala wrote:
>> 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.

You're right.  I shouldn't have brought local functions into the 
picture.  What actually matters is which functions, local or global, are 
specialized to different argument lists, while also needing URLs assigned.

>>> 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 suggest passing URLs instead of functions for this case, avoiding any 
need for functors.

> 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.

You can get around this issue by using type [string] instead of [url].  
Use [show] to convert [url] to [string], then use [bless] to convert 
back.  I've done this before for various sites.  You can even use 
[Basis.currentUrl] to get the current URL, without forcing each caller 
of the redirecting function to construct the URL explicitly.

Note that this is _not_ a case of unjustifiable draconian behavior by 
the compiler, since [bless] will do run-time checking that URLs follow 
the policy you've configured in .urp files.