13

I have this Haskell code which when compiled with GHC and run, aborts with a loop detected.

data Foo = Foo ()
 deriving (Eq,Show)

type Foop = Foo -> ((),Foo)

noOp :: Foop
noOp st = ((),st)

someOp :: Foop
someOp st@(Foo x) = ((),st)

(<+>) :: Foop -> Foop -> Foop
(<+>) f g st = let ((_,st'),(_,st'')) = ((f st),(g st')) in ((),st'')

main = print $ (noOp <+> someOp) $ Foo ()

I think it shouldn't, and here are some modifications. Each of them makes the loop go away:

  • change data Foo to newtype Foo
  • change (noOp <+> someOp) to (someOp <+> noOp)
  • remove the deconstruction @(Foo x)

Is this a bug in GHC or is it my lack of understanding the evaluation process?

Improve this question

2 Answers 2

Reset to default
12
  • Pattern match (_, _) demands WHNF of (f st, g st'). Easy.
  • Pattern match (_, (_,_)) demands WHNF of g st'. Here's the problem, because g is strict, hence it first needs st' in WHNF too. The runtime finds st' in the pattern ((_,st'), (_,_)), so before it can actually traverse down into st' it needs to WHNF both of the tuples. Because g is strict however, this first requires st'... and so on.

If you match the result of g with a lazy irrefutable pattern

(<+>) f g st = let ((_,st'), ~(_,st'')) = (f st, g st') in ((),st'')

then the problem goes away, because this is evaluated thus:

  • Pattern match (_, _) demands WHNF of (f st, g st'). Easy.
  • Pattern match (_, ~(_,_)) demands nothing more for the time being.
  • Pattern match ((_,st'), ~(_,_)) demands WHNF of f st. Fortunately, we can fulfill this, because st does not depend on the pattern.
  • Now we've satisfied the pattern match, the runtime can already proceed with the in ((),st''). Only at this point is the irrefutable pattern ~(_,st'') forced, but this is now not a problem anymore because st' is available here, so it's just a matter of computing g once.

The fixes you've tried all amount to making g non-strict:

remove the deconstruction @(Foo _)

Without that, g doesn't really need to look at its argument to construct the result skeleton, i.e. the tuple match (_,st'') can then succeed without first requiring WHNF of st'.

change data Foo to newtype Foo

This has the effect that the Foo constructor doesn't actually exist at runtime, so there's nothing that the pattern st@(Foo _) would force.

change noOp <+> someOp to someOp <+> noOp

As I said, the loop only comes about because g is strict. If you put f in its position, which is not strict, then there's no problem.

Improve this answer
Sign up to request clarification or add additional context in comments.

6 Comments

Thanks, this might be a good step towards helping me to understand it :-) However I still don't understand why it can't first WHNF the left tuple to get st' and then the right tuple to get st''? I can see that WHNFing the right tuple requires WHNFing the left tuple but I don't see the problem with WHNFing the left tuple.
You can first WHNF the left tuple, but it doesn't give you st'. It only gives you (_,~st'), as it were.
In the specific case, (_,st') = f st = noOp st = ((),st), so st' = st = Foo () which would also satisfy the strictness of g alias someOp. Shouldn't this be possible to compute?
let Pat (Pet x) (Pot y) = bar in baz is evaluated as let Pat ξ υ = bar in ξ `seq` υ `seq` (let Pet x = ξ; Pet y = υ in baz). So υ is forced before x actually gets into being.
I think that doesn't explain why forcing υ wouldn't force x. What you say makes it sound (to me) like it should be a statically invalid expression.
|
7

It's not a bug -- you just found a tricky corner of the lazy pattern semantics. Let me present a simpler case:

> data Id a = Id a
> let Id a = undefined ; Id b = Id 3 in b
3
> let (Id a, Id b) = (undefined, Id 3) in b
*** Exception: Prelude.undefined

The difference is that the first let is equivalent to

case undefined of
  ~(Id a) -> case Id 3  of
               ~(Id b) -> b

while the second is

case (undefined, Id 3) of
  ~(Id a, Id b) -> b

The first will not evaluate the undefined unless a is demanded (which does not happen).

The second will pattern match against both patterns Id a and Id b as soon as either variable is demanded, forcing both undefined and Id 3 in the process.

Note that, because of this issue, the patterns ~(K1 (K2 x) (K3 y)), ~(K1 ~(K2 x) (K3 y)), ~(K1 (K2 x) ~(K3 y)) and ~(K1 ~(K2 x) ~(K3 y)) have different semantics.

To fix your code, try

let (~(_,st'),~(_,st'')) = ((f st),(g st')) in ((),st'')

or

let (_,st') = f st ; (_,st'') = g st' in ((),st'')
Improve this answer

7 Comments

It's sufficient to use one irrefutable match: let ((_,st'), ~(_,st'')) = (f st, g st').
@leftaroundabout Isn't st'' the first thing which is demanded? let ... in ((), st''). Further, g could be non-strict in the general case.
Thanks, that was insightful. Now in my code there is no undefined and I still don't see why it loops. Could you also shed some light on that?
@JoSo Briefly put, there is a circular dependency between st',st'' and f st, g st' since st' occurs in both. This makes the definition recursive, essentially. The patterns, as they are, force both f st and g st' before defining (loosely speaking) st', st'', triggering a loop. leftaroundabout explained in his answer at the top in more detail.
Well, with f _ = undefined you create a new problem that's somewhat unrelated to the original question. I wouldn't make that other pattern lazy without good reason – lazy patterns tend to be pretty bad for performance. (Indeed your other proposal, let (_,st') = f st ; (_,st'') = g st' in ((),st''), is IMO a better solution than anything with lazy patterns.)
|

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.