Issues with Sexplib (#1)

Issues with Sexplib (#1)

[Dario Teixeira]

Hi,

I have found a couple of issues with Sexplib/Type-conv.  I am not sure they
are bugs or features, but to me they come across as unexpected, regardless.
In this message I'll report the first one;  the second follows momentarily.

Consider the Foobar module defined below.  It uses a phantom type to annotate
values of type Foobar.t, defined recursively.  The idea is that constructors
A and C are deemed "basic" while B and D are "complex".  Functions make_basic
and make_complex are used to "freeze" the structure.  Because the complex
phantom value propagates across a structure, one cannot apply make_basic to
a structure that uses any of the complex constructors.  On the other hand,
make_complex can be applied to any structure.

module Foobar:
sig
    type foobar_t =
        | A
        | B
        | C of foobar_t
        | D of foobar_t
        with sexp

    type basic_t = [ `Basic ] with sexp
    type complex_t = [ `Complex ] with sexp

    type 'a t with sexp

    val make_a: unit -> [> `Basic ] t
    val make_b: unit -> [> `Complex ] t
    val make_c: 'a t -> 'a t
    val make_d: 'a t -> [> `Complex ] t

    val make_basic: [< `Basic ] t -> [ `Basic ] t
    val make_complex: [< `Basic | `Complex ] t -> [ `Complex ] t
end =
struct
    type foobar_t =
        | A
        | B
        | C of foobar_t
        | D of foobar_t
        with sexp

    type basic_t = [ `Basic ] with sexp
    type complex_t = [`Complex ] with sexp

    type 'a t = foobar_t with sexp

    let make_a () = A
    let make_b () = B
    let make_c foobar = C foobar
    let make_d foobar = D foobar

    let make_basic x = x
    let make_complex x = x
end


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.

open Foobar

let foobar = make_complex (make_c (make_b ()))

let doc =
     let sexp = sexp_of_t sexp_of_complex_t foobar in
     let str = Sexplib.Sexp.to_string_hum sexp
     in print_endline str;
     let sexp2 = Sexplib.Sexp.of_string str in
     let doc = t_of_sexp basic_t_of_sexp sexp2
     in doc


The resulting types are:

val foobar : Document.Foobar.complex_t Document.Foobar.t    (* Complex *)
val doc : Document.Foobar.basic_t Document.Foobar.t         (* Basic *)

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.

Thanks for your time!
Best regards,
Dario Teixeira

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

[Till Varoquaux]

This is not really a bug; I'd qualify this as an "undesirable"
feature: sexplib erases type information; for instance the
representation of None* will always be the same and therefore will be
desexpable to any other option type. You may also note that some other
type have compatible representations. In practice it would be really
hard for a camlp4 extension to keep track of types. In you case you
could use custom converters and save the phantom type in the sexp.

Till

*well more or less: you could be using a custom converter or an old
version of sexplib
On Sat, Nov 29, 2008 at 11:40 AM, Dario Teixeira
<darioteixeira@yahoo.com> wrote:
> Hi,
>
> I have found a couple of issues with Sexplib/Type-conv.  I am not sure they
> are bugs or features, but to me they come across as unexpected, regardless.
> In this message I'll report the first one;  the second follows momentarily.
>
> Consider the Foobar module defined below.  It uses a phantom type to annotate
> values of type Foobar.t, defined recursively.  The idea is that constructors
> A and C are deemed "basic" while B and D are "complex".  Functions make_basic
> and make_complex are used to "freeze" the structure.  Because the complex
> phantom value propagates across a structure, one cannot apply make_basic to
> a structure that uses any of the complex constructors.  On the other hand,
> make_complex can be applied to any structure.
>
> module Foobar:
> sig
>    type foobar_t =
>        | A
>        | B
>        | C of foobar_t
>        | D of foobar_t
>        with sexp
>
>    type basic_t = [ `Basic ] with sexp
>    type complex_t = [ `Complex ] with sexp
>
>    type 'a t with sexp
>
>    val make_a: unit -> [> `Basic ] t
>    val make_b: unit -> [> `Complex ] t
>    val make_c: 'a t -> 'a t
>    val make_d: 'a t -> [> `Complex ] t
>
>    val make_basic: [< `Basic ] t -> [ `Basic ] t
>    val make_complex: [< `Basic | `Complex ] t -> [ `Complex ] t
> end =
> struct
>    type foobar_t =
>        | A
>        | B
>        | C of foobar_t
>        | D of foobar_t
>        with sexp
>
>    type basic_t = [ `Basic ] with sexp
>    type complex_t = [`Complex ] with sexp
>
>    type 'a t = foobar_t with sexp
>
>    let make_a () = A
>    let make_b () = B
>    let make_c foobar = C foobar
>    let make_d foobar = D foobar
>
>    let make_basic x = x
>    let make_complex x = x
> end
>
>
> 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.
>
> open Foobar
>
> let foobar = make_complex (make_c (make_b ()))
>
> let doc =
>     let sexp = sexp_of_t sexp_of_complex_t foobar in
>     let str = Sexplib.Sexp.to_string_hum sexp
>     in print_endline str;
>     let sexp2 = Sexplib.Sexp.of_string str in
>     let doc = t_of_sexp basic_t_of_sexp sexp2
>     in doc
>
>
> The resulting types are:
>
> val foobar : Document.Foobar.complex_t Document.Foobar.t    (* Complex *)
> val doc : Document.Foobar.basic_t Document.Foobar.t         (* Basic *)
>
> 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.
>
> Thanks for your time!
> Best regards,
> Dario Teixeira
>
>
>
>
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

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

[Dario Teixeira]

Hi,

> This is not really a bug; I'd qualify this as an "undesirable"
> feature: sexplib erases type information; for instance the
> representation of None* will always be the same and therefore
> will be desexpable to any other option type. You may also note
> that some other type have compatible representations. In
> practice it would be really hard for a camlp4 extension to keep
> track of types. In you case you could use custom converters and
> save the phantom type in the sexp.

Yes, I figured as much (see the last paragraph of my original
message).  I was just wondering if there was already a canned
solution to this sort of problem (or one in the works), before
I wrote a custom converter.

Cheers,
Dario Teixeira

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

[Markus Mottl]

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