The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

I found the general idea quite interesting.
I wonder if could be possible to use serialization as an unifying
theoretical tool for finite sets and maps that can be easily be
provable (sintactically) equal.
That is, to show that a=b in coq you need syntactical equivalence or
to "import more axioms"
(sorry for my imprecise and confounding coq-terminolgy)
If (some) terms could be easily converted (back and forth) in a list
of chars/tokens that represents the syntactic definition of the term,
than lots of stuff with finite data-structure would become trivial.

May be the "right" representation of a finite collection is not the
collection of the term but the collection of their serialization?



On 9 March 2013 07:55, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> Hi all, I often found useful to have serialization in Coq.
>
> I mean to have some type data:
>
> Inductive data :=
> | Leaf : data
> | Node : data → data → data.
>
> (or another variant, just this one is cool as it allows easy product…)
>
> And for a serializable type t, two functions:
>
> serialize : t → data
> deserialize : data → t
> (or data → option t)
>
> and a proof of
> ∀ x, deserialize (serialize x) = x
> (or ∀ x, deserialize (serialize x) = Some x)
>
> This would have the following good points:
> → for any serializable data, we have decidable equality for free
> → for any serializable data, we can give a comparision function (not
> necessarily the one, you want for a special usage, but well, it can be
> handy for FSetAVL and related stuff)
> → to implement an exception mechanism (the exception type can be "data"
> and is solved dynamically with the deserialization, thus allowing to
> pass exceptions of a unknown type at definition time of the function)
> → avoid quadratic stuff in usual boolean equalities (a type with n
> constructors will require n² branches)
>
> A type class for serialization is easy to do, but automatic generation
> (in Ocaml code, like *_rec, *_rect, *_ind, *_beq) would be a real plus I
> think, although of course many terms won't be serializable.
>
> Not being a Coq source code hacker, I do not know how hard it can be,
> especially dealing with dependant types and mutual recursion. I guess,
> it could make some interesting internship for a student.