[Ur] serialized vs. sql_injectable_prim

[Adam Chlipala]

Gergely Buday wrote:
> what is the difference between serialized t and sql_injectable_prim?
> The latter is applied to those have an sql counterpart?
>
> And, serialized t seems to be an abstract type, what are the functions
> that operate on them? Should I use show and read to convert to and
> from string?
>    

I think each of these questions is answered by searching basis.urs for 
all instances of the type family in question.  The operations you find 
there are the only available operations.

[sql_injectable_prim] captures the idea of a non-[option] type that may 
be injected directly into SQL code.

[serialized] captures the idea of a (mostly) arbitrary value serialized 
into a form that may be injected into SQL code.  It is intentional that 
there is no way to convert between [serialized] and [string], as this 
would make it possible to look at the values of abstract types.  
Especially a [read] instance would make it possible to break the 
invariants of these types arbitrarily.