coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
- To: Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>
- Cc: Adam Koprowski <adam.koprowski AT gmail.com>, coq-club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Issues/questions with extraction.
- Date: Thu, 4 Jun 2009 14:35:51 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=cmKSSPuYu508aYkxAdt32g22aH9ZKwyXCEK+cHExo5y7ol/mok8067Tn4QesTeeKEI uDyKWuHeuv96X+/NpgqZr7o3GvGLDfhsQ+rXJbqjSpCA/2HN5cO/GjKmyns+o7Oth+UA 8hvCKPaSztxliA1hd1NVbvQpROXxl03qUZxc8=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Issues/questions with extraction., Adam Koprowski
- Re: [Coq-Club] Issues/questions with extraction.,
Pierre Letouzey
- Re: [Coq-Club] Issues/questions with extraction., Stéphane Lescuyer
- Re: [Coq-Club] Issues/questions with extraction.,
Adam Koprowski
- Re: [Coq-Club] Issues/questions with extraction.,
Yves Bertot
- Re: [Coq-Club] Issues/questions with extraction.,
Andrej Bauer
- Re: [Coq-Club] Issues/questions with extraction.,
Adam Chlipala
- Re: [Coq-Club] Issues/questions with extraction.,
Jean-Francois Monin
- Re: [Coq-Club] Issues/questions with extraction., Ryan Rusich
- Re: [Coq-Club] Issues/questions with extraction.,
Jean-Francois Monin
- Re: [Coq-Club] Issues/questions with extraction.,
Adam Chlipala
- Re: [Coq-Club] Issues/questions with extraction.,
Andrej Bauer
- Re: [Coq-Club] Issues/questions with extraction.,
Yves Bertot
- Re: [Coq-Club] Issues/questions with extraction.,
Pierre Letouzey
Archive powered by MhonArc 2.6.16.