The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 02/10/2012 12:16 PM, AUGER Cédric wrote:
> Hi, all;
> I would like to know what is the reason why the following code:
>
>    
> > Record foo : Type := {bar:forall (A:Set), A ->  A; foobar:nat}.
> > Definition id : foo := {|bar := fun A a =>  a; foobar := 0|}.
> >
> > Recursive Extraction id.
> >      
> is extracted to:
>
>    
> > > type __ = Obj.t
> > >
> > > type nat =
> > > | O
> > > | S of nat
> > >
> > > type foo = { bar : (__ ->  __ ->  __); foobar : nat }
> > >
> > > (** val id : foo **)
> > >
> > > let id =
> > >   { bar = (fun _ a ->  a); foobar = O }
> > >        

OCaml does support first-class polymorphism at the top level of a record 
field's type, but I imagine the extraction translation would be 
complicated by the need to use first-class polymorphism in only those 
positions, so it hasn't been implemented.  (If it isn't clear, the field 
[bar] above is an example of first-class polymorphism, where type 
parameters are quantified at some point beside the beginning of a 
[let]-bound definition.)