XStrict: Why some binders are not made strict?
Simon Peyton Jones
simonpj at microsoft.com
Tue Dec 15 15:00:11 UTC 2015
 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 callby 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 roche.info]
 Sent: 11 December 2015 23:56
 To: Simon Peyton Jones <simonpj at microsoft.com>; Johan Tibell
 <johan.tibell at gmail.com>
 Cc: ghcdevs 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) (n1)
 > 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), (n1) 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: ghcdevs [mailto:ghcdevsbounces at haskell.org] On Behalf Of
 >  Roman Cheplyaka
 >  Sent: 11 December 2015 12:57
 >  To: Johan Tibell <johan.tibell at gmail.com>
 >  Cc: ghcdevs 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
 >  > callbyvalue 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
 >

More information about the ghcdevs
mailing list