Two Thoughts

I posted a mail about an impure calculus. Now the question would be: Why would one be interested in that? The answer is rather trivial.

Even pure programming languages, like Haskell and Clean, compile to side-effecting programs, even when they carefully try to hide that. The underlying semantics of a functional program is, without being too pompous about it, therefore best expressed in an impure calculus. Ideally with a corresponding operational semantics, since that is what programs do: They have run-time behaviour.[1][2][3]

Now, the reason why am I interested in lazy calculi: I want mostly eager behaviour -I like predictability,- but at some points I want laziness for it's expressiveness. For example, one really nice thing about Haskell is that equivalence of, say, the contents of two trees may be determined by lazily unfolding them to two lists and checking those lists for equality. This is hard to program in a language with eager semantics. I was wondering if I could `cheat` my way around this problem and settle on a semantics in the middle of lazy and eager behaviour, the language seems to be eager, but, under water, when side-effect free, the language is essentially lazy. I.e., when dealing with pure functions/data, evaluation is lazy.

No idea whether the latter is achievable. Guess not, though Haskell proves otherwise. Rephrasing: Not as easily as I want it - with this semantics I'll end up with an impure Haskell variant. Worst of both worlds.

^[1] Black addendum: And if I read one more paper which thinks it'll contribute anything interesting to compiler technology by chasing arrows, I'll puke, and see it as an outright failure of fundamental CS to get anything right.
^[2]I am referring to compiler/code-generation techniques here, not top-level type-theoretical concerns.
^[3]An ideal compiler for a pure lazy language would compile superficially effect-free programs down to lazy side-effecting terms to eager side-effecting terms to imperative code. Then again, ideals don't work, and it seems it has been investigated anyway. Though this might almost exactly be what GHC does these days.