The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

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.

-Greg

On 3/5/2014 7:49 PM, Kevin Sullivan wrote:

Dear Colleagues:

A grad student of mine is looking at integrating Haskell code extracted
from a Coq specification into an industrial environment. The environment
in this case includes a standard Haskell installation, the yesod web
service framework, etc. The Coq spec uses types such as Coq String, Coq
Z, etc. When we extract code, we end up with extracted versions of Coq
string, Coq Z etc. But the frameworks expect the use of their
"built-in" analogs, e.g., Haskell's String type.

The question is, what's the current best practice for "bridging" from
Coq's types to analogs provided and used natively in target languages
and related frameworks? Or for swapping out definitions extracted from
Coq and allowing references to be bound to the native versions? Clearly
doing such a substitution increases the TCB, nor is it necessarily safe,
in that the semantics might not always match exactly.

So, again, what is the best practice in this regard?

Thanks,
Kevin