[Ur] How to serialize/deserialize data structures?

[Adam Chlipala]

Artyom Shalkhakov wrote:
> Hello,
>
> Looking through basis.urs in the latest stable version, one finds:
>
>    
>> con serialized :: Type ->  Type
>> val serialize : t ::: Type ->  t ->  serialized t
>> val deserialize : t ::: Type ->  serialized t ->  t
>> val sql_serialized : t ::: Type ->  sql_injectable_prim (serialized t)
>>      
> The question are
> - what are type families
> - how to use sql_serialized
>
> Having played a bit with type families of Haskell, I tend to think
> that they are type-level functions, defined by induction on the
> structure of input types. That is, a type family is defined by
> clauses, where each clause can employ some sort of pattern matching
> over it's input types. Is this intuition correct? What are type
> families in Ur?
>    

Ur includes a copy of System F (the polymorphic lambda calculus) at the 
type level.  Type families are just type-level functions, with none of 
the incidental restrictions that are attached in Haskell.  It turns out 
you don't need to worry at all about these details to use [serialized], 
though.

Serialization is supported specially by the compiler, so it's about as 
easy to use as it could be.  You don't need to do it any differently for 
any types.  Rather, you'll get a compile-time error if you try to 
serialize a type that contains a function arrow or one of a few other 
unsupported constructs.  Beyond that, you can do the following for any 
type, with no additional code required:

type t = ...
val x : t = ...

val ser : serialized t = serialize x
val x' : t = deserialize ser

(The example isn't meant to suggest that you need to do 
[de]serialization in top-level declarations.)