-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 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
| >
|
More information about the ghc-devs
mailing list