Bang patterns, ~ patterns, and lazy let

[John Hughes]

Simon Peyton-Jones wrote:

>| What have you got in mind? ANY tupling of bindings may change the SCC
>| structure, and hence the results of type inference--I'm taking that as
>| read. But that still leaves the question of whether the dynamic
>| semantics of the program is changed. Let's assume for the time being
>| that all bindings carry a type signature--then the SCC structure is
>| irrelevant, isn't it? Or am I missing something here? I'm under the
>| impression that the *dynamic* semantics of
>| 
>|     p1 = e1
>|     p2 = e2
>| 
>| *would* be the same as (p1,p2) = (e1,e2) under my strict matching
>| proposal. I don't see how the SCC structure can affect that.
>
>Well I put the example that you sent me on the Wiki, right at the
>bottom.  Did I get it wrong?
>
>  let { (y:ys) = xs; (z:zs) = ys } in body
>means
>  case xs of (y:ys) -> case ys of (z:zs) -> body
>
>whereas
>  let (y:ys, z:zs) = (xs,ys)  in body
>means
>  case (fix (\~(y:ys, z:zs). (xs,ys))) of (y:ys, z:zs) -> body
>
>which isn't the same.
>
>Simon
>  
>
Oh yes, you're right of course.

In the denotational semantics I wrote last night, multiple bindings are 
combined using (+), which *is* the same as tupling them. But remember 
the thing I left unproven, because it was late at night?

E[[let defs1 in let defs2 in exp]]env = E[[let defs1; defs2 in exp]]env


It's not true, as this example shows. That'll teach me! In

	let y:ys = xs; z:zs = ys in body

then the result is _|_, because matching the entire *group* against (xs, _|_) fails, but once the example is split into two nested lets then everything works. Yuck.


John