-XStrict: Why some binders are not made strict?

[Simon Peyton Jones]

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

You make good points.  Also, consider

	f (g x)

where f is define in some other (lazy) module.  Is that done call-by value?  That is, is (g x) evaluated before the call?  According to the current spec, no. So a thunk is built!

But if we write

	let y = g x in f y

then, lo, the (g x) is computed eagerly.

So the present semantics seems to be more 
	functions always evaluate their arguments to
      WHNF (but not to NF)!

I do think this could do with a tighter spec.  Johan, Adam, this is your baby.

Simon


|  -----Original Message-----
|  From: Roman Cheplyaka [mailto:roma at ro-che.info]
|  Sent: 11 December 2015 23:56
|  To: Simon Peyton Jones <simonpj at microsoft.com>; Johan Tibell
|  <johan.tibell at gmail.com>
|  Cc: ghc-devs at haskell.org
|  Subject: Re: -XStrict: Why some binders are not made strict?
|  
|  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
|  >
|