From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p2NNuhhu005122
	for <caml-list@sympa-roc.inria.fr>; Thu, 24 Mar 2011 00:56:43 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AlgBAG4lik3RVdK2mGdsb2JhbAClPQgUAQEBAQEICQ0HFCWITaAEjHOFDIkLAQEDBYVkBIU1hzqERYRBOoEc
X-IronPort-AV: E=Sophos;i="4.63,234,1299452400"; 
   d="scan'208";a="103376793"
Received: from mail-iy0-f182.google.com ([209.85.210.182])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 24 Mar 2011 00:56:37 +0100
Received: by iyj12 with SMTP id 12so14852932iyj.27
        for <caml-list@inria.fr>; Wed, 23 Mar 2011 16:56:36 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=domainkey-signature:sender:subject:mime-version:content-type:from
         :in-reply-to:date:cc:content-transfer-encoding:message-id:references
         :to:x-mailer;
        bh=PKMWaQv8xzhxc8ekfL4WSCYkMNvicqK9XnzOlIpMbkI=;
        b=JxzbdlKtoP783ROLOqBbIP6BTpAurmvla6BwtGBM6onY3QsidLLSN4Y5Xc4urfjTu6
         vfTUWEMZpuW9+wS4LFEMij9g4RE1QrbJyZBopiDYI8FIPggycfUODMpAXw0EjXMzejjr
         f86y+jEga+MIca9ijQ0asxd10aY1kjrh4aqCI=
DomainKey-Signature: a=rsa-sha1; c=nofws;
        d=gmail.com; s=gamma;
        h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc
         :content-transfer-encoding:message-id:references:to:x-mailer;
        b=R1wvT/6FWluCQMuqPFWfQpWLxBWO3gO8vojbvmNqUMHvqcl86SBAU3WssXTfC5H74a
         mlAOi/n+Mos0g4bQdIqHxFI2a3pRuK0e62NZ91b1sOHex4XV+rcnklqqjIloFXMyQn00
         ym+ogekMJpRCLjsRPflQqmUEznxrdTgMCLBpk=
Received: by 10.42.75.137 with SMTP id a9mr12211781ick.194.1300924596713;
        Wed, 23 Mar 2011 16:56:36 -0700 (PDT)
Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157])
        by mx.google.com with ESMTPS id i2sm5577062icv.15.2011.03.23.16.56.34
        (version=TLSv1/SSLv3 cipher=OTHER);
        Wed, 23 Mar 2011 16:56:35 -0700 (PDT)
Sender: Jacques Garrigue <jacques.garrigue@gmail.com>
Mime-Version: 1.0 (Apple Message framework v1082)
Content-Type: text/plain; charset=us-ascii
From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
In-Reply-To: <07EE3576-E5F0-4187-AE8C-DEFEA5C92303@gmail.com>
Date: Thu, 24 Mar 2011 08:56:32 +0900
Cc: caml-list@inria.fr
Content-Transfer-Encoding: 7bit
Message-Id: <622E23E3-5614-4ADE-B517-672577A406A2@math.nagoya-u.ac.jp>
References: <07EE3576-E5F0-4187-AE8C-DEFEA5C92303@gmail.com>
To: Joel Reymont <joelr1@gmail.com>
X-Mailer: Apple Mail (2.1082)
Subject: Re: [Caml-list] fighting the type system

On 2011/03/24, at 7:01, Joel Reymont wrote:

> How do I do this?
> 
> 	Thanks in advance, Joel

Well, you don't because this is clearly unsound.

> --- Util.ml
> 
> type 'a writable = < write : Protocol.t -> unit; .. > as 'a
> 
> module type Endpoint = 
> sig 
>  val request : unit -> 'a writable
>  val response : 'a writable -> 'b writable
>  val read_request : Protocol.t -> 'a writable
>  val read_response : Protocol.t -> 'a writable
> end

Your definition of 'a writable is actually equivalent to writing

  class type writable = object method write : Protocol.t -> unit end

and replacing uses of 'a writable by #writable.
The trouble is that returning a value of type #writable is unsound,
since it means that this value has any possible method, including write.
So you would be able to write:
     (request ())#foo
and have the type checker happily comply.

I'm not sure of what you're trying to do.
If you just want the Endpoint interface to specify an object type
containing at least write, you could use a private row type:

module type Endpoint = 
sig
 type writable = private <write : Protocol.t -> unit; .. >
 val request : unit -> writable
 val response : writable -> writable
 val read_request : Protocol.t -> writable
 val read_response : Protocol.t -> writable
end

You can then instantiate it with a concrete type, using
   Endpoint with type writable := mywriter

Jacques Garrigue