[Caml-list] Phantom types and read-only variables

[Yaron Minsky]

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

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Yaron Minsky]

One addendum. this can clearly be done with Obj.magic, but I'm
wondering if there's any safe alternative.

y

[Remi Vanicat]

On Sat, 5 Feb 2005 11:50:43 -0500, Yaron Minsky <ymi...@gmail.com> wrote:

Ocaml don't do any automatic type conversion, you have to explicitly coerce :
let freeze t = (t :> ro t)

will do what you want.

[Markus Mottl]

On Sat, 05 Feb 2005, Yaron Minsky 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:

[snip]

> 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?

Hm, it seems to me that the compiler could do a better job here.

Instead of writing:

type 'a t = { mutable value: int }

write:

type v = { mutable value: int }
type 'a t = v

This should make the code compile.

I think the compiler should be able to infer automatically that 'a isn't
used on the right hand side of the record definition (i.e. that it is
just a phantom type) without using the hint of a separate monomorphic
record definition. I guess this feature should be trivial to add.
Maybe in the next release? :-)

Regards,
Markus

--
Markus Mottl markus...@gmail.com http://www.ocaml.info

[Ethan Aubin]

(*

In article <891bd33905020...@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...@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 ();; *)

[Jacques Garrigue]

From: Markus Mottl <markus...@gmail.com>

> Hm, it seems to me that the compiler could do a better job here.
>
> Instead of writing:
>
> type 'a t = { mutable value: int }
>
> write:
>
> type v = { mutable value: int }
> type 'a t = v
>
> This should make the code compile.

Indeed, by doing that you make t extensible to a type that drops the
type parameter, meaning that type inference will never try to unify
the parameter.

A more direct way would be to define

type 'a t = int ref

Alternatively, you could just slightly change the definition of
freeze, to allow dropping the parameter

# type 'a t = { mutable value: int } ;;
# let freeze ({value=_} as v) = v ;;
val freeze : 'a t -> 'b t = <fun>

> I think the compiler should be able to infer automatically that 'a isn't
> used on the right hand side of the record definition (i.e. that it is
> just a phantom type) without using the hint of a separate monomorphic
> record definition. I guess this feature should be trivial to add.
> Maybe in the next release? :-)

Actually, this is a bit problematic.
Types defined as abbreviations are automatically expanded during
unification, so that unused parameters disappear.
But datatypes cannot be expanded, so their parameters are going to be
unified. Avoiding it would mean checking whether the parameters appear
in the real definition during unification. This is possible, but would
change the semantics of unification, something you want to be careful
about.

Actually ocaml 3.09 will go in the somehow opposite direction:
allowing private types to behave as phantom types. Currently private
types have their variance automatically inferred from their
definition, meaning you can use the above subtyping trick even after
the type is made private, but considering the fact they are
semi-abstract, it seems more natural to require their variance to be
explicitly given, allowing one to disallow such subtyping.

Jacques Garrigue