The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

----- Mail original -----
> Hi Trevor, cc-Pierre,
> 
> > Is this a limitation of the extraction plugin, or am I missing
> > something when extracting Haskell?
> 
> Using the following commands produces pretty much what I'd expect to
> see:
> 
> > Extraction Language Haskell.
> > Extract Inductive Datatypes.nat => "Integer" ["0" "succ"]
> >   "(\fO fS n -> if n==0 then fO () else fS (n-1))".
> > Extract Inlined Constant plus => "(+)".
> > Extract Inlined Constant mult => "(*)".
> > Extraction fact_body.
> > Extraction fact.
> 

Hi

I would also expect this to work. Trevor, what kind of code do you obtain
and find unsatisfactory ? What is your version of Coq ?

> But using "Recursive Extraction fact" seems to generate too much code:
> it also produces code for mult and plus, which is exactly what the
> Extract Inlined Constant commands should avoid... 

This is bug #2469, which is now fixed in the svn archives.

By the way, since this kind of extraction from nat to Integer or ocaml's
equivalent seem to be quite popular these days, let me take the opportunity
to stress one more time how *unsafe* this approach is. I've only implemented
it as an experiment, after many user requests. But coding with nat while 
getting
efficient code only leave you currently with the illusion of certification.
The "Extract Inductive" line allows to simulate in Integer the computations
done on nat. That means awful complexities for almost everything, for a
correctness which is already questionable (is the hand-provided recursor above
really doing what we think ?). Then, we could hack more and more coq functions
by providing efficient haskell/ocaml replacements. Problem: each time you
"optimize" a function this way, you just "void the guarantee" some more,
so to say. And making mistakes while writing these Extract Constant is
_very_ easy.

So, for the vast amount of situations where computation speed is important
but not critical, I would rather advocate using datatypes like Z or N,
leaving as few nat as possible (for instance for counters). This way, the core
of the program is pristine extracted code, and the untrusted code is 
restricted
to some I/O and conversions (Integer<->Z for example).

Otherwise, for taking advantage of the full cpu speed, one can design a 
precise
sets of Parameters and Axioms, clearly identifying what is checked in coq and
what is left external. There are ongoing works aiming at providing such
axiomatizations and default implementations, cf for instance the "native 
integer"
branch.

Best regards,

Pierre Letouzey