From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 99854BC88 for ; Sat, 5 Feb 2005 21:22:53 +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 j15KMqGh028038 for ; Sat, 5 Feb 2005 21:22:52 +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 VAA26741 for ; Sat, 5 Feb 2005 21:22:52 +0100 (MET) Received: from ciao.gmane.org (main.gmane.org [80.91.229.2]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j15KMpVk028035 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO) for ; Sat, 5 Feb 2005 21:22:52 +0100 Received: from list by ciao.gmane.org with local (Exim 4.43) id 1CxWQz-0007uY-5A for caml-list@inria.fr; Sat, 05 Feb 2005 21:21:37 +0100 Received: from denali.ccs.neu.edu ([129.10.116.200]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Sat, 05 Feb 2005 21:21:37 +0100 Received: from aubineth by denali.ccs.neu.edu with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Sat, 05 Feb 2005 21:21:37 +0100 X-Injected-Via-Gmane: http://gmane.org/ To: caml-list@inria.fr From: Ethan Aubin Subject: Re: Phantom types and read-only variables Date: Sat, 5 Feb 2005 20:21:26 +0000 (UTC) Message-ID: References: <891bd33905020508504e272acf@mail.gmail.com> <891bd33905020509243edf074d@mail.gmail.com> X-Complaints-To: usenet@sea.gmane.org X-Gmane-NNTP-Posting-Host: denali.ccs.neu.edu User-Agent: tin/1.4.1-19991201 ("Polish") (UNIX) (SunOS/5.9 (sun4u)) Sender: news X-Gmane-MailScanner: Found to be clean X-Gmane-MailScanner: Found to be clean X-MailScanner-From: gclci-caml-list@m.gmane.org X-MailScanner-To: caml-list@inria.fr X-Miltered: at nez-perce with ID 42052B1C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 42052B1B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; ccs:01 read-only:01 wrote:01 compiler:01 wrote:01 simulate:01 printf:01 printf:01 val:01 ...:98 neu:02 variables:02 unit:02 unit:02 types:02 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=none autolearn=disabled version=3.0.2 X-Spam-Level: (* In article <891bd33905020508504e272acf@mail.gmail.com> you wrote: > 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: Coincidentally, I was trying to to get a better grasp on phantom types and wrote something which you might find useful. My goal was to simulate file useage so that 1) you could not write a readonly file 2) you could downgrade the permissions on a file from read-write to readonly and 3) a file must be closed after using it. Perhaps some more advanced camler could like to tell me how to make this code more pretty? Also, I don't know if this is a proper arrow or not... - ethan.aubin@pobox.com *) type ('s1,'s2,'a) stateA = State of ('s1 -> ('a * 's2)) type filename = string ref type 'a file = File of filename type ('s1,'s2,'b) fileSt = ('s1 file,'s2 file, 'b) stateA let return a : ('a,'b,'c) fileSt = State (fun s -> (a,s)) let modify f : ('a,'b,'c) fileSt = State (fun st -> (), f st);; let frwopen () : [< `Read | `Write] file = File (ref "empty") let fropen () : [< `Read] file = File (ref "empty") let fwopen () : [< `Write] file = File (ref "empty") let read : (([> `Read] as 'perm), 'perm, string) fileSt = State (fun st -> let File r = st in !r,st) let write ~str : ([> `Write] as 'perm,'perm,unit) fileSt = State (fun (File r) -> r := str; (),File r) let print : (([> `Read] as 'a),'a,unit) fileSt = State (fun (File r) -> Printf.printf "value=%s\n" !r; ((), File r));; let closef ((File r) : [< `Write | `Read] file) : [`Close] file = File r;; (* This is not useful, because infered type is: val close : (_[< `Read | `Write ], [ `Close ], unit) fileSt *) (* let close = modify closef;; *) let to_readonly = let f ((File r) : [> `Read] file) : [`Read] file = File r in modify f;; let (>>>) ((State f) : ('a,'b,'c) fileSt) ((State g) : ('d,'e,'f) fileSt) : ('g,'h,'i) fileSt = State (fun s -> let (_,s1) = f s in g s1);; let r = read and w = write "i";; let runFileSt ~comp:((State f) : ('perm,[`Close],'v) fileSt) ~(st : [< `Read | `Write] file) () : 'v = let (v,_) = f st in v;; (* Print a file, update it, print the new value, close it *) let comp = print >>> w >>> print >>> (modify closef);; runFileSt ~comp ~st:(frwopen ()) ();; let permdown = print >>> w >>> to_readonly >>> print >>> (modify closef);; runFileSt ~comp:permdown ~st:(frwopen ()) ();; (* This correctly doesn't type *) (* let write_to_readonly = print >>> w >>> to_readonly >>> w >>> (modify closef);; *) (* Don't close the file, *) let bad_file_left_open = print >>> w >>> print;; (* so we refuse to run it. i.e. This fails to type *) (* runFileSt ~comp:bad_file_left_open ~st ();; *)