The Coq mailing list

[Éric Tanter <etanter AT dcc.uchile.cl>]

Thanks for your answers but I guess I didn’t express myself clearly, since the problem I’m pointing out is not addressed.

(background: while I’m clearly not an OCaml expert, I do know about parametric polymorphism, type theory, basic Coq usage, and the documentation about extraction.)

I found a very minimal example that makes my point (I’m in Coq 8.5beta2):

Test.v

--------

Require Import String ExtrOcamlString.

Extraction "append.ml" append.

This yields the following definitions:

in append.ml

-----------------

(** val append : char list -> char list -> char list **)

let rec append s1 s2 =

  match s1 with

  | [] -> s2

  | c::s1' -> c::(append s1' s2)

in append.mli

------------------

val append : char list -> char list -> char list

As you can notice, append in append.ml has a _more general inferred_ type than what it is meant to have:

$ ocaml -init append.ml

        OCaml version 4.02.1

# append;;

- : 'a list -> 'a list -> 'a list = <fun>

This means that for instance, the _expression_ `append [] []' in append.ml has type ‘a list, instead of having type char list. 

so if you add that to the .ml file:

let x = append [] [];;

print_endline x

the compiler complains:

File "append.ml", line 13, characters 14-15:

Error: This _expression_ has type 'a list

       but an _expression_ was expected of type string

So the extra polymorphism that is granted by leaving the type implicit in append.ml is a double-edged sword. Can be helpful, but can be problematic.

In a larger development (no idea why the problem does not reproduce with a more minimalist file), the mismatch between the .ml file and the .mli file even prevents compilation:

$ ocamlc foo.mli

$ ocamlc foo.ml

File “foo.ml", line 1:

Error: The implementation foo.ml

       does not match the interface foo.cmi:

       Values do not match:

         val append : 'a list -> 'a list -> 'a list

       is not included in

         val append : char list -> char list -> char list

       File “foo.ml", line 59, characters 8-14: Actual declaration

I have noticed that extraction to Haskell *does* include the type information *for real* (ie. not as a comment).

append :: char list -> char list -> char list

append s1 s2 =

  case s1 of {

   [] -> s2;

   (c : s1') -> c : (append s1' s2)}

Doing the same in OCaml would prevent the issues I describe above.

Is that clearer?

Thanks,

— Éric