-XStrict: Why some binders are not made strict?

[Roman Cheplyaka]

Thanks Simon, this is an interesting and compelling interpretation. But
I'm wondering whether it is enough to specify the dynamic semantics
unambiguously.

Two examples:

1.

  let _ = undefined in ()

Intuitively, since we are talking about /strictness/, this should
evaluate to bottom. However, it seems that your rule also admits () as
an answer; it is equivalent to () under lazy evaluation *and* it does
not create any thunks.

2.

  f g = g undefined

When compiled lazily, this code doesn't construct any thunks:

  f = \r srt:SRT:[02v :-> undefined] [g_suM] g_suM undefined;

So, under your rule, this is an admissible code for -XStrict, too. But
we can hardly call it strict.

On 12/12/2015 12:38 AM, Simon Peyton Jones wrote:
> | As I said, I prefer this semantics mainly because it's easier to
> | explain: all variables (and underscores) bound in a strict module refer
> | to WHNF values. Do you have a similarly simple explanation for the
> | semantics you're suggesting?
> 
> Here's one, which is roughly what the current implementation does (modulo bugs):
> 
> * Code compiled under -XStrict constructs no thunks.
> 
> So consider
> 
> 	module M1 where data T = C Int Int
> 	module M2 where f n = C (n+1) (n-1)
> 	module M3 where g x = let C y z = f x in ...
> 
> Look at M3.  Usually we'd get a thunk for (f 4), but not with -XStrict.  But even with -XStrict in M3, y,z might be bound to thunks.   
> 
> If you compile M2 with -XStrict, function f won't build thunks for (n+1), (n-1) but will evaluate them instead.
> 
> If you compile M1 with StrictData, then C is made strict, so again M2 will build no thunks even if M2 was compiled without -XStrict.
> 
> I quite like this design.  It's not clear to me that anything useful is gained by forcing y and z in M3 before evaluating the body "...".
> 
> 
> So Roman's design makes sense, but so does the implemented design (modulo any bugs).  The trouble is that the implemented design is not well described.
> 
> Simon
> 
> | -----Original Message-----
> | From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Roman
> | Cheplyaka
> | Sent: 11 December 2015 12:57
> | To: Johan Tibell <johan.tibell at gmail.com>
> | Cc: ghc-devs at haskell.org
> | Subject: Re: -XStrict: Why some binders are not made strict?
> | 
> | On 12/11/2015 02:21 PM, Johan Tibell wrote:
> | > If we force strictness all the way down it's not really call-by-value
> | > either, because the caller doesn't know what to evaluate (I think).
> | 
> | Not sure what you mean here.
> | 
> | > In addition, making pattern matching strict in this way makes it hard to
> | > mix and match strict and lazy data types (e.g. Maybe), because using a
> | > lazy data type from another module will make it appear strict in your
> | > code (hurting modularity).
> | 
> | I don't think this is a case about modularity. A lazy Maybe value
> | defined in a lazy module remains lazy; and you can pass it to lazy
> | functions without forcing it. Only when you pattern match on it *in the
> | strict module*, the evaluation happens.
> | 
> | As I said, I prefer this semantics mainly because it's easier to
> | explain: all variables (and underscores) bound in a strict module refer
> | to WHNF values. Do you have a similarly simple explanation for the
> | semantics you're suggesting?
> | 
> | Roman
> 


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20151212/9fe24416/attachment.sig>