The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

First of all, please provide complete files to explain what you want
use of Parameter/Variable/Axiom is acceptable if a definition dœsn't
matter.

Le Tue, 5 Jul 2011 14:21:16 +0000,
frank maltman 
<frank.maltman AT googlemail.com>
 a écrit :

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

I don't see any interest in providing such propositionnal types, as
you won't be able to use them effectively.

For instance, you won't be able to prove that "Read <> Read_None"
(unless you use an axiom, but if so, you should have put it in Set/Type)

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

I don't understand why you need this Prop parameter; have you read the
manual about extraction? Have you tried Extraction Implicit?
If not, do it; you may also consider taking a look in the Cocorico!
wiki, about Extraction, or send a more complete (and parsable) file to
give better explanations of what you want.

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