The Coq mailing list

[Trevor Elliott <awesomelyawesome AT gmail.com>]

Hi Everyone,

I think that my previous emails haven't really capured the problem that I've
been encountering, so I'm including a full example to describe the situation.

I would like to extract this function, defined in Coq, to Haskell, and get a
reasonably efficient implementation:

> Function example (a b c:nat) : nat := a*b + c.

For the sake of the example, I'm going to start off by extracting to OCaml.

> Extraction Language Ocaml.
> Recursive Extraction example.

This produces the following OCaml program:

> type nat =
>   | O
>   | S of nat
>
> (** val plus : nat -> nat -> nat **)
>
> let rec plus n m =
>   match n with
>     | O -> m
>     | S p -> S (plus p m)
>
> (** val mult : nat -> nat -> nat **)
>
> let rec mult n m =
>   match n with
>     | O -> O
>     | S p -> plus m (mult p m)
>
> (** val example : nat -> nat -> nat -> nat **)
>
> let example a b c =
>   plus (mult a b) c

I can make this version more efficient by importing the ExtrOcamlNatInt 
module.

> Require Import ExtrOcamlNatInt.
> Extraction Language Ocaml.
> Recursive Extraction example.

This produces the following program that uses the native implementations of
multiplication and addition:

> (** val plus : int -> int -> int **)
>
> let rec plus = (+)
>
> (** val mult : int -> int -> int **)
>
> let rec mult = ( * )
>
> (** val example : int -> int -> int -> int **)
>
> let example a b c =
>   plus (mult a b) c

All of this works as I would expect.  The problems show up when I attempt to
repeat this process for extraction to Haskell.  Repeating the first step, I 
can
extract the example function to Haskell, initially producing an inefficient
implementation:

> Extraction Language Haskell.
> Recursive Extraction example.

Produces this Haskell program:

> module Main where
>
> import qualified Prelude
>
> data Nat = 0
>          | S Nat
>
> plus :: Nat -> Nat -> Nat
> plus n m =
>   case n of
>     O -> m
>     S p -> S (plus p m)
>
> mult :: Nat -> Nat -> Nat
> mult n m =
>   case n of
>     O -> O
>     S p -> plus m (mult p m)
>
> example :: Nat -> Nat -> Nat -> Nat
> example a b c =
>   plus (mult a b) c

Adding Extract Constant for mult and plus should yield implementations of mult
and plus that look like:

> mult :: Prelude.Int -> Prelude.Int -> Prelude.Int
> mult  = (*)

I setup the extraction like this:

> Extract Constant mult => "(*)".
> Extract Constant plus => "(+)".
> Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ]
>   "(\f0 fS n -> if n <= 0 then f0 () else fS (n-1))".
> Extraction Language Haskell.
> Recursive Extraction example.

But the result looks much the same as the first time; the only difference is
that the resulting program lacks the definition of Nat.

> module Main where
>
> import qualified Prelude
>
> plus :: Prelude.Int -> Prelude.Int -> Prelude.Int
> plus n m =
>   (\f0 fS n -> if n <= 0 then f0 () else fS (n-1))
>     (\_ -> m)
>     (\p -> Prelude.succ (plus p m))
>     n
>
> mult :: Prelude.Int -> Prelude.Int -> Prelude.Int
> mult n m =
>   (\f0 fS n -> if n <= 0 then f0 () else fS (n-1))
>     (\_ -> 0)
>     (\p -> plus m (mult p m))
>     n
>
> example :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int
> example a b c =
>   plus (mult a b) c

So my main question is: how can I force the definitions of plus and mult to be
the ones that I supply with the Extract Constant command, producing Haskell
code that looks like the OCaml example?

Thanks,

--trevor