Haskell with all the safeties off

David Feuer

6 Sep 2012 6 Sep '12

7:35 p.m.

I have no plans to do such a thing anytime soon, but is there a way to tell GHC to allow nasal demons to fly if the program forces bottom? This mode of operation would seem to be a useful optimization when compiling a program produced by Coq or similar, enabling various transformations that can turn bottom into non-bottom, eliminating runtime checks in incomplete patterns, etc.

Attachments:

attachment.html (text/html — 389 bytes)

Show replies by date

Edward Z. Yang

7 Sep 7 Sep

2 a.m.

Haskell already does this, to some extent, in the design of imprecise exceptions. But note that bottom *does* have well defined behavior, so these "optimizations" are not very desirable. Edward Excerpts from David Feuer's message of Thu Sep 06 19:35:43 -0400 2012:

...

I have no plans to do such a thing anytime soon, but is there a way to tell GHC to allow nasal demons to fly if the program forces bottom? This mode of operation would seem to be a useful optimization when compiling a program produced by Coq or similar, enabling various transformations that can turn bottom into non-bottom, eliminating runtime checks in incomplete patterns, etc.

David Feuer

12:06 p.m.

On Sep 7, 2012 2:00 AM, "Edward Z. Yang" @ mit.edu > wrote:

...

Haskell already does this, to some extent, in the design of imprecise exceptions. But note that bottom *does* have well defined behavior, so these "optimizations" are not very desirable.

...

Edward

Excerpts from David Feuer's message of Thu Sep 06 19:35:43 -0400 2012:

...
I have no plans to do such a thing anytime soon, but is there a way to tell GHC to allow nasal demons to fly if the program forces bottom? This mode of operation would seem to be a useful optimization when compiling a

...

...
produced by Coq or similar, enabling various transformations that can turn bottom into non-bottom, eliminating runtime checks in incomplete

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. program patterns,

...

...
etc.

Edward Z. Yang

12:56 p.m.

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. Edward

Ramana Kumar

8 Sep 8 Sep

4:20 a.m.

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...)

...

Edward

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

AUGER Cédric

3:10 p.m.

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

4640

Age (days ago)

4642

Last active (days ago)

List overview

Download

5 comments

4 participants

participants (4)

AUGER Cédric
David Feuer
Edward Z. Yang
Ramana Kumar