From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=2.0 required=5.0 tests=AWL,DNS_FROM_RFC_POST, SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id E2E74BBAF for ; Tue, 2 Dec 2008 20:14:47 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuwAAIwXNUlKfS4fimdsb2JhbACDHY9yPgEBAQoJDAcPBbFXgQKMKwEDAQOCfA X-IronPort-AV: E=Sophos;i="4.33,703,1220220000"; d="scan'208";a="32096102" Received: from yw-out-2324.google.com ([74.125.46.31]) by mail4-smtp-sop.national.inria.fr with ESMTP; 02 Dec 2008 20:14:47 +0100 Received: by yw-out-2324.google.com with SMTP id 5so1321716ywb.3 for ; Tue, 02 Dec 2008 11:14:46 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to :subject:cc:in-reply-to:mime-version:content-type :content-transfer-encoding:content-disposition:references; bh=6HkFSylLr3F1FJvwEM5fLXZw5iupPw/8Z6i+5x1DUI0=; b=qVakdC4zfSKzvKw+4eMd5gM/Q8i+pSAj11luQvfPbRYS5kUaYXnfgVK6pr5WJx9VYW L6zEOB9L+Eo51TJQZN+vAbPRCuBar+bS3kLiXxEOtU+9+aJtERqaEIuhKP96OZe3gUBH MuhLp5qraWnFjTKTLU3vWHR8rwJrOoAbSmBAs= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=sVSHsxwFPmQKWo2FwQ2DeJMkPUO/7iTfsoFmS1iz0k5g9THekZklnJmCnGie2Da6Jx hAZncrUPa6iXj6+NXNtMneZV7QFwJk5hojqhiSKxtOs8M90heRd5qxq2KD84K/nQTNMJ McF2MFxgon0ZG7q2el7UKBtQztyTTDuZDo+EI= Received: by 10.142.103.2 with SMTP id a2mr929857wfc.164.1228245285662; Tue, 02 Dec 2008 11:14:45 -0800 (PST) Received: by 10.143.90.7 with HTTP; Tue, 2 Dec 2008 11:14:45 -0800 (PST) Message-ID: Date: Tue, 2 Dec 2008 14:14:45 -0500 From: "Markus Mottl" To: "Dario Teixeira" Subject: Re: [Caml-list] Issues with Sexplib (#1) Cc: caml-list@yquem.inria.fr In-Reply-To: <110907.37517.qm@web111509.mail.gq1.yahoo.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <110907.37517.qm@web111509.mail.gq1.yahoo.com> X-Spam: no; 0.00; markus:01 mottl:01 markus:01 mottl:01 foobar:01 compile-time:01 runtime:01 runtime:01 sexp:01 well-formed:01 corresponds:01 extensional:01 extensional:01 terminating:01 ocaml:01 On Sat, Nov 29, 2008 at 11:40 AM, Dario Teixeira 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