On Thu, Jan 17, 2002 at 12:16:14PM +0000, Ross Paterson wrote:
We can avoid smash products and coalesced sums by analysing [t] as being the lifting of a not-necessarily-pointed cpo T[[t]]:
[t] = lift (T[[t]])
We can define T[[t]] by induction over t, using the following operations on cpos (not necessarily having a bottom element):
lift D = D plus a new bottom element D x E = cartesian product of D and E D + E = disjoint union of D and E D -> E = the cpo of continuous functions from D to E 1 = the one-element cpo 0 = the empty cpo ... For Haskell's function type, we have
T[[s -> t]] = [s] -> [t]
If I understand it correctly, this makes \x.undefined :: a -> b different from undefined :: a -> b For instance, in this setup, the CPO [()->()] has four elements, in a totally ordered CPO; in increasing order, they are undefined const undefined id const () Is it really clear the first two ('undefined' and 'const undefined') are different? Ken says they are observationally equivalent. --Dylan Thurston