The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Sun, Oct 14, 2007 at 06:18:39PM +0200, Lukasz Stafiniak wrote:
> OK, it seems it would defy type erasure, so not much sense in thinking 
> about it.
> 
> On 10/12/07, Lukasz Stafiniak 
> <lukstafi AT gmail.com>
>  wrote:
> > Hello,
> >
> > I'm just coming back from a seminar about extracting programs for a
> > given evaluation strategy as evaluators, and I have this question...
> > How much the use of "Obj.magic" in extracted programs could be
> > avoided, if Coq extracted programs into a language with types
> > supporting GADT? (E.g. Haskell does.)
> >
> > Best Regards,
> > Łukasz
> >
> 

Well, to make a general (and vague...) answer, I'm pretty sure that
_any_ empowerment of the basic type system of Ocaml/Haskell can lead
to the removal of some Obj.magic in extracted code. Of course, to
temper this, I'm also pretty sure that we cannot remove all Obj.magic 
of all examples: the strength of Coq type system is far beyond what 
can be done in Haskell / Ocaml, even with nice extensions. 

Concerning GADT, they seem indeed quite interesting in this
prospect. Learning more about them and taking advantage of them (or
other type extensions) for extraction is somewhere in my "TODO" list.

For instance, it would be nice to avoid Obj.magic in extraction of 
records such as: 

Record MySubType : Type := { Carrier :> MyBaseType; 
                             SomeThingMore : Carrier -> Carrier }.

"Advanced" typing of extracted code has not been investigated much for
the moment. In fact, for simpicity sake, I was originally trying to
build an extraction as "generic" as possible, and in particular with
as little specific features of Haskell and Ocaml as possible. Now that
this "generic" extraction works reasonably well, it may indeed be time
to go further concerning the full use of the target type systems.

By the way, could you commment more on your point concerning 
"defy type erasure" ?

Regards, 
Pierre Letouzey