The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Pierre,

thanks for your reply.

Pierre Letouzey (Mon, Jun 14, 2004 at 05:55:49PM +0200):
> On Sun, 13 Jun 2004, Stefan Karrmann wrote:
> > as a newbie to coq I have some questions. As I'm used to functional
> > programs I tried to start with function definitions and extraction.
> >
> > How can I switch from coq's nat to Haskell's Integer type? The former
> > uses much more memory.
> 
> Well, for the moment, nothing fully automatic exists to replace nat by
> Integer (or Ocaml equivalent). It could be done, but would not be so
> simple:
> 
> - In the case where you have only a type domain and a few operations, e.g:
> Parameter my_nat : Set.
> Parameter my_zero : my_nat.
> Parameter my_plus : my_nat -> my_nat -> my_nat.
> Then it is trivial to replace these axioms by efficient implementations
> when extracting:
> Extract Constant my_nat => "Integer"
> Extract Constant my_zero => "0"
> Extract Constant my_plus => "(+)"
> 
> - But Coq nat is more than a type with a few operations: it has an
> inductive structure (data Nat = O | S Nat) and you can do matching on a
> nat value. So you need to translate this matching to Haskell Integer.
> Of course this can be done, but if you do it systematically, you loose all
> the interest of a translation to Integer. For example, plus in nat is
> defined by matching, and you would then obtain a linear-time plus in
> Haskell instead of the quasi-constant-time (+).

Would views help, cf. `Views: An Extension to Haskell Pattern Matching'
<http://www.haskell.org/development/views.html>?
quote:
  view (Integral a) => Natural a of a = Zero | Succ a
     where
       natural 0 = Zero
       natural n
         | n > 0      = Succ (n-1)
         | otherwise
            = error "Natural: Natural view excludes negative values"
   [...]
   In a view declaration of the form

      view c => s of t = k where d

   is equivalent to

      data c => s = k
      d

   and is valid if and only if d defines (only) a suitably named function
   of type c => t -> s and [...]

At least the equivalent pure haskell implementation should help for
extractions to Haskell and Ml.

Sincerly,
-- 
Stefan Karrmann