The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

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