The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Well, in the general case that the annotations are not added in source, the compiler will conclude the most general thing it can to allow compilation to be as general as possible until it is needed to resolve a type. So, polymorphy is used where possible. It has a higher runtime cost, but allows you to be more flexible in code. Type annotations permit the compiler to perform generation that is specific to the type.

Are you just wanting to know the type of the functions that OCaml sees? Is there any way that you can use something like merlin? 

"How easy/hard/possible would it be..."

Well, if Coq doesn't have that now it is definitely possible, but likely hard. Probably you'd have to defer such an annotation to the time the OCaml compiler runs, in which case what you'd want is some way to recompose the source with the inferred types. This would probably require working with the Camlp4 library, as I understand that is the facility from which parsers for ocaml are written. You'd have to be able to construct the AST, infer types, annotate the AST with them, and then pretty print them out. So that's what I think is involved to get that :) 

On Thu, Jul 23, 2015 at 1:37 PM, Éric Tanter <etanter AT dcc.uchile.cl> wrote:

Hi,

Is it possible to instruct the extraction to ML to include type annotations in function signatures?

For instance, instead of producing this:

(** val foo : int -> int **)

let foo n = n + 1

I would like the following:

let foo (n:int) : int = n

If not, how easy/hard/possible would it be to support it?

Thanks!

— Éric

PS: yes, it *does* matter for the cases I’m considering ;-)