Re: [Caml-list] Issues with Sexplib (#1)

["Markus Mottl" <markus.mottl@gmail.com>]

On Sat, Nov 29, 2008 at 11:40 AM, Dario Teixeira
<darioteixeira@yahoo.com> wrote:
> So far so good; now consider the code below, which serialises and then
> unserialises a value of type Foobar.t.  Note how a "complex" structure
> can be unserialised as "basic" without any consequences.  Therefore, the
> (de)serialisation process can be used to circumvent the restrictions imposed
> by the phantom type.
[snip]
> I understand that phantom types have only a compile-time significance,
> with no runtime expression at all (hence their name).  Therefore, it's not
> altogether surprising that the S-expression builder would simply ignore them.
> Still, is there a way to make them explicit in the serialised data, such
> that the unserialiser would cause a runtime error in the above example?
> Note that the serialiser is already passed sexp_of_complex_t though it
> doesn't seem to put it into any actual use.

This is not just a matter of phantom types.  Even ordinary abstract
types suffer from this if there are constraints on what constitutes a
well-formed value, i.e. not every concrete representation conforms to
a valid value.  E.g. if some abstract type t represents a sorted list
and the internal representation is just a list, somebody could pass
you an S-expression corresponding to an unsorted list.

The only way around this problem is to have functions that check at
runtime whether some value of the internal, concrete type corresponds
to a valid abstract type.  Once you have implemented such a function
(e.g. "check_sorted", etc.), you can always easily wrap the converter
for reading from S-expressions to call this test right after
deserializing.

If possible, the best way to handle such situations is to come up with
extensional representations that syntactically only allow construction
of legal values.  Then you do not need to add extra checks.  But note
that it is not always easy to find such an extensional representation.
 Sometimes the representation might also become unwieldy, and there
may not even be such an extensional representation for theoretical
reasons.  E.g. think of encoding exactly all terminating programs
extensionally, which would be very nice but is clearly impossible.

Regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com