
On 3 Jan 2008, at 3:40 AM, Jens Blanck wrote:
The normal view taken by Haskellers is that the denotations of Haskell types are CPPOs.
CPPO?
So:
(1) Must be monotone (2) Must be continuous
Could you please define what you mean by those terms in this context?
(Needn't be strict, even though that messes up the resulting category substantially).
I'm not convinced that the category is all that "messed up".
Well, no coproducts (Haskell uses a lifted version of the coproduct from CPO). Of course, Haskell makes things even worse by lifting the product and exponential objects, as well, which come to think of it is unnecessary even in the category of CPPOs and not necessarily strict continuous functions. The extra P would stand for "pointed" (has a least element, bottom), this is common in some communities. To me though, a cpo (complete partial order) is closed under directed suprema and the empty set is directed so bottom is already required. Not so. A set is directed iff every finite subset has an upper bound in the set; {} is finite, so it must have an upper bound in the set. So directed sets must be non-empty. (So CPOs needn't be pointed). jcc