The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

Hello.

We've developed a very small monadic IO library in O'Caml and are
trying to get code extracted from Coq to use it.

The O'Caml interface looks like:

io.ml:

type 'a io

val pure : 'a -> 'a io
val bind : 'a io -> ('a -> 'b io) -> 'b io
val run  : 'a io -> 'a io_result
val lift : (unit -> 'a io_result) -> 'a io

io_file.mli:

val open_read     : string -> (handle -> 'a io) -> 'a io
val open_write    : string -> (handle -> 'a io) -> 'a io
val open_truncate : string -> (handle -> 'a io) -> 'a io
val write         : handle -> string -> int64 io
...

Now the above interface for the open* functions obviously
allows one to leak the file handle...

  open_read "file.txt" (fun h -> pure h)

So, in the Coq interface, we've attempted to add extra type
safety:

IO_File.v:

Inductive read_mode : Prop :=
  | Read      : read_mode
  | Read_None : read_mode.

Inductive write_mode : Prop :=
  | Write      : write_mode
  | Write_None : write_mode.

Axiom handle : read_mode -> write_mode -> Prop -> Type.
Extract Constant handle => "handle".

Axiom open_truncate : forall {A : Set}, string -> (forall {S : Prop}, handle 
Read_None Write S -> IO.io A) -> IO.io A.
Extract Constant open_truncate => "open_truncate".

It's the same technique as Haskell's ST monad; using a higher
rank type to prevent leakage of a resource. We also branded file
handles with their "mode" to statically prevent writing to file
handles opened in read-only mode, and so on.

The problem occurs when it comes to extracting code that uses
the library:

Axiom file_name : string.
Axiom message   : string.

Definition test : IO.io unit :=
  IO_File.open_truncate file_name
    (fun _ handle => IO.order
      (IO_File.write handle message)
      (IO.pure tt)).

Extracting this function results in:

let test =
  open_truncate file_name (fun _ handle ->
    order (write handle message) (pure ()))

Note that the argument to the function passed to
open_truncate is in the Prop sort but hasn't been removed
by extraction. The type of this function obviously doesn't
match what the O'Caml definition is expecting!

Any ideas what's going on here? We're open to suggestions of
alternatives to the higher rank type, too.