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