[Haskell-cafe] Haskell with all the safeties off

[AUGER Cédric]

Le Sat, 8 Sep 2012 09:20:29 +0100,
Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> a écrit :

> On Fri, Sep 7, 2012 at 5:56 PM, Edward Z. Yang <ezyang at mit.edu> 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 at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >