Some people have referred to semantic issues and Abramsky and Ong's work when contributing to the lifted/unlifted debate. I think it would be fair to summarise them as follows. Pro lifting =========== The simplest possible lambda calculus has lifting in its canonical model as soon as "laziness" is introduced. Otherwise, non-strict constructors could not be modelled in the calculus. When actual non-strict constructors are provided, therefore, essentially nothing new has been added. The same models work beautifully. Thus in my POPL 93 paper about lazy semantics, I used lifted function spaces to obtain a direct correspondence between operational and denotational semantics that held *everywhere*. Contrast this with Purushothaman and Seaman's ESOP 92 paper where they used unlifted function spaces, and there the correspondence was only true at base types. Summary: operational and denotational models "fit" with one another if function spaces are lifted (and products too by implication). Con Lifting =========== If our goal is to improve equational reasoning then, as many people have pointed out, more (interesting) equations hold when function and product spaces are not lifted. Furthermore, the natural semantics of unboxed types is that of domains without bottoms (FPCA 91), so if Haskell is ever likely to move (in the future) in the direction of accepting unboxed types into its definition, then it would make sense not to introduce possibly unnecessary liftings elsewhere. John.
