From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <pierre.weis@inria.fr>
Delivered-To: caml-list@yquem.inria.fr
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78])
	by yquem.inria.fr (Postfix) with ESMTP id 099FDBC88
	for <caml-list@yquem.inria.fr>; Sat,  5 Feb 2005 17:50:46 +0100 (CET)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j15GojpU008023
	for <caml-list@yquem.inria.fr>; Sat, 5 Feb 2005 17:50:45 +0100
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id RAA19672 for <caml-list@pauillac.inria.fr>; Sat, 5 Feb 2005 17:50:45 +0100 (MET)
Received: from wproxy.gmail.com (wproxy.gmail.com [64.233.184.199])
	by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j15GoiA8008020
	for <caml-list@inria.fr>; Sat, 5 Feb 2005 17:50:44 +0100
Received: by wproxy.gmail.com with SMTP id 58so559426wri
        for <caml-list@inria.fr>; Sat, 05 Feb 2005 08:50:44 -0800 (PST)
DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws;
        s=beta; d=gmail.com;
        h=received:message-id:date:from:reply-to:to:subject:mime-version:content-type:content-transfer-encoding;
        b=PFTh5Qf+dgTNcVFN4O1ubpgdx59UjMnJImY24c9ueBbFzxhni0syOFhA/zWVz/yYEVoayXgk0G+VsDAg776SDDomiwCsr53I3NaX8jMgODA2uw0qvLAn3uAeIEsHgv3SBqBfGRp4u0XLhRp/XJl6JQgxukMMNlNE9bJ6Sx1fRhQ=
Received: by 10.54.47.17 with SMTP id u17mr265524wru;
        Sat, 05 Feb 2005 08:50:43 -0800 (PST)
Received: by 10.54.2.70 with HTTP; Sat, 5 Feb 2005 08:50:43 -0800 (PST)
Message-ID: <891bd33905020508504e272acf@mail.gmail.com>
Date: Sat, 5 Feb 2005 11:50:43 -0500
From: Yaron Minsky <yminsky@gmail.com>
Reply-To: yminsky@cs.cornell.edu
To: Caml Mailing List <caml-list@inria.fr>
Subject: Phantom types and read-only variables
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
X-Miltered: at nez-perce with ID 4204F965.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Miltered: at nez-perce with ID 4204F964.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; yaron:01 minsky:01 yminsky:01 read-only:01 compiler:01 struct:01 mutable:01 sig:01 val:01 val:01 compiler:01 complains:01 int:01 int:01 constraints:01 
X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr
X-Spam-Status: No, score=0.0 required=5.0 tests=RCVD_BY_IP autolearn=disabled 
	version=3.0.2
X-Spam-Level: 

I'm trying to use phantom types to build a "freezable" variable, where
I can create a version of the variable to which write operations can
not be applied.  Here's my first attempt, which was rejected by the
compiler:

type ro = Readonly
type rw = Readwrite

module M = 
struct
  type 'a t = { mutable value: int }

  let create i = { value = i }
  let freeze t = t
  let read x = x.value
  let write x i =
    x.value <- i
end

module N = 
  (M : sig
     type 'a t
     val create : int -> rw t
     val freeze : 'a t -> ro t
     val read : 'a t -> int
     val write : rw t -> int -> unit
   end)

I do basically understand why the compiler rejects module N.  It
basically complains that the freeze in M is not compatible with the
constraints on N.  In particular:

Values do not match:
  val freeze : 'a -> 'a
is not included in
  val freeze : 'a t -> ro t

So, what's the right approach here?

y