Re: Phantom types and read-only variables

[Ethan Aubin <aubineth@ccs.neu.edu>]

(*
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 ();; *)