The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

For strings, as far as I can remember, I would not advise use of the String library, as in Haskell, strings are lists of characters, and Coq does not use a list, but some structure which is isomorph to a list but have less primitives than what provides the List module (so giving up the String module to a list of <to be defined> would be more convenient in the Coq side, and should ease integration with Haskell), furthermore Haskell strings are not Ascii set only (it has support for Unicode), so it could be a bad idea to use the String Coq module anyway.

What is a sad thing when extracting is that Coq Type classes are not converted into Haskell ones, and that Coq Modules do not have an equivalent in the Haskell side (nor does dependant types). Agda would probably a better option than Coq to extract code to Haskell. I do not know if there exists good translations from Coq to Agda though.

Note also that good practice to extract to OCaml might not apply to Haskell, for instance you do not have to worry on side effects for higher order functions:
in OCaml, the extraction of a "(A -> B) -> C" function or of inductive types which can hold functions, are problematic as the properties of an extracted function can be broken when running the extracted function with an argument which is a function which performs a side effect.

2014-03-06 1:49 GMT+01:00 Kevin Sullivan <sullivan.kevinj AT gmail.com>:

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

--
.../Sedrikov\...