More on liftings: In our FPCA 91 paper, Simon and I came to the conclusion that the "proper" way to give semantics to data declarations was, as follows. If data T = A U V | B W then the model for T (written here T*) is T* = ((U* x V*) + W*)_\bot where the x is pure domain product, the + is disjoint union (i.e. not smash sum, not separated sum, but a union which results in a domain without a least element), and _\bot is lifting. The form of bottomless types is now obvious: bottomless S = A U V | B W is modelled by S* = (U* x V*) + W* What this means is that constructors really are playing three roles in standard Haskell: they are formed as a composition of lifting and injection into a sum, and introduce a (true) product. I believe we ought to be very cautious about introducing special cases for single constructors, for example, which do not generalise neatly. John.
