Re: [Haskell-cafe] Haskell with all the safeties off

Le Sat, 8 Sep 2012 09:20:29 +0100, Ramana Kumar a écrit :

On Fri, Sep 7, 2012 at 5:56 PM, Edward Z. Yang wrote:

...

Excerpts from David Feuer's message of Fri Sep 07 12:06:00 -0400 2012:

...

They're not *usually* desirable, but when the code has been proven not to fall into bottom, there doesn't seem to be much point in ensuring that things will work right if it does. This sort of thing only really makes sense when using Haskell as a compiler target.

OK, so it sounds like what you're more looking for is a way of giving extra information to GHC's strictness analyzer, so that it is more willing to unbox/skip making thunks even when the analyzer itself isn't able to figure it out. But it seems to me that in any such case, there might be a way to add seq's which have equivalent effect.

But in the case that you've independently proven the code correct, it would be much more convenient to just tell GHC to "trust me" with a flag rather than having to go analyse and edit the code to put in the required seqs (thereby breaking the proof too...)

For Coq, I think that you can do something like: Definition seq {A B : Type} (a : A) (b : B) := b. Then you do your code the Haskell way. As seq is mainly the identity, it won't bother you for proofs (and won't break inductive definition using Fixpoint). And as I am pretty sure the extraction doesn't inline functions, you then just have to do something like: Extraction Constant seq "seq". (* I do not recall very well the syntay here, but it is documented *) Then your extracted code will place seq where you requested them. I am recompiling Coq, yet, so I cannot test it. This way, it won't break the proof (but you have to place more faith in the extraction system).

...

Edward

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe