The Coq mailing list

[Trevor Elliott <awesomelyawesome AT gmail.com>]

Hi Everyone,

While playing around with extraction, I noticed a possible
inconsistency in the way that Coq treats extraction targets.  For
example, when extracting this implementation of factorial:

> Fixpoint fact_body (a n : nat) : nat :=
>   match n with
>     | 0   => a
>     | S m => fact_body (a*n) m
>   end.
> Definition fact : nat -> nat := fact_body 1.

Coq will produce very efficient OCaml, when ExtrOcamlNatInt is
imported, but inefficient Haskell or Scheme; mult and plus are
translated to the OCaml (*) and (+) operators.  Initially, I thought
that this was due to a lack of a set of analogous ExtrHaskell* and
ExtrScheme* modules in plugins/extraction, but producing my own
version of ExtrOcamlNatInt for Haskell yielded no change in the
extracted code.

Is this a limitation of the extraction plugin, or am I missing
something when extracting Haskell?

Thanks!

--trevor