Re: [Ur] Ur record types as sets of fields

[Adam Chlipala]

On 11/02/2017 09:51 PM, Anthony Clayden wrote:

I'm curious what the full signature would look like. Here's my guess:

 fun natJoin [ t1' :: {Type} ] [ t1_2 :: {Type} ] [ t2' :: {Type} ]
 [ t1' ~ t1_2 ] [ t1' ~ t2' ] [ t1_2 ~ t2' ]
 ( t1 : $( t1' ++ t1_2 ) )  ( t2 : $( t1_2 ++ t2' ) )
 = ??


One possibility is:
    t1 ++ (t2 --- t1_2)
It's not clear to me what result type you expect, though.


And how would I invoke it? With those three `~` constraints, does that need

 natJoin ! ! ! r1 r2

And can Ur figure out the rest?


Disjointness proofs are implicit by default, so just
    natJoin r1 r2


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] No sql_injectable(_prim) xbody (or xml in general).

[Adam Chlipala]

On 11/02/2017 11:19 PM, Artyom Shalkhakov wrote:
2017-11-03 1:59 GMT+06:00 Peter Brottveit Bock >:


It seems to me that it's not possible to store xml in a database.
Is there any reason for this?


Storing it in a database is prone to XML/HTML injection (therefore the 
general case is disallowed).


Right, that's true.  However, it shouldn't be a concern when only your 
Ur/Web app accesses that database.


Still, overnight I thought of another issue: legitimate JavaScript code 
within HTML fragments can become illegitimate across versions of your 
Ur/Web app!  A global identifier may no longer exist, causing an 
unbound-identifier exception when using HTML retrieved from the 
database.  To me, this is the kiss of death, reminding me why this 
feature deserves to be left out.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur record types as sets of fields

[Anthony Clayden]

> On 4/11/2017, at 12:57 AM, Adam Chlipala  wrote:
> 
>> On 11/02/2017 09:51 PM, Anthony Clayden wrote:
>> I'm curious what the full signature would look like. Here's my guess:
>> 
>> fun natJoin [ t1' :: {Type} ] [ t1_2 :: {Type} ] [ t2' :: {Type} ]
>> [ t1' ~ t1_2 ] [ t1' ~ t2' ] [ t1_2 ~ t2' ]
>> ( t1 : $( t1' ++ t1_2 ) )  ( t2 : $( t1_2 ++ t2' ) )
>> = ??
> 
> One possibility is:
> t1 ++ (t2 --- t1_2)

IIUC that's merely projecting away the t1_2 attributes from t2; then 
cross-multiplying with t1(?) What it needs is matching records type t1 with 
records type t2 that have the same values in the fields in common -- i.e. in 
their t1_2 fields. That's typically implemented as a record-by-record fold over 
one argument.

> It's not clear to me what result type you expect, though.
> 
Oh, that was in the earlier message: [ t1' ++ t1_2 ++ t2' ]

Perhaps that should be $( t1' ++ t1_2 ++ t2' )

What I gave was based on the `fun proj ...` definition in the 'Ur by example' 
section of your paper, which doesn't give the type of the result.


>> And how would I invoke it? With those three `~` constraints, does that need
>> 
>> natJoin ! ! ! r1 r2
>> 
>> And can Ur figure out the rest?
> 
> Disjointness proofs are implicit by default, so just
> natJoin r1 r2
> 
cool. thanks 

AntC
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] Ur record types as sets of fields

[Adam Chlipala]

On 11/03/2017 08:22 AM, Anthony Clayden wrote:

On 4/11/2017, at 12:57 AM, Adam Chlipala  wrote:


On 11/02/2017 09:51 PM, Anthony Clayden wrote:
I'm curious what the full signature would look like. Here's my guess:

 fun natJoin [ t1' :: {Type} ] [ t1_2 :: {Type} ] [ t2' :: {Type} ]
 [ t1' ~ t1_2 ] [ t1' ~ t2' ] [ t1_2 ~ t2' ]
 ( t1 : $( t1' ++ t1_2 ) )  ( t2 : $( t1_2 ++ t2' ) )
 = ??

One possibility is:
 t1 ++ (t2 --- t1_2)

IIUC that's merely projecting away the t1_2 attributes from t2; then 
cross-multiplying with t1(?) What it needs is matching records type t1 with 
records type t2 that have the same values in the fields in common -- i.e. in 
their t1_2 fields. That's typically implemented as a record-by-record fold over 
one argument.


It's not clear to me what result type you expect, though.


Oh, that was in the earlier message: [ t1' ++ t1_2 ++ t2' ]


Oh, you meant the brackets to signify a list, Haskell-style?  But then 
the argument types don't make sense, as they only give single records, 
not lists or sets of records.


In real Ur/Web code, such a function would be a bad smell, since SQL 
queries do all this natively.


___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] No sql_injectable(_prim) xbody (or xml in general).

[Peter Brottveit Bock]

I don't really see the injection problem in the case of ur/web,  since there is 
a strict separation between strings and xml. (I also just checked: it seems  
one can't send xml from the client to the server—which is good in case of 
malicious clients.)

I do see the problem with the javascript, though. Related to this, I was 
surprised to learn yesterday that all types are serializeable. Given the 
problem you just highlighted, this seems problematic!

Example code:

fun get_text () : transaction string =
return "hello world"

fun generate_page () : transaction xbody =
text <- source "";
return


 {[x]} 
}/>
 s <- rpc (get_text ()); set text s } 
/>


table t : { Elem : serialized xbody }

fun add_page () : transaction unit =
page <- generate_page ();
dml(INSERT INTO t(Elem) VALUES ({[serialize page]}))

fun main () : transaction page =
current_pages <- 
queryX (SELECT * FROM t) (fn row => deserialize row.T.Elem);
return 

 rpc (add_page ())}/>

{current_pages}




Running this page, clicking on "add page", and then refreshing gives an error 
in Firefox's developer console.

— Peter

On Fri, 3 Nov 2017, at 13:00, Adam Chlipala wrote:
> On 11/02/2017 11:19 PM, Artyom Shalkhakov wrote:
> > 2017-11-03 1:59 GMT+06:00 Peter Brottveit Bock  > >:
> >
> > It seems to me that it's not possible to store xml in a database.
> > Is there any reason for this?
> >
> >
> > Storing it in a database is prone to XML/HTML injection (therefore the 
> > general case is disallowed).
> 
> Right, that's true.  However, it shouldn't be a concern when only your 
> Ur/Web app accesses that database.
> 
> Still, overnight I thought of another issue: legitimate JavaScript code 
> within HTML fragments can become illegitimate across versions of your 
> Ur/Web app!  A global identifier may no longer exist, causing an 
> unbound-identifier exception when using HTML retrieved from the 
> database.  To me, this is the kiss of death, reminding me why this 
> feature deserves to be left out.
> ___
> Ur mailing list
> Ur@impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Re: [Ur] No sql_injectable(_prim) xbody (or xml in general).

[Adam Chlipala]

Actually, not all types are serializable, but you're right that XML 
currently is!  This might call for more checking in the compiler for bad 
type parameters of [serialize]/[deserialize]. Thanks for pointing it out.


On 11/03/2017 08:58 AM, Peter Brottveit Bock wrote:

I don't really see the injection problem in the case of ur/web,  since there is 
a strict separation between strings and xml. (I also just checked: it seems  
one can't send xml from the client to the server—which is good in case of 
malicious clients.)

I do see the problem with the javascript, though. Related to this, I was 
surprised to learn yesterday that all types are serializeable. Given the 
problem you just highlighted, this seems problematic!

Example code:

fun get_text () : transaction string =
 return "hello world"

fun generate_page () : transaction xbody =
 text <- source "";
 return
 
 
  {[x]} 
 }/>
  s <- rpc (get_text ()); set text s }
 />
 

table t : { Elem : serialized xbody }

fun add_page () : transaction unit =
 page <- generate_page ();
 dml(INSERT INTO t(Elem) VALUES ({[serialize page]}))

fun main () : transaction page =
 current_pages <-
 queryX (SELECT * FROM t) (fn row => deserialize row.T.Elem);
 return 
 
  rpc (add_page ())}/>
 
 {current_pages}
 
 


Running this page, clicking on "add page", and then refreshing gives an error 
in Firefox's developer console.

— Peter

On Fri, 3 Nov 2017, at 13:00, Adam Chlipala wrote:

On 11/02/2017 11:19 PM, Artyom Shalkhakov wrote:

2017-11-03 1:59 GMT+06:00 Peter Brottveit Bock mailto:p...@peterbb.net>>:

 It seems to me that it's not possible to store xml in a database.
 Is there any reason for this?


Storing it in a database is prone to XML/HTML injection (therefore the
general case is disallowed).

Right, that's true.  However, it shouldn't be a concern when only your
Ur/Web app accesses that database.

Still, overnight I thought of another issue: legitimate JavaScript code
within HTML fragments can become illegitimate across versions of your
Ur/Web app!  A global identifier may no longer exist, causing an
unbound-identifier exception when using HTML retrieved from the
database.  To me, this is the kiss of death, reminding me why this
feature deserves to be left out.
___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur



___
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur