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

[Artyom Shalkhakov]

Hello Peter,

2017-11-03 1:59 GMT+06:00 Peter Brottveit Bock :

> Hi,
>
> It seems to me that it's not possible to store xml in a database. Is there
> any reason for this?
>
> My understanding of ur/web is that the xml data type is—under the
> hood—simply a string. I therefore would have thought it would be trivial to
> store it in a database.
>
>
Storing it in a database is prone to XML/HTML injection (therefore the
general case is disallowed).

If you want to store in database, then you will have to print it to a
string and then parse it back into XML/HTML (for a strictly controlled
subset of XML/HTML).

There is a library for this use-case in UPO:

https://github.com/achlipala/upo/blob/master/html.urs


> As a minimal example:
>
> --
> table db : { Elem : xbody }
>
> fun display_db () =
> queryX (SELECT * FROM db)
>(fn row => row.Db.Elem)
>
> fun add_to_db (x : xbody) : transaction unit =
> dml (INSERT INTO db(Elem) VALUES ({[x]}))
>
> fun main () =
> add_to_db  Hello ;
> display_db ()
> --
>
> fails with
> --
> example.ur:5:38: (to 5:43) Can't resolve type class instance
>Class constraint:
> sql_injectable (xml ([Dyn = (), MakeForm = (), Body = ()]) ([]) ([]))
> Reduced to unresolvable:
> sql_injectable_prim
>  (xml ([Dyn = (), MakeForm = (), Body = ()]) ([]) ([]))
> --
>
> — Peter
>
> ___
> Ur mailing list
> Ur@impredicative.com
> http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
>



-- 
Cheers,
Artyom Shalkhakov
___
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 3/11/2017, at 2:06 AM, Adam Chlipala  wrote:
> 
>> On 11/01/2017 08:26 PM, Anthony Clayden wrote:
>> I'm wondering whether Ur's disjointness constraint might be used to build a 
>> record merge operator -- as needed for Relational Algebra Natural Join.
>> 
>> Given two records of type t1, t2 with (some) fields in common, some private; 
>> let's chop their fields into projections:
>> t1' -- fields private to t1
>> t1_2 -- fields in common
>> t2' -- fields private to t2
>> 
>> Then we can say (treating `++` as union of fields):
>> t1 is [ t1' ++ t1_2 ];
>> t2 is [ t1_2 ++ t2' ];
>> the result of Natural Join is [ t1' ++ t1_2 ++ t2' ].
>> 
>> We also require those projections to be disjoint:
>> [ t1' ~ t1_2 ], [ t1' ~ t2' ], [ t1_2 ~ t2' ]
>> 
>> Those constraints uniquely 'fix' all those record types modulo ordering of 
>> names/fields in the records. Is that going to work?
> 
> Short answer: yes, it works!

Thanks Adam.

>   And I don't think a long answer is needed.
> 
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' ) )
= ??

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

natJoin ! ! ! r1 r2

And can Ur figure out the rest?



>> It also feels weird using `++` for record union: again it strongly suggests 
>> Haskell's list concatenation, which is non-commutative. Perhaps Ur's `++` is 
>> non-commutative(?) It's the inbuilt semantics for `$( )`, `!` that make `++` 
>> commutative in effect(?)
> 
> Yes, Ur/Web [++] is commutative.  I'm not sure what constitutes an 
> "explanation of why," but yours seems reasonable.
> 
> 
AntC
___
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]

You're right that there are currently no type-class instances for 
storing XML in the SQL database.  At the moment, I can't remember any 
good reasons for not adding an instance for all [xml] types. I'll plan 
to do it, if no one adds a counterargument here in the next few days!


On 11/02/2017 03:59 PM, Peter Brottveit Bock wrote:

Hi,

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

My understanding of ur/web is that the xml data type is—under the hood—simply a 
string. I therefore would have thought it would be trivial to store it in a 
database.

As a minimal example:

--
table db : { Elem : xbody }

fun display_db () =
 queryX (SELECT * FROM db)
(fn row => row.Db.Elem)

fun add_to_db (x : xbody) : transaction unit =
 dml (INSERT INTO db(Elem) VALUES ({[x]}))

fun main () =
 add_to_db  Hello ;
 display_db ()
--

fails with
--
example.ur:5:38: (to 5:43) Can't resolve type class instance
Class constraint:
sql_injectable (xml ([Dyn = (), MakeForm = (), Body = ()]) ([]) ([]))
Reduced to unresolvable:
sql_injectable_prim
  (xml ([Dyn = (), MakeForm = (), Body = ()]) ([]) ([]))
--

— Peter


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

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

[Peter Brottveit Bock]

Hi,

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

My understanding of ur/web is that the xml data type is—under the hood—simply a 
string. I therefore would have thought it would be trivial to store it in a 
database.

As a minimal example:

--
table db : { Elem : xbody }

fun display_db () =
queryX (SELECT * FROM db)
   (fn row => row.Db.Elem)

fun add_to_db (x : xbody) : transaction unit =
dml (INSERT INTO db(Elem) VALUES ({[x]}))

fun main () =
add_to_db  Hello ;
display_db ()
--

fails with
--
example.ur:5:38: (to 5:43) Can't resolve type class instance
   Class constraint: 
sql_injectable (xml ([Dyn = (), MakeForm = (), Body = ()]) ([]) ([]))
Reduced to unresolvable: 
sql_injectable_prim
 (xml ([Dyn = (), MakeForm = (), Body = ()]) ([]) ([]))
--

— Peter

___
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/01/2017 08:26 PM, Anthony Clayden wrote:
I'm wondering whether Ur's disjointness constraint might be used to 
build a record merge operator -- as needed for Relational Algebra 
Natural Join.


Given two records of type t1, t2 with (some) fields in common, some 
private; let's chop their fields into projections:

t1' -- fields private to t1
t1_2 -- fields in common
t2' -- fields private to t2

Then we can say (treating `++` as union of fields):
t1 is [ t1' ++ t1_2 ];
t2 is [ t1_2 ++ t2' ];
the result of Natural Join is [ t1' ++ t1_2 ++ t2' ].

We also require those projections to be disjoint:
[ t1' ~ t1_2 ], [ t1' ~ t2' ], [ t1_2 ~ t2' ]

Those constraints uniquely 'fix' all those record types modulo 
ordering of names/fields in the records. Is that going to work?


Short answer: yes, it works!  And I don't think a long answer is needed.

It also feels weird using `++` for record union: again it strongly 
suggests Haskell's list concatenation, which is non-commutative. 
Perhaps Ur's `++` is non-commutative(?) It's the inbuilt semantics for 
`$( )`, `!` that make `++` commutative in effect(?)


Yes, Ur/Web [++] is commutative.  I'm not sure what constitutes an 
"explanation of why," but yours seems reasonable.


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