The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

My response here is in danger of coming across as rudely close to "RTFM," but: have you read the whole chapter of the Coq reference manual called "Extraction of programs in Objective Caml and Haskell"?  There I think you find all the commands you need to do extraction to alternative type representations, as long as your original code contains no explicit pattern matches on those types.

On 03/06/2014 07:14 AM, Kevin Sullivan wrote:

Thanks Greg and Cedric,

I'm not necessarily committed to Haskell. What hooks did you, Greg, have in mind for doing such mappings/replacements when extracting to OCaml?

Kevin

On Wed, Mar 5, 2014 at 11:05 PM, Greg Morrisett <greg AT eecs.harvard.edu> wrote:
I don't have experience extracting Haskell, but when I do OCaml,
I tend to map certain things (ascii, nat) to native OCaml
types (e.g., char, bignum).  I agree it's less than optimal, but
that's the price of interoperability with legacy code...

Anyway, there are good hooks for doing this kind of replacement.