The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

On Thu, Jun 4, 2009 at 2:18 PM, Pierre Letouzey
<Pierre.Letouzey AT pps.jussieu.fr>
 wrote:
> On Thu, Jun 04, 2009 at 12:25:35PM +0200, Adam Koprowski wrote:
>>    2. Extraction to Haskell does not support modules. That means that if 
>> one
>>    want to use parts of standard library with modules (such as very useful
>>    FSets/FMaps) then one basically has to give up the hope of extracting
>>    Haskell code, right? Or are there any work-arounds possible?
>>
>
> No hope for Haskell extraction of modules for the moment. But:
>
>  1) Now that Coq provides Type Classes, we can imagine having a
>    Type-Classes version of FSet/FMaps, it's somewhere on my TODO
>    list.

Just to let you guys know, I've already developed such a library, and
my experience is that it's a reasonable alternative to the
modules-based version in many cases. Switching from one to the other,
even in a big project, is surprisingly easy. There are still a couple
of things that I'm not satisfied with, but I'll try to make it
available ASAP. In any case, having both libraries in the contribs
raises the issue of duplication of proofs, maintenance, etc... that,
we can discuss in due course.

Stéphane
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06