On Fri, Sep 7, 2012 at 5:56 PM, Edward Z. Yang
<ezyang@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...)
Edward