OO design

OO design

[David Baelde]

Hi,

I'm no OO guru, so my question may be irrelevant, or there just might
not be an answer, which wouldn't hurt..

Let's say that I have a base class, with some kind of activation
procedure: anybody wanting to use the class must call #enter before,
and then call #leave for releasing. Internally, the methods #do_enter
and #do_leave are called respectively at the first #enter and last
#leave.

Nobody should call the #do_* directly, and I'd also like to make sure
the #enter and #leave are never overriden, since their behaviour is
important and actually much more complex than what I said.

I could just rely on the user who derives my base class, but let's see
what we can do. First the #do_* should be made private, so they can be
defined in the derived classes, but never called from the outside. To
avoid the overriding of #enter and #leave the only solution seems to
make them normal functions instead of methods. But then how could
#enter call #do_enter ? I tried to first define the class with public
#enter and make that method private in the interface, but OCaml told
me that was impossible.

I'm just curious if anybody has an opinion/idea about that.
--
David

Re: [Caml-list] OO design

[Gerd Stolpmann]

Am Freitag, den 05.05.2006, 11:35 +0200 schrieb David Baelde:
> Hi,
> 
> I'm no OO guru, so my question may be irrelevant, or there just might
> not be an answer, which wouldn't hurt..
> 
> Let's say that I have a base class, with some kind of activation
> procedure: anybody wanting to use the class must call #enter before,
> and then call #leave for releasing. Internally, the methods #do_enter
> and #do_leave are called respectively at the first #enter and last
> #leave.
> 
> Nobody should call the #do_* directly, and I'd also like to make sure
> the #enter and #leave are never overriden, since their behaviour is
> important and actually much more complex than what I said.
> 
> I could just rely on the user who derives my base class, but let's see
> what we can do. First the #do_* should be made private, so they can be
> defined in the derived classes, but never called from the outside. To
> avoid the overriding of #enter and #leave the only solution seems to
> make them normal functions instead of methods. But then how could
> #enter call #do_enter ? I tried to first define the class with public
> #enter and make that method private in the interface, but OCaml told
> me that was impossible.
> 
> I'm just curious if anybody has an opinion/idea about that.

There is an easy solution if you completely forbid subclassing (see
below). However, there is no water-proof solution, because class types
are structural in O'Caml, i.e. you cannot prevent that a user simulates
subclassing using this style:

class pirate_foo (foo : official_foo) =
  object
    method enter = ...
    method leave = ...
    method other_method = foo # other_method
  end

If you want to safely encapsulate a certain invariant into a structure
you must go with modules/functors in O'Caml.

To forbid explicit subclassing just do not to export the class as such:

module Foo : sig
 class type foo_type =
   object
     method enter : ...
     method leave : ...
     ...
   end

 val create_foo : ... -> foo_type
end = struct
 class type foo_type =
   object
     method enter : ...
     method leave : ...
     ...
   end

 class foo ... : foo_type =
    object  
     method enter ... = ...
     method leave ... = ...
     ...
   end

 let create_foo ... = new foo ...
end

Without class, the user can no longer inherit from it. The created
object, however, is fully usable.

I do not see a way how to completely hide enter and leave from the class
type. 

Gerd
-- 
------------------------------------------------------------
Gerd Stolpmann * Viktoriastr. 45 * 64293 Darmstadt * Germany 
gerd@gerd-stolpmann.de          http://www.gerd-stolpmann.de
Phone: +49-6151-153855                  Fax: +49-6151-997714
------------------------------------------------------------

Re: [Caml-list] OO design

[Remi Vanicat]

2006/5/5, David Baelde <david.baelde@gmail.com>:
> Hi,
>
> I'm no OO guru, so my question may be irrelevant, or there just might
> not be an answer, which wouldn't hurt..
>
> Let's say that I have a base class, with some kind of activation
> procedure: anybody wanting to use the class must call #enter before,
> and then call #leave for releasing. Internally, the methods #do_enter
> and #do_leave are called respectively at the first #enter and last
> #leave.
>
> Nobody should call the #do_* directly, and I'd also like to make sure
> the #enter and #leave are never overriden, since their behaviour is
> important and actually much more complex than what I said.

If the solution given Gerd Stolpmann have the problem to disallow the
inheritence, I've another that make ineritence and overriding enter
and leave possible, but ensure that method that overide enter and
leave do call the old enter and leave :

struct
  type enter = unit
  type leave = unit
  class foo =
     method enter ... : enter = ....
     method leave ....: leave = ...
     ....
   end
end : sig
  type enter
  type leave
  class foo :
    method enter : ... -> enter
    method leave : ... -> leave
  end
end

after this, the only way to produce an object of type enter is to call
the original enter method (same for leave). And as method that overide
enter must have the same type, the have to call the enter method to
have it (well, there might be other way, but the user of the method
have to make thing complicated for this).

Another plus of this method of doing it is that if you haev e method of type
  method bar : enter -> unit
then one can only call it if he had call previously the enter method.

Re: [Caml-list] OO design

[Andrej Bauer]

Remi Vanicat wrote:
> 2006/5/5, David Baelde <david.baelde@gmail.com>: 
> after this, the only way to produce an object of type enter is to call
> the original enter method (same for leave).

... or throw an exception, or loop forever, or print a poem on sreen
then call the original function, or call original enter twice, or call
original enter, then original leave, then original enter, etc.

Andrej

Re: [Caml-list] OO design

[Jacques Garrigue]

From: "David Baelde" <david.baelde@gmail.com>

> I'm no OO guru, so my question may be irrelevant, or there just might
> not be an answer, which wouldn't hurt..
> 
> Let's say that I have a base class, with some kind of activation
> procedure: anybody wanting to use the class must call #enter before,
> and then call #leave for releasing. Internally, the methods #do_enter
> and #do_leave are called respectively at the first #enter and last
> #leave.
> 
> Nobody should call the #do_* directly, and I'd also like to make sure
> the #enter and #leave are never overriden, since their behaviour is
> important and actually much more complex than what I said.
> 
> I could just rely on the user who derives my base class, but let's see
> what we can do. First the #do_* should be made private, so they can be
> defined in the derived classes, but never called from the outside. To
> avoid the overriding of #enter and #leave the only solution seems to
> make them normal functions instead of methods. But then how could
> #enter call #do_enter ? I tried to first define the class with public
> #enter and make that method private in the interface, but OCaml told
> me that was impossible.

I would be tempted to say: there is no answer.
Ocaml objects are not about enforcing protocols, but about allowing
inheritance and structural subtyping, and this does not fit well with
your problem.
There are many things you can try to make it harder to derive incorrect
classes, but basically if the user wants to do it, he can.

Yet, since it seems that you are already relying on the (library)
programmer to write correct code for the #do_* methods, another point
of view might be that you just want to make sure that only the final user
of objects cannot break things. Then the technique described in other
answers make sense, for instance prohibiting inheritance from an
already completed class.
An even stronger protection is to make object types private. This way you
are sure than nobody can forge an object of the same type, and you can
even hide public methods if you wish. But you loose inheritance.
See the object example in my paper on private rows about how to do this.

Combining structural subtyping and modular privacy would introduce a
lot extra complexity in the type system.

Jacques Garrigue

Re: [Caml-list] OO design

[David Teller]

On Monday 08 May 2006 05:17, Jacques Garrigue wrote:
> I would be tempted to say: there is no answer.
> Ocaml objects are not about enforcing protocols, but about allowing
> inheritance and structural subtyping, and this does not fit well with
> your problem.

Which brings us to a question : how do you enforce protocols in OCaml ?

Say, is there a "good" way of rewriting file-related operations so that, say, 
ProtocolUnix.read and ProtocolUnix.write *statically* only accept opened 
files, and in addition, ProtocolUnix.write only accepts files which have been 
opened with write priviledges ?

I mean, there are manners of checking this with, say, model checking tools. In 
the specific case of file management, I guess we can do it with a little bit 
of simple subclassing, but I assume there's a large run-time penalty for this 
extra bit of checking, due to the management of objects by OCaml. Has anyone 
attempted to determine how well this scales up ? Or explored other options ?

Cheers,
 David

Re: [Caml-list] OO design

[Dan Grossman]

Phantom types are a programming idiom that can often pull off this sort 
of thing.

--Dan

David Teller wrote:
> On Monday 08 May 2006 05:17, Jacques Garrigue wrote:
> 
>>I would be tempted to say: there is no answer.
>>Ocaml objects are not about enforcing protocols, but about allowing
>>inheritance and structural subtyping, and this does not fit well with
>>your problem.
> 
> 
> Which brings us to a question : how do you enforce protocols in OCaml ?
> 
> Say, is there a "good" way of rewriting file-related operations so that, say, 
> ProtocolUnix.read and ProtocolUnix.write *statically* only accept opened 
> files, and in addition, ProtocolUnix.write only accepts files which have been 
> opened with write priviledges ?
> 
> I mean, there are manners of checking this with, say, model checking tools. In 
> the specific case of file management, I guess we can do it with a little bit 
> of simple subclassing, but I assume there's a large run-time penalty for this 
> extra bit of checking, due to the management of objects by OCaml. Has anyone 
> attempted to determine how well this scales up ? Or explored other options ?
> 
> Cheers,
>  David
> 
> _______________________________________________
> 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

Re: OO design

[Geoffrey Alan Washburn]

Dan Grossman wrote:

> Phantom types are a programming idiom that can often pull off this sort 
> of thing.

	Maybe I'm just not smart enough, but I can't seem to think of a way to 
do this in an effectful language without getting bitten by aliasing.  In 
a purely functional setting, a monadic approach seems plausible, but if 
you can create a "ref" anywhere, as in OCaml, it seems straightforward 
to subvert any uses of phantom types for implementing protocols.  I 
suppose one could look at it from the angle that phantom types make it 
harder for cooperative users to make mistakes, but I can't see how they 
can prevent the need for runtime checks.

Re: [Caml-list] Re: OO design

[Dan Grossman]

I totally agree -- effects limit the class of protocols you can enforce, 
but I believe (please correct me if I've missed a dirty trick) the 
"simple stuff" still works fine.  For example:

type read;
type write;
type 'a file;
val open_r : string -> read file;
val open_w : string -> write file;
val write : write file -> char -> unit;
val read : read file -> char;
val close : 'a file -> unit;

It enforces that you don't confuse your reads and writes, but *not* that 
you don't use a file after you close it.  A monadic approach (where each 
operation would return a "new" file) or linearity appears necessary for 
the latter.

--Dan

Geoffrey Alan Washburn wrote:
> Dan Grossman wrote:
> 
>> Phantom types are a programming idiom that can often pull off this 
>> sort of thing.
> 
> 
>     Maybe I'm just not smart enough, but I can't seem to think of a way 
> to do this in an effectful language without getting bitten by aliasing.  
> In a purely functional setting, a monadic approach seems plausible, but 
> if you can create a "ref" anywhere, as in OCaml, it seems 
> straightforward to subvert any uses of phantom types for implementing 
> protocols.  I suppose one could look at it from the angle that phantom 
> types make it harder for cooperative users to make mistakes, but I can't 
> see how they can prevent the need for runtime checks.
> 
> _______________________________________________
> 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

Re: OO design

[Geoffrey Alan Washburn]

Dan Grossman wrote:

> It enforces that you don't confuse your reads and writes, but *not* that 
> you don't use a file after you close it.  A monadic approach (where each 
> operation would return a "new" file) or linearity appears necessary for 
> the latter.

	Okay, good point.  However, that raises the interesting question of 
whether there is a nice positive specification of the class of 
"protocols" that are expressible in the presence of effects, rather than 
a negative characterization -- all those that can be broken by aliasing, 
nontermination, etc.

Re: [Caml-list] Re: OO design

[Shawn]

Dan Grossman wrote:
>
> I totally agree -- effects limit the class of protocols you can 
> enforce, but I believe (please correct me if I've missed a dirty 
> trick) the "simple stuff" still works fine.  For example:
>
> type read;
> type write;
> type 'a file;
> val open_r : string -> read file;
> val open_w : string -> write file;
> val write : write file -> char -> unit;
> val read : read file -> char;
> val close : 'a file -> unit;
>
> It enforces that you don't confuse your reads and writes, but *not* 
> that you don't use a file after you close it.  A monadic approach 
> (where each operation would return a "new" file) or linearity appears 
> necessary for the latter.
How can an approach like this handle files opened for reading and 
writing at the same time? Hmm. Maybe an OO approach? readable_file and 
writable_file classes, and a read_write_file that inherits from both. 
It'd be easy to add new file-like types too. I'm not normally a big fan 
of OO, but this is a place where it seems to make sense to use. Of 
course, it doesn't do anything about the compile time checking of 
attempts to use a closed file either.

Re: [Caml-list] Re: OO design

[brogoff]

On Wed, 10 May 2006, Dan Grossman wrote:
> I totally agree -- effects limit the class of protocols you can enforce,
> but I believe (please correct me if I've missed a dirty trick) the
> "simple stuff" still works fine.  For example:
>
> type read;
> type write;
> type 'a file;
> val open_r : string -> read file;
> val open_w : string -> write file;
> val write : write file -> char -> unit;
> val read : read file -> char;
> val close : 'a file -> unit;
>
> It enforces that you don't confuse your reads and writes, but *not* that
> you don't use a file after you close it.

I think phantom types are overkill for this kind of either/or interface.
The method used in the OCaml library of having an in_channel and out_channel
is straightforward enough. Phantom types would make more sense to me
when you have files which can be read and written, with an interface like this

module File :
    sig
      type (-'a) file

      val open_in : string -> [`In] file
      val open_out : string -> [`Out] file
      val open_inout : string -> [`In|`Out] file
      val read : [> `In ] file -> char
      val write : [> `Out ] file -> char -> unit
      val close : 'a file -> unit
    end =
  struct
    (* Implementation omitted *)
  end ;;

Note that I used polymorphic variants or row types to model this, I'm not
sure how to do this cleanly in SML. Of course, you could code it up as
in_channel, out_channel, and inout_channel ;-)

>  A monadic approach (where each
> operation would return a "new" file) or linearity appears necessary for
> the latter.

Yoann Padioleau's suggestion to use the Lisp approach (with-open-file)
looks like the best approach for ML to me.

-- Brian

Re: [Caml-list] Re: OO design

[Dan Grossman]

I believe
http://arxiv.org/abs/cs.PL/0403034
is relevant, claiming that phantom types can encode any first-order 
subtyping hierarchy.

If I recall correctly, you force the client to provide "witnesses" 
(i.e., coercions), which to answer a later question in the thread, is 
how you can support things like passing a "read_write" file handle to 
read.  That is, you have a functions like:

val up_to_read : read_write file -> read file
val up_to_write : read_write file -> write file

These are the identity function and we can expect cross-module inlining 
to remove them.

--Dan

Geoffrey Alan Washburn wrote:
> Dan Grossman wrote:
> 
>> It enforces that you don't confuse your reads and writes, but *not* 
>> that you don't use a file after you close it.  A monadic approach 
>> (where each operation would return a "new" file) or linearity appears 
>> necessary for the latter.
> 
> 
>     Okay, good point.  However, that raises the interesting question of 
> whether there is a nice positive specification of the class of 
> "protocols" that are expressible in the presence of effects, rather than 
> a negative characterization -- all those that can be broken by aliasing, 
> nontermination, etc.
> 
> _______________________________________________
> 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

Re: [Caml-list] Re: OO design

[Till Varoquaux]

One rather standard way to preserve atomicity of open/close operation
is to use with... commands:

let with_open_out filename f =
 let chan = open_out filename in
 let res=(try
           f chan
          with e ->
           close_out chan;
           raise e)
 in
 close_out chan;
 res

Where f is the function you want to use to generate f's content (takes
an out_channel).
This forces chan to be closed no matter what happens.


You may also want to have a look at ocamlnet's channel's
implementation (it's OO and might do a lot of you are looking for):
http://ocamlnet.sourceforge.net/refman/Netchannels.html

Cheers,
Till
On 5/10/06, Shawn <shawnw@speakeasy.org> wrote:
> Dan Grossman wrote:
> >
> > I totally agree -- effects limit the class of protocols you can
> > enforce, but I believe (please correct me if I've missed a dirty
> > trick) the "simple stuff" still works fine.  For example:
> >
> > type read;
> > type write;
> > type 'a file;
> > val open_r : string -> read file;
> > val open_w : string -> write file;
> > val write : write file -> char -> unit;
> > val read : read file -> char;
> > val close : 'a file -> unit;
> >
> > It enforces that you don't confuse your reads and writes, but *not*
> > that you don't use a file after you close it.  A monadic approach
> > (where each operation would return a "new" file) or linearity appears
> > necessary for the latter.
> How can an approach like this handle files opened for reading and
> writing at the same time? Hmm. Maybe an OO approach? readable_file and
> writable_file classes, and a read_write_file that inherits from both.
> It'd be easy to add new file-like types too. I'm not normally a big fan
> of OO, but this is a place where it seems to make sense to use. Of
> course, it doesn't do anything about the compile time checking of
> attempts to use a closed file either.
>
> _______________________________________________
> 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
>

Re: [Caml-list] Re: OO design

[Shawn]

Till Varoquaux wrote:
> One rather standard way to preserve atomicity of open/close operation
> is to use with... commands:

Why are you top-posting?

Anyways, doing just that is what I usually do, but because it's 
simpler/shorter to just call a function than rewrite the file 
opening/closing code every time I need I/O, not because I worry about 
forgetting to close the file when I'm done.

Re: OO design

[Geoffrey Alan Washburn]

brogoff wrote:
>>  A monadic approach (where each
>> operation would return a "new" file) or linearity appears necessary for
>> the latter.
> 
> Yoann Padioleau's suggestion to use the Lisp approach (with-open-file)
> looks like the best approach for ML to me.

	It has advantages, but I'm not seeing how this prevents the problems 
with aliasing.  Take Till's version (with_open_out), it gives the 
function the channel itself.  There is nothing to stop the function from 
stashing the channel in a reference cell and then later attempting to 
use it after it has been closed.

	So giving the function the channel directly is bad, what about instead 
passing it some functions to manipulate the open channel?  Same problem.

	Another solution almost solves the problem of never reading from or 
writing to a closed channel is to have an "implicit" current channel 
that starts out as stdin/stdout.  Then "with-open" would change the 
current implicit channel.  However, this actually just transforms the 
problem from "trying to read from or write to a closed channel" to 
"reading from or writing to the wrong channel".

	The only "solution" that I've seen that seems to actually solve the 
"problem" is to write a small interpreted language for performing I/O, 
but that is a bit heavy weight for general use.

Re: [Caml-list] Re: OO design

[Till Varoquaux]

> > Yoann Padioleau's suggestion to use the Lisp approach (with-open-file)
> > looks like the best approach for ML to me.

OOps, I just saw Yann's post.... guess I should have read this thread
more carefuly before posting.

>         The only "solution" that I've seen that seems to actually solve the
> "problem" is to write a small interpreted language for performing I/O,
> but that is a bit heavy weight for general use.

I might be stating the obvious but a solution that *should* work in
most cases would be to use a event way of reading (think sax) where
you would pass a "reading" function that would be called back one or
more time with data from the file. If this "reading" function where to
return false "read_from_file" would stop calling it back:

read_from_file: (filename:String) (f:String->Boolean) : Unit

The writing counterpart could be:

flush_to_file:(filename:String) (f:Unit->String Option) : Unit

where f would be called until it returned None.

Note that this is a rather unflexible and inelegant solution. I don't
recommand it.

Cheers,
Till

Re: [Caml-list] Re: OO design

[Jacques Garrigue]

From: Dan Grossman

> A monadic approach (where each
> operation would return a "new" file) or linearity appears necessary for
> the latter.

And you can perfectly encode the monadic approach in ocaml.
In our case, we need the type of the monad to keep information about
open and closed files.
I include such a solution, which ensures the safety of file accesses,
at the end of this post. Note that file handles are indexed
statically, but you can use as many as you wish.

It should be safe with references (there is no file handle that you
can keep around, everything stays in the monad.) But beware of fancy
extensions, like continuations, that would allow you to capture your
environement, included files that were open when you created the
continuation...

From: Geoffrey Alan Washburn

> 	The only "solution" that I've seen that seems to actually solve the 
> "problem" is to write a small interpreted language for performing I/O, 
> but that is a bit heavy weight for general use.

I see indeed no other easy option if you have continuations in the
language.

Jacques

(* safeio.mli *)
type ('a,'b) monad    (* A monad, with action 'a, returning 'b *)
type ('a,'b) handle   (* A file handle to be used/modified *)
type input = [`In]    (* Permissions *)
type output = [`Out]
type active = [`In|`Out]
type closed = [`Closed]
type all_closed = <c: closed; n: all_closed> (* All files closed *)

val ch1 : (<c:'a;n:'b> -> <c:'c;n:'b>, 'a -> 'c) handle
val succ : ('a -> 'b, 'c) handle -> (<c:'d;n:'a> -> <c:'d;n:'b>, 'c) handle
val ch2 : (* shorthand for [succ ch1] *)
    (<c:'a; n: <c:'b; n:'c> > -> <c:'a; n: <c:'d; n:'c> >, 'b -> 'd) handle

val run : (all_closed -> all_closed, 'a) monad -> 'a

val open_in : ('a, closed -> input) handle -> string -> ('a, unit) monad
val open_out : ('a, closed -> output) handle -> string -> ('a, unit) monad
val close : ('a, [< active] -> closed) handle -> ('a, unit) monad
val input : ('a, input -> input) handle -> ('a, char option) monad
val output : ('a, output -> output) handle -> char -> ('a, unit) monad

val return : 'a -> ('b -> 'b, 'a) monad
val bind :
  ('a -> 'b, 'd) monad -> ('d -> ('b -> 'c, 'e) monad) -> ('a -> 'c, 'e) monad
val ( $ ) :
  ('a -> 'b, unit) monad -> ('b -> 'c, 'd) monad -> ('a -> 'c, 'd) monad

(* safeio.ml *)
type channel = Closed | In of in_channel | Out of out_channel
type channels = {mutable c: channel; mutable n: channels option}
type ('a,'b) monad = channels -> 'b
type ('a,'b) handle = int
(* Implementation left as exercise... *)

(* Example of use *)
open Safeio ;;

let rec copy2 () =
  bind (input ch1)
    (function None -> return ()
    | Some c -> bind (output ch2 c) copy2);;
val copy2 : unit ->
  (< c : input; n : < c : output; n : 'a > > ->
   < c : input; n : < c : output; n : 'a > >, unit) monad

let copy_file f1 f2 =
  open_in ch1 f1 $
  open_out ch2 f2 $
  copy2 () $
  close ch1 $
  close ch2 ;;

run (copy_file "a" "b") ;;

Re: OO design

[Geoffrey Alan Washburn]

Jacques Garrigue wrote:
> From: Dan Grossman
> 
>> A monadic approach (where each
>> operation would return a "new" file) or linearity appears necessary for
>> the latter.
> 
> And you can perfectly encode the monadic approach in ocaml.
> In our case, we need the type of the monad to keep information about
> open and closed files.
> I include such a solution, which ensures the safety of file accesses,
> at the end of this post. Note that file handles are indexed
> statically, but you can use as many as you wish.
> 
> It should be safe with references (there is no file handle that you
> can keep around, everything stays in the monad.) But beware of fancy
> extensions, like continuations, that would allow you to capture your
> environement, included files that were open when you created the
> continuation...

	Ah, good point.  I hadn't been thinking about it quite correctly when I 
was doing the thought experiment, but a simpler way to look at it is 
that "the IO monad and the (implicit) state monad commute".  Therefore, 
mutable references won't actually cause a problem.

Re: [Caml-list] OO design

[yoann padioleau]

 
> Which brings us to a question : how do you enforce protocols in OCaml ?
> 
> Say, is there a "good" way of rewriting file-related operations so that, say, 
> ProtocolUnix.read and ProtocolUnix.write *statically* only accept opened 
> files, and in addition, ProtocolUnix.write only accepts files which have been 
> opened with write priviledges ?

Have different types,  in_channel  and out_channel. But ocaml already have this.
The problem is that when you close a channel, ocaml does not warn you
if you try to read from a close channel.

> 
> I mean, there are manners of checking this with, say, model checking tools. In 
> the specific case of file management, I guess we can do it with a little bit 
> of simple subclassing, but I assume there's a large run-time penalty for this 
> extra bit of checking, due to the management of objects by OCaml. Has anyone 
> attempted to determine how well this scales up ? Or explored other options ?

Using higher order functions.
Instead of having a  open/read/close sequence protocol that you must follow, 
enforce such a protocol by defining a higher order function let's say
with_open_out_file that do all that for you under the hood.


with_open_out_file "/tmp/test.txt" (fun write_func -> 
 (* you can call write_func that do the writing *)
  write_func "toto";
  write_func "titi";
 );
 


let with_open_out_file file f = 
 let chan = open_out file in
 let read_func = output_string chan in

  try (
   f read_func;
   close_out chan;
  ) 
 with 
  x -> close_out chan; raise x


Note how the channel is automatically closed for you. 


This technique is used in Lisp library I think.